Again Unsyncref; changes in thy_output in order to tackle duplicate meta_args_problem

Isa_DOF.thy

@@ -1475,7 +1475,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
         val cid_txt  = "type = " ^ (enclose "{" "}" cid_long);
 
 
-        fun ltx_of_term _ _ (((Const ("List.list.Cons", t1) $  (Const ("String.Char", t2 ) $ t))) $ t') 
+        fun (* ltx_of_term _ _ (((Const ("List.list.Cons", t1) $  (Const ("String.Char", t2 ) $ t))) $ t') 
                            = (HOLogic.dest_string (((Const ("List.list.Cons", t1) $  (Const ("String.Char", t2 ) $ t))) $ t'))
           | ltx_of_term _ _ (Const ("List.list.Nil", _)) = ""
           | ltx_of_term _ _ (@{term "numeral :: _ \<Rightarrow> _"} $ t) = Int.toString(HOLogic.dest_numeral t)
@@ -1487,7 +1487,7 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
                                                in if encl then enclose "{" "}" inner else inner end
           | ltx_of_term _ _ (Const ("Option.option.None", _)) = ""
           | ltx_of_term ctxt _ (Const ("Option.option.Some", _)$t) = ltx_of_term ctxt true t
-          | ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t)
+          | *)ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t)
 
 
         fun ltx_of_term_dbg ctx encl term  = let 
@@ -1637,11 +1637,6 @@ ML\<open>
   Latex.output_text: Latex.text list -> string;
 \<close>
 
-ML\<open>
-   Pretty.text;
-   Pretty.str;
-   Pretty.block_enclose;
-\<close>
 
 ML\<open>
 structure OntoLinkParser = 
@@ -1689,7 +1684,7 @@ 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 _ = writeln ("ZZZ" ^ Input.source_content src ^ "::2::" ^ 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) 
@@ -1945,19 +1940,16 @@ val _ =
 end (* struct *)
 \<close>  
 
+(*
+ML\<open>
+   Pretty.text;
+   Pretty.str;
+   Pretty.block_enclose;
+\<close>
+
 ML\<open>Pretty.text_fold; Pretty.unformatted_string_of\<close>
 ML\<open> (String.concatWith ","); Token.content_of\<close>
 
-(*
-ML\<open>
-val _ = Thy_Output.set_meta_args_parser
-                       (fn thy => (Scan.optional (   ODL_Command_Parser.attributes 
-                                                  >> ODL_LTX_Converter.meta_args_2_string thy) ""));
-val _ = Thy_Output.set_meta_args_parser
-                       (fn thy => (Scan.optional (   ODL_Command_Parser.attributes 
-                                                  >> ODL_LTX_Converter.meta_args_2_string thy) ""));
-\<close>
-*)
 
 ML\<open>
  Document.state;
@@ -1971,5 +1963,6 @@ ML\<open>
  Parse.!!!;
 
 \<close>
+*)
 
 end

ROOT

@@ -6,10 +6,7 @@ session "Isabelle_DOF" = "Functional-Automata" +
     Isa_DOF
     "ontologies/Conceptual"
     "ontologies/CENELEC_50128"
-    (*
     "ontologies/scholarly_paper"
     "ontologies/technical_report"
     "ontologies/mathex_onto"
-    *)
-
 

examples/cenelec/mini_odo/ROOT

@@ -1,8 +1,5 @@
 session "mini_odo" = "Isabelle_DOF" +
   options [document = pdf, document_output = "output"]
-  theories [document = false]
-    (* Foo *)
-    (* Bar *)
   theories
     "mini_odo"
   document_files

patches/thy_output.ML

@@ -194,11 +194,11 @@ fun present_token ctxt tok =
     Ignore_Token => []
   | Basic_Token tok => output_token ctxt tok
   | Markup_Token (cmd, meta_args, source) =>
-      Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ meta_args ^ "{") "%\n}\n"
+      Latex.enclose_body ("%\n\\isamarkup" ^ cmd (* ^ meta_args *) ^ "{") "%\n}\n"
         (output_document ctxt {markdown = false} source)
   | Markup_Env_Token (cmd, meta_args, source) =>
       [Latex.environment_block
-         ("isamarkup" ^ cmd ^ meta_args)
+         ("isamarkup" ^ cmd (* ^ meta_args*))
          (Latex.string meta_args :: output_document ctxt {markdown = true} source)]
   | Raw_Token source =>
       Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
@@ -366,7 +366,11 @@ val locale =
   Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
     Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
 
-val meta_args_parser_hook =  Synchronized.var "meta args parder hook" 
+(*
+val meta_args_parser_hook =  Synchronized.var "meta args parser hook" 
+                             ((fn thy => fn s => ("",s)): theory -> string parser);
+*)
+val meta_args_parser_hook =  Unsynchronized.ref 
                              ((fn thy => fn s => ("",s)): theory -> string parser);
 
 
@@ -392,7 +396,7 @@ fun present_thy options thy (segments: segment list) =
       Scan.repeat tag --
       (improper |--
       (Parse.!!!! 
-      (  (Synchronized.value meta_args_parser_hook thy)
+      (  (!meta_args_parser_hook thy)
          -- (  (improper -- locale -- improper) 
          |-- (Parse.document_source)) 
          --| improper_end)))
@@ -479,8 +483,13 @@ fun present_thy options thy (segments: segment list) =
     else error "Messed-up outer syntax for presentation"
   end;
 
+(*
 fun set_meta_args_parser f = let val _ = writeln "Meta-args parser set to new value" 
-                             in  (Synchronized.assign meta_args_parser_hook  f) end
+                             in  (Unsynchronized.assign meta_args_parser_hook  f) end
+*)
+fun set_meta_args_parser f = let val _ = writeln "Meta-args parser set to new value" 
+                             in  ( meta_args_parser_hook := f) end
+
 
 end;