Fix scholarly_paper

Isabelle_DOF-Example-II/paper.thy

@@ -527,7 +527,7 @@ a denotational proof.
 \<close>
 
 
-Corollary*[co1::"corollary", short_name="\<open>Corollaries on reference processes.\<close>",level="Some 2"]
+Corollary*[co1::"corollary", short_name="\<open>Corollaries on \<open>{DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>\<close>",level="Some 2"]
 \<open> \<^hfill> \<^br>  \<^vs>\<open>-0.3cm\<close>
   \<^enum> \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<sqsubseteq>\<^sub>\<F> CHAOS A\<close>
   \<^enum> \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<sqsubseteq>\<^sub>\<F> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A\<close>  

Isabelle_DOF-Unit-Tests/ROOT

@@ -13,7 +13,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
     "Attributes"
     "AssnsLemmaThmEtc" 
     "Ontology_Matching_Example"
-    "Cenelec_Test"
+    (*"Cenelec_Test"*)
     "OutOfOrderPresntn"
   document_files
     "root.bib"

Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy

@@ -159,6 +159,10 @@ doc_class example  = text_section +
    short_name      :: string <= "''''"
    invariant L\<^sub>e\<^sub>x\<^sub>a    :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 0"
 
+text*[bu::author]\<open>\<close>
+
+text*[tt::example , main_author = "Some (@{author \<open>bu\<close> })"]\<open>\<close>
+
 text\<open>The intended use for the \<open>doc_class\<close>es \<^verbatim>\<open>math_motivation\<close> (or \<^verbatim>\<open>math_mtv\<close> for short),
      \<^verbatim>\<open>math_explanation\<close> (or \<^verbatim>\<open>math_exp\<close> for short) and 
      \<^verbatim>\<open>math_example\<close> (or \<^verbatim>\<open>math_ex\<close> for short)
@@ -671,6 +675,32 @@ define_shortcut* eg  \<rightleftharpoons> \<open>\eg\<close>  (* Latin: „exemp
                  etc \<rightleftharpoons> \<open>\etc\<close> (* Latin : „et cetera“ meaning „et cetera“ *)
 
 print_doc_classes
+Definition*[testdef::"definition"]\<open>\<close>
+ML\<open>
+val thy = \<^theory>
+\<close>
+ML\<open>
+val ctxt = Proof_Context.init_global thy
+fun ltx_of_term _ _ (c as \<^Const_>\<open>Cons \<^Type>\<open>char\<close> for _ _\<close>) = HOLogic.dest_string c
+          | ltx_of_term _ _ \<^Const_>\<open>Nil _\<close> = ""
+          | ltx_of_term _ _ \<^Const_>\<open>numeral _ for t\<close> = Int.toString(HOLogic.dest_numeral t)
+          | ltx_of_term ctx encl \<^Const_>\<open>Cons _ for t1 t2\<close> =
+              let val inner = (case t2 of 
+                                 \<^Const_>\<open>Nil _\<close> => ltx_of_term ctx true t1
+                              | _ => ((ltx_of_term ctx false t1)^", " ^(ltx_of_term ctx false t2)))
+              in if encl then enclose "{" "}" inner else inner end
+          | ltx_of_term _ _ \<^Const_>\<open>None _\<close> = ""
+          | ltx_of_term ctxt _ \<^Const_>\<open>Some _ for t\<close> = ltx_of_term ctxt true t
+          | ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t)
+val cid = "definition"
+val cid_long = DOF_core.get_onto_class_name_global' cid thy
+fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) 
+                                            (Symbol.explode (YXML.content_of s)))
+fun toLong n =  #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy))
+val default_args = map (fn (b,_,t) => (toLong (Long_Name.base_name ( Sign.full_name thy b)), 
+                                                       ltx_of_term ctxt true t))
+                               (DOF_core.get_attribute_defaults cid_long thy)
+\<close>
 
 end
 

Isabelle_DOF/thys/Isa_DOF.thy

@@ -2223,7 +2223,10 @@ fun meta_args_2_latex thy sem_attrs transform_attr
         val label_and_type = String.concat [ l, ",", cid_txt]
         val str_args = label_and_type::str_args
     in
