LaTeX Generator Crash resolved, many little changes...
This commit is contained in:
parent
ed1bef5cbf
commit
9e396b4778
24
Isa_DOF.thy
24
Isa_DOF.thy
|
|
@ -46,7 +46,6 @@ 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>
|
||||
|
|
@ -1532,16 +1531,18 @@ end
|
|||
This code depends on a MODIFIED Isabelle2017 version resulting from applying the files
|
||||
under Isabell_DOF/patches.
|
||||
*)
|
||||
(* REMARK PORT 2018 : transmission of meta-args to LaTeX crude and untested. Can be found in
|
||||
present_token. *)
|
||||
|
||||
|
||||
end
|
||||
|
||||
\<close>
|
||||
ML\<open>
|
||||
val _ = Thy_Output.set_meta_args_parser
|
||||
(fn thy => let val _ = error "META_ARGS_PARSING"
|
||||
in
|
||||
(Scan.optional ( ODL_Command_Parser.attributes
|
||||
>> ODL_LTX_Converter.meta_args_2_string thy) "")
|
||||
end)
|
||||
(fn thy => let val _ = writeln "META_ARGS_PARSING"
|
||||
in (Scan.optional ( ODL_Command_Parser.attributes
|
||||
>> ODL_LTX_Converter.meta_args_2_string thy) "")
|
||||
end);
|
||||
|
||||
\<close>
|
||||
|
||||
|
|
@ -1947,17 +1948,18 @@ end (* struct *)
|
|||
|
||||
ML\<open>Pretty.text_fold; Pretty.unformatted_string_of\<close>
|
||||
ML\<open> (String.concatWith ","); Token.content_of\<close>
|
||||
ML\<open>open Theory\<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) ""))
|
||||
>> 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) ""))
|
||||
>> ODL_LTX_Converter.meta_args_2_string thy) ""));
|
||||
\<close>
|
||||
*)
|
||||
|
||||
ML\<open>
|
||||
Document.state;
|
||||
Session.get_keywords();
|
||||
|
|
|
|||
2
ROOT
2
ROOT
|
|
@ -5,8 +5,8 @@ session "Isabelle_DOF" = "Functional-Automata" +
|
|||
theories
|
||||
Isa_DOF
|
||||
"ontologies/Conceptual"
|
||||
(*
|
||||
"ontologies/CENELEC_50128"
|
||||
(*
|
||||
"ontologies/scholarly_paper"
|
||||
"ontologies/technical_report"
|
||||
"ontologies/mathex_onto"
|
||||
|
|
|
|||
|
|
@ -9,11 +9,11 @@ text\<open>@{theory \<open>Draft.Conceptual\<close>} provides a monitor @{typ M}
|
|||
\<^theory_text>\<open>doc_class\<close>es @{typ M} is enabled for.\<close>
|
||||
open_monitor*[struct::M]
|
||||
|
||||
sectionX[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||
|
||||
textX[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||
|
||||
textX[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
|
||||
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
|
||||
... @{C c1} @{thm "refl"}\<close>
|
||||
|
||||
|
||||
|
|
@ -21,9 +21,9 @@ update_instance*[d::D, a1 := X2]
|
|||
|
||||
text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>}\<close>
|
||||
|
||||
textX[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
|
||||
text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
|
||||
|
||||
textX[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||
text*[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||
|
||||
theorem some_proof : "P" sorry
|
||||
|
||||
|
|
|
|||
|
|
@ -1768,6 +1768,14 @@ Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> s
|
|||
(* this is where antiquotation expansion happens : uses eval_antiquote *)
|
||||
|
||||
*)
|
||||
(* stuff over global environment : *)
|
||||
(*
|
||||
ML\<open> Document.state();\<close>
|
||||
ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
|
||||
Outer_Syntax.command; \<close>
|
||||
ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
|
||||
*)
|
||||
|
||||
|
||||
section\<open>Inner Syntax\<close>
|
||||
text\<open>MORE TO COME\<close>
|
||||
|
|
|
|||
|
|
@ -46,10 +46,9 @@ doc_class M =
|
|||
accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
|
||||
|
||||
|
||||
text\<open>fdgh\<close>
|
||||
|
||||
ML\<open> Document.state();\<close>
|
||||
(*
|
||||
ML\<open> Document.state();\<close>
|
||||
ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
|
||||
Outer_Syntax.command; \<close>
|
||||
ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
|
||||
|
|
|
|||
|
|
@ -401,7 +401,8 @@ val locale =
|
|||
Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
|
||||
Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
|
||||
|
||||
val meta_args_parser_hook = Unsynchronized.ref((fn thy => fn s => ("",s)): theory -> string parser)
|
||||
val meta_args_parser_hook = Synchronized.var "meta args parder hook"
|
||||
((fn thy => fn s => ("",s)): theory -> string parser);
|
||||
|
||||
|
||||
in
|
||||
|
|
@ -410,12 +411,6 @@ type segment = {span: Command_Span.span, command: Toplevel.transition, state: To
|
|||
|
||||
fun present_thy options thy (segments: segment list) =
|
||||
let
|
||||
|
||||
val X = List.concat(map (fn X => Command_Span.content (#span X)) segments)
|
||||
val Y = (String.concatWith "::") (map Token.content_of X)
|
||||
val _ = writeln("present_thy BEGIN:"^Context.theory_name thy^"\n"
|
||||
^Y^
|
||||
"present_thy END:"^Context.theory_name thy^"\n")
|
||||
|
||||
val keywords = Thy_Header.get_keywords thy;
|
||||
|
||||
|
|
@ -444,7 +439,7 @@ fun present_thy options thy (segments: segment list) =
|
|||
Scan.repeat tag --
|
||||
(improper |--
|
||||
(Parse.!!!!
|
||||
( (!meta_args_parser_hook thy)
|
||||
( (Synchronized.value meta_args_parser_hook thy)
|
||||
-- ( (improper -- locale -- improper)
|
||||
|-- (Parse.document_source))
|
||||
--| improper_end)))
|
||||
|
|
@ -457,11 +452,7 @@ fun present_thy options thy (segments: segment list) =
|
|||
Scan.one Token.is_command -- Scan.repeat tag
|
||||
>> (fn ((cmd_mod, cmd), tags) =>
|
||||
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @
|
||||
[(SOME (let val _ = writeln("present_thy ZZZ:"^ Context.theory_name thy
|
||||
^ Token.content_of cmd^"\n")
|
||||
in
|
||||
Token.content_of cmd
|
||||
end, Token.pos_of cmd, tags),
|
||||
[(SOME (Token.content_of cmd, Token.pos_of cmd, tags),
|
||||
(Basic_Token cmd, (markup_false, d)))]));
|
||||
|
||||
val cmt = Scan.peek (fn d =>
|
||||
|
|
@ -509,8 +500,6 @@ fun present_thy options thy (segments: segment list) =
|
|||
>> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
|
||||
make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
|
||||
|
||||
val _ = writeln("HUMPFLEPUMF'")
|
||||
|
||||
val spans = segments
|
||||
|> maps (Command_Span.content o #span)
|
||||
|> drop_suffix Token.is_space
|
||||
|
|
@ -534,8 +523,6 @@ fun present_thy options thy (segments: segment list) =
|
|||
fun present _ [] = I
|
||||
| present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
|
||||
|
||||
val _ = writeln("HUMPFLEPUMF''"^Context.theory_name thy)
|
||||
|
||||
in
|
||||
if length command_results = length spans then
|
||||
((NONE, []), NONE, true, [], (I, I))
|
||||
|
|
@ -546,7 +533,7 @@ fun present_thy options thy (segments: segment list) =
|
|||
end;
|
||||
|
||||
fun set_meta_args_parser f = let val _ = writeln "Meta-args parser set to new value"
|
||||
in (meta_args_parser_hook:= f) end
|
||||
in (Synchronized.assign meta_args_parser_hook f) end
|
||||
|
||||
end;
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue