Experiments with the LaTeX generator

Isa_COL.thy

@@ -5,7 +5,7 @@ text\<open> Offering
 \<^item> 
 \<^item> LaTeX support. \<close> 
   
-  
+ 
 theory Isa_COL   
   imports  Isa_DOF  
 begin

Isa_DOF.thy

@@ -46,7 +46,7 @@ begin
 
 
 text\<open> @{footnote \<open>sdf\<close>}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close> 
-
+ML_file "patches/thy_output.ML";
 
 section\<open>Primitive Markup Generators\<close>
 ML\<open>
@@ -109,7 +109,7 @@ fun holstring_to_bstring ctxt (x:string) : bstring  =
 
 section\<open> A HomeGrown Document Type Management (the ''Model'') \<close>
   
-ML\<open>
+ML\<open> 
 structure DOF_core = 
 struct
 
@@ -1534,8 +1534,11 @@ end
  *)
 
 val _ = Thy_Output.set_meta_args_parser 
-                       (fn thy => (Scan.optional (   ODL_Command_Parser.attributes 
-                                                  >> meta_args_2_string thy) "")) 
+                       (fn thy => let val _ = writeln "META_ARGS_PARSING"
+                                  in
+                                  (Scan.optional (   ODL_Command_Parser.attributes 
+                                                  >> meta_args_2_string thy) "")
+                                  end) 
 
 
 end
@@ -1685,10 +1688,10 @@ val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input)
 
 
 fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked = x, define = y}, src ) = 
-            let val _ = check_and_mark ctxt cid_decl  
+            let val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ cid_decl)
+                val _ = check_and_mark ctxt cid_decl  
                           ({strict_checking = not x}) 
-                          (Input.pos_of src) (Input.source_content src)
-                val _ = writeln ("ZZZ" ^ Input.source_content src ^ "::" ^ cid_decl)
+                          (Input.pos_of src) (Input.source_content src) 
             in  (if y then Latex.enclose_block "\\label{" "}" 
                       else Latex.enclose_block "\\autoref{" "}")
                 [Latex.string (Input.source_content src)] 

ROOT

@@ -4,8 +4,8 @@ session "Isabelle_DOF" = "Functional-Automata" +
     "Regular-Sets"
   theories
     Isa_DOF
-    "ontologies/CENELEC_50128"
     "ontologies/Conceptual"
+    "ontologies/CENELEC_50128"
     "ontologies/scholarly_paper"
     "ontologies/technical_report"
     "ontologies/mathex_onto"

ROOTS

@@ -1 +0,0 @@
-examples

examples/conceptual/Attributes.thy

@@ -16,7 +16,7 @@ val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, moni
 Symtab.dest docitem_tab;
 Symtab.dest docclass_tab;
 \<close>
-
+ 
 ML\<open>
 fun fac x = if x = 0 then 1 else x * (fac(x -1));
 fac 3;

examples/conceptual/Concept_Example.thy

@@ -14,7 +14,7 @@ section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ...  \<close>
 
 text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, 
-                         ... @{docitem c1} @{thm "refl"}\<close>
+                         ... @{docitem "c1"} @{thm "refl"} \<close>
 
 
 update_instance*[d::D, a1 := X2]

ontologies/Conceptual.thy

@@ -54,4 +54,4 @@ text*[sdfg] {* fg @{thm refl}*}
 text*[xxxy] {* dd @{docitem \<open>sdfg\<close>}  @{thm refl}*}    
 
 
-end     
+end     

patches/thy_output.ML

@@ -174,12 +174,21 @@ val is_black_comment = Token.is_formal_comment;
 
 (* presentation tokens *)
 
+(* orig Isabelle 2018
 datatype token =
     Ignore_Token
   | Basic_Token of Token.T
   | Markup_Token of string * Input.source
   | Markup_Env_Token of string * Input.source
   | Raw_Token of Input.source;
+*)
+
+datatype token =
+    Ignore_Token
+  | Basic_Token of Token.T
+  | Markup_Token of string * string * Input.source
+  | Markup_Env_Token of string * string * Input.source
+  | Raw_Token of Input.source;
 
 fun basic_token pred (Basic_Token tok) = pred tok
   | basic_token _ _ = false;
@@ -189,6 +198,7 @@ val white_comment_token = basic_token is_white_comment;
 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
 
+(* orig Isabelle 2018
 fun present_token ctxt tok =
   (case tok of
     Ignore_Token => []
@@ -201,6 +211,21 @@ fun present_token ctxt tok =
   | Raw_Token source =>
       Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
 
+*)
+
+(* modified by bu: added meta_args; currently ignored*) 
+fun present_token ctxt tok =
+  (case tok of
+    Ignore_Token => []
+  | Basic_Token tok => output_token ctxt tok
+  | Markup_Token (cmd, meta_args, source) =>
+      Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
+        (output_document ctxt {markdown = false} source)
+  | Markup_Env_Token (cmd, meta_args,source) =>
+      [Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)]
+  | Raw_Token source =>
+      Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
+
 
 (* command spans *)
 
@@ -381,6 +406,7 @@ fun present_thy options thy (segments: segment list) =
     val ignored = Scan.state --| ignore
       >> (fn d => (NONE, (Ignore_Token, ("", d))));
 
+    (* orig Isabelle 2018
     fun markup pred mk flag = Scan.peek (fn d =>
       improper |--
         Parse.position (Scan.one (fn tok =>
@@ -390,6 +416,22 @@ fun present_thy options thy (segments: segment list) =
       >> (fn (((tok, pos'), tags), source) =>
         let val name = Token.content_of tok
         in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end));
+    *)
+
+    fun markup pred mk flag = Scan.peek (fn d =>
+      improper |--
+        Parse.position (Scan.one (fn tok =>  Token.is_command tok andalso 
+                                             pred keywords (Token.content_of tok))) --
+      Scan.repeat tag --
+      (improper |--
+      (Parse.!!!! 
+      (  (!meta_args_parser_hook thy)
+         -- (  (improper -- locale -- improper) 
+         |-- (Parse.document_source)) 
+         --| improper_end)))
+      >> (fn (((tok, pos'), tags), (meta_args,source)) =>
+        let val name = Token.content_of tok
+        in (SOME (name, pos', tags), (mk (name, meta_args, source), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
       Scan.optional (Scan.one Token.is_command_modifier ::: improper) [] --
@@ -405,7 +447,7 @@ fun present_thy options thy (segments: segment list) =
     val cmt = Scan.peek (fn d =>
       (Parse.$$$ "--" || Parse.$$$ Symbol.comment) |--
         Parse.!!!! (improper |-- Parse.document_source) >>
-        (fn source => (NONE, (Markup_Token ("cmt", source), ("", d)))));
+        (fn source => (NONE, (Markup_Token ("cmt", "", source), ("", d)))));
 
 
     val other = Scan.peek (fn d =>
@@ -415,7 +457,7 @@ fun present_thy options thy (segments: segment list) =
       (ignored ||
         markup Keyword.is_document_heading Markup_Token markup_true ||
         markup Keyword.is_document_body Markup_Env_Token markup_true ||
-        markup Keyword.is_document_raw (Raw_Token o #2) "") >> single ||
+        markup Keyword.is_document_raw (Raw_Token o #3) "") >> single ||
       command ||
       (cmt || other) >> single;