-      Latex.string (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"]))
+      (*Latex.string (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"]))*)
+      (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"]))
+      |> Syntax.read_input
+      |> Document_Output.output_document ctxt {markdown = true}
     end
 
 (* level-attribute information management *)
@@ -2298,14 +2301,12 @@ val _ =
   document_command \<^command_keyword>\<open>text*\<close> "formal comment (primary style)"
     {markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) [] I;
 
-
 (* This is just a stub at present *)
 val _ =
   document_command \<^command_keyword>\<open>text-macro*\<close> "formal comment macro"
     {markdown = true, body = true}
     (gen_enriched_document_cmd {inline=false} (* declare as macro *) I I) [] I;
 
- 
 val (declare_reference_default_class, declare_reference_default_class_setup) 
      = Attrib.config_string \<^binding>\<open>declare_reference_default_class\<close> (K "");
 
@@ -3591,4 +3592,114 @@ scala_build_generated_files
     "scala/dof.scala"
     "scala/dof_document_build.scala" (in "../")
 
+ML\<open>
+val str_args = ["short_name=\<open>Corollaries on \<open>{DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>\<close>"]
+val t = Latex.string (enclose "[" "]" (String.concat [", args={", (commas str_args), "}"]))
+\<close>
+ML\<open>
+val ctxt = \<^context>
+val s = "\<open>Corollaries on \<open>{DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>\<close>"
+val markdown = true
+
+val input = Syntax.read_input s
+val tt = Document_Output.output_document ctxt {markdown = markdown} input
+val ttt = Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) "cons\<^sub>a\<upsilon>"
+val str_args = ["short_name=" ^ s]
+val t = Latex.string (enclose "[" "]" (String.concat [", args={", (commas str_args), "}"]))
+\<close>
+ML\<open>
+val ctxt = \<^context>
+val ss = ["[ ", "a", " ]"]
+val markdown = true
+
+val inputs = ss |> map Syntax.read_input
+val tt = inputs |> map (Document_Output.output_document ctxt {markdown = markdown})
+val ttt = flat tt
+\<close>
+
+ML\<open>
+val ctxt = \<^context>
+val s = "[ a ]"
+val markdown = true
+
+val input = Syntax.read_input s
+val tt = Document_Output.output_document ctxt {markdown = markdown} input
+\<close>
+text\<open>\<open>Corollaries on \<open>{DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>\<close>\<close>
+(*datatype math_content_class = 
+    "defn"       \<comment>\<open>definition\<close> 
+  | "axm"        \<comment>\<open>axiom\<close>
+  | "theom"      \<comment>\<open>theorem\<close> 
+  | "lemm"       \<comment>\<open>lemma\<close>
+  | "corr"       \<comment>\<open>corollary\<close>
+  | "prpo"       \<comment>\<open>proposition\<close>
+  | "rulE"       \<comment>\<open>rule\<close>
+  | "assn"       \<comment>\<open>assertion\<close>    
+  | "hypt"      \<comment>\<open>hypothesis\<close>    
+  | "assm"       \<comment>\<open>assumption\<close>
+  | "prms"       \<comment>\<open>premise\<close>  
+  | "cons"       \<comment>\<open>consequence\<close>
+  | "conc_stmt"  \<comment>\<open>math. conclusion\<close>
+  | "prf_stmt"   \<comment>\<open>math. proof\<close>
+  | "expl_stmt"  \<comment>\<open>math. example\<close> 
+  | "rmrk"       \<comment>\<open>remark\<close>  
+  | "notn"       \<comment>\<open>notation\<close>  
+  | "tmgy"       \<comment>\<open>terminology\<close>
+
+doc_class "consequence" = 
+   referentiable :: bool <= "True"
+   level         :: "int option"         <= "Some 2"
+   mcc           :: "math_content_class" <= "cons" 
+   invariant d7  :: "mcc \<sigma> = cons"
+text*[consequence_instance::consequence, level = "Some 3", mcc = "cons"]\<open>aaaaaaaaaaaaa\<close>
+
+ML\<open>
+val s = \<^const_name>\<open>cons\<close>
+val t = s |> Long_Name.base_name
+          |> Symbol_Pos.is_identifier
+val tt = Latex.string s
+val v = \<^const_name>\<open>cons\<close> = s
+\<close>
+ML\<open>
+val s = \<^const_name>\<open>cons\<close>
+val output_name' = Latex.output_name o translate_string (fn "." => "DOT" | s => s)
+val t = output_name' s
+val tt = t  |> Syntax.read_input
+val tttt = t |> Latex.string
+\<close>
+ML\<open>
+val s = "\<open>cons\<^sub>a\<upsilon>\<close>"
+val output_name' = Latex.output_name o translate_string (fn "." => "DOT" | s => s)
+val t = output_name' s
+val tt = t  |> Syntax.read_input
+val ttt = tt  |> Document_Output.output_document ctxt {markdown = true}
+val tttt = t |> Latex.string
+\<close>
+ML\<open>
+val thy = \<^theory>
+\<close>
+ML\<open>
+val cid = "consequence"
+val cid_long = DOF_core.get_onto_class_name_global' cid thy
+val attr_list = [(("level", Position.none), "Some 3"), (("mcc", Position.none), "cons\<^sub>a\<upsilon>")]
+val default_args = DOF_core.get_attribute_defaults cid_long thy
+
+fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) 
+                                            (Symbol.explode (YXML.content_of s)))
+fun toLong n =  #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy))
+val t = default_args |> map (#1 #> Binding.name_of)
+val tt = attr_list |> map (fst #> fst #> YXML.content_of)
+val ttt = toLong "mcc"
+\<close>
+ML\<open>
+val t = Token.make_string ("consequence", Position.none)
+        |> single
+        |> Parse.const
+        |> fst
+val tt = YXML.content_of t
+\<close>
+ML\<open>
+val t = curry op <> Symbol.DEL
+\<close>*)
+
 end

Isabelle_DOF/thys/manual/M_01_Introduction.thy

@@ -17,6 +17,12 @@ theory "M_01_Introduction"
 begin
 (*>*)
 
+ML\<open>
+val t = \<^term>\<open>\<lambda>x. x\<close>
+\<close>
+text\<open>
+\<^term>\<open>\<lambda>x. x\<close>
+\<close>
 chapter*[intro::introduction]\<open> Introduction \<close>  
 text*[introtext::introduction]\<open> 
 The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the most pervasive challenge in the