From ec49f4596634b9b37c9677898c2b153da04c60f0 Mon Sep 17 00:00:00 2001 From: Makarius Date: Sat, 18 Dec 2021 23:06:51 +0100 Subject: [PATCH 01/11] Adaptations for Isabelle2021-1. --- examples/CENELEC_50128/mini_odo/ROOT | 2 +- examples/math_exam/MathExam/ROOT | 2 +- .../2018-cicm-isabelle_dof-applications/ROOT | 3 +- examples/scholarly_paper/2020-iFM-CSP/ROOT | 2 +- examples/scholarly_paper/2021-ITP-PMTI/ROOT | 2 +- .../technical_report/Isabelle_DOF-Manual/ROOT | 3 +- .../TR_my_commented_isabelle/ROOT | 3 +- src/DOF/Isa_COL.thy | 85 ++-- src/DOF/Isa_DOF.thy | 365 ++++++++---------- src/ROOT | 2 +- .../scholarly_paper/scholarly_paper.thy | 94 ++--- src/patches/present_theory | 36 ++ src/scripts/build_lib.sh | 11 +- 13 files changed, 276 insertions(+), 334 deletions(-) create mode 100644 src/patches/present_theory diff --git a/examples/CENELEC_50128/mini_odo/ROOT b/examples/CENELEC_50128/mini_odo/ROOT index d7d13755..34c7fe80 100755 --- a/examples/CENELEC_50128/mini_odo/ROOT +++ b/examples/CENELEC_50128/mini_odo/ROOT @@ -1,5 +1,5 @@ session "mini_odo" = "Isabelle_DOF" + - options [document = pdf, document_output = "output"] + options [document = pdf, document_output = "output", document_build = "build"] theories "mini_odo" document_files diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT index 9f5e87ee..21668d02 100755 --- a/examples/math_exam/MathExam/ROOT +++ b/examples/math_exam/MathExam/ROOT @@ -1,5 +1,5 @@ session "MathExam" = "Isabelle_DOF" + - options [document = pdf, document_output = "output"] + options [document = pdf, document_output = "output", document_build = "build"] theories MathExam document_files diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT index 2e8e931b..a3017a2b 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT @@ -1,5 +1,6 @@ session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", quick_and_dirty = true] + options [document = pdf, document_output = "output", document_build = "build", + quick_and_dirty = true] theories IsaDofApplications document_files diff --git a/examples/scholarly_paper/2020-iFM-CSP/ROOT b/examples/scholarly_paper/2020-iFM-CSP/ROOT index 1445bb26..f5388f29 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/ROOT +++ b/examples/scholarly_paper/2020-iFM-CSP/ROOT @@ -1,5 +1,5 @@ session "2020-iFM-csp" = "Isabelle_DOF" + - options [document = pdf, document_output = "output"] + options [document = pdf, document_output = "output", document_build = "build"] theories "paper" document_files diff --git a/examples/scholarly_paper/2021-ITP-PMTI/ROOT b/examples/scholarly_paper/2021-ITP-PMTI/ROOT index a0e6c427..0cfda600 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/ROOT +++ b/examples/scholarly_paper/2021-ITP-PMTI/ROOT @@ -1,5 +1,5 @@ session "2021-ITP-PMTI" = "Isabelle_DOF" + - options [document = pdf, document_output = "output"] + options [document = pdf, document_output = "output", document_build = "build"] theories "paper" document_files diff --git a/examples/technical_report/Isabelle_DOF-Manual/ROOT b/examples/technical_report/Isabelle_DOF-Manual/ROOT index cdce3754..6e759f0e 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/ROOT +++ b/examples/technical_report/Isabelle_DOF-Manual/ROOT @@ -1,5 +1,6 @@ session "Isabelle_DOF-Manual" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", quick_and_dirty = true] + options [document = pdf, document_output = "output", document_build = "build", + quick_and_dirty = true] theories "Isabelle_DOF-Manual" document_files diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index 5a8afa7a..ffc5b145 100755 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -1,5 +1,6 @@ session "TR_MyCommentedIsabelle" = "Isabelle_DOF" + - options [document = pdf, document_output = "output",quick_and_dirty = true] + options [document = pdf, document_output = "output", document_build = "build", + quick_and_dirty = true] theories "TR_MyCommentedIsabelle" document_files diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index f6273f3d..67f66838 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -106,60 +106,32 @@ in fun enriched_formal_statement_command ncid (S: (string * string) list) = let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ (("formal_results",@{here}),"([]::thm list)")::doc_attrs - in fn md => fn margs => fn thy => + in fn margs => fn thy => gen_enriched_document_cmd {inline=true} - (transform_cid thy ncid) transform_attr md margs thy + (transform_cid thy ncid) transform_attr margs thy end; fun enriched_document_cmd_exp ncid (S: (string * string) list) = (* expands ncid into supertype-check. *) let fun transform_attr attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ attrs - in fn md => fn margs => fn thy => - gen_enriched_document_cmd {inline=true} (transform_cid thy ncid) transform_attr md margs thy + in fn margs => fn thy => + gen_enriched_document_cmd {inline=true} (transform_cid thy ncid) transform_attr margs thy end; end (* local *) -val _ = - Outer_Syntax.command ("title*", @{here}) "section heading" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_text_element_cmd NONE {markdown = false} ))) ; +fun heading_command (name, pos) descr level = + ODL_Command_Parser.document_command (name, pos) descr + {markdown = false, body = true} (enriched_text_element_cmd level); -val _ = - Outer_Syntax.command ("subtitle*", @{here}) "section heading" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_text_element_cmd NONE {markdown = false} ))); - -val _ = - Outer_Syntax.command ("chapter*", @{here}) "section heading" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 0)) {markdown = false} ))); - -val _ = - Outer_Syntax.command ("section*", @{here}) "section heading" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 1)) {markdown = false} ))); - - -val _ = - Outer_Syntax.command ("subsection*", @{here}) "subsection heading" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 2)) {markdown = false} ))); - -val _ = - Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 3)) {markdown = false} ))); - -val _ = - Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 4)) {markdown = false} ))); - -val _ = - Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 5)) {markdown = false} ))); +val _ = heading_command ("title*", @{here}) "section heading" NONE; +val _ = heading_command ("subtitle*", @{here}) "section heading" NONE; +val _ = heading_command ("chapter*", @{here}) "section heading" (SOME (SOME 0)); +val _ = heading_command ("section*", @{here}) "section heading" (SOME (SOME 1)); +val _ = heading_command ("subsection*", @{here}) "subsection heading" (SOME (SOME 2)); +val _ = heading_command ("subsubsection*", @{here}) "subsubsection heading" (SOME (SOME 3)); +val _ = heading_command ("paragraph*", @{here}) "paragraph heading" (SOME (SOME 4)); +val _ = heading_command ("subparagraph*", @{here}) "subparagraph heading" (SOME (SOME 5)); end end @@ -206,24 +178,13 @@ print_doc_classes subsection\Ontological Macros\ -ML\ local open ODL_Command_Parser in +ML\ (* *********************************************************************** *) (* Ontological Macro Command Support *) (* *********************************************************************** *) -val _ = - Outer_Syntax.command ("figure*", @{here}) "figure" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (Onto_Macros.enriched_text_element_cmd NONE {markdown = false} ))); - -val _ = - Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (Onto_Macros.enriched_text_element_cmd NONE {markdown = false} ))); - - - -end +val _ = Onto_Macros.heading_command ("figure*", @{here}) "figure" NONE; +val _ = Onto_Macros.heading_command ("side_by_side_figure*", @{here}) "multiple figures" NONE; \ (*<*) @@ -247,22 +208,22 @@ section\Tables\ ML\ local -fun mk_line st1 st2 [a] = [a @ [Latex.string st2]] - |mk_line st1 st2 (a::S) = [a @ [Latex.string st1]] @ mk_line st1 st2 S; +fun mk_line st1 st2 [a] = [a @ Latex.string st2] + |mk_line st1 st2 (a::S) = [a @ Latex.string st1] @ mk_line st1 st2 S; fun table_antiquotation name = - Thy_Output.antiquotation_raw_embedded name + Document_Output.antiquotation_raw_embedded name (Scan.repeat1(Scan.repeat1(Scan.lift Args.cartouche_input))) (fn ctxt => (fn content:Input.source list list => let fun check _ = () (* ToDo *) val _ = check content in content - |> (map(map (Thy_Output.output_document ctxt {markdown = false}) + |> (map(map (Document_Output.output_document ctxt {markdown = false}) #> mk_line "&" "\\\\" #> List.concat ) #> List.concat) - |> Latex.enclose_block "\\table[allerhandquatsch]{" "}" + |> XML.enclose "\\table[allerhandquatsch]{" "}" end ) ); diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 6826442e..5b168928 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -69,9 +69,7 @@ val instances_of_suffixN = "_instances" (* derived from: theory_markup *) fun docref_markup_gen refN def name id pos = if id = 0 then Markup.empty - else - Markup.properties (Position.entity_properties_of def id pos) - (Markup.entity refN name); (* or better store the thy-name as property ? ? ? *) + else Position.make_entity_markup {def = def} id refN (name, pos); (* or better store the thy-name as property ? ? ? *) val docref_markup = docref_markup_gen docrefN @@ -1194,8 +1192,6 @@ fun document_command markdown (loc, txt) = *) - - ML\ structure ODL_Command_Parser = struct @@ -1205,7 +1201,6 @@ type meta_args_t = (((string * Position.T) * (string * Position.T) option) * ((string * Position.T) * string) list) -val semi = Scan.option (Parse.$$$ ";"); val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore); val improper = Scan.many is_improper; (* parses white-space and comments *) @@ -1317,7 +1312,8 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) let val cid_ty = cid_2_cidType cid_long thy val generalize_term = Term.map_types (generalize_typ 0) fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t - fun instantiate_term S t = Term_Subst.map_types_same (Term_Subst.instantiateT S) (t) + fun instantiate_term S t = + Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S)) (t) fun read_assn (lhs, pos:Position.T, opr, rhs) term = let val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy val (ln,lnt,lnu,lnut) = case info_opt of @@ -1484,74 +1480,6 @@ fun update_instance_command (((oid:string,pos),cid_pos), end -(* old version : -fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transform - markdown - (((((oid,pos),cid_pos), doc_attrs) : meta_args_t, - xstring_opt:(xstring * Position.T) option), - toks:Input.source) - : theory -> theory = - let val toplvl = Toplevel.theory_toplevel - fun check thy = let val ctxt = Toplevel.presentation_context (toplvl thy); - val pos = Input.pos_of toks; - val _ = Context_Position.reports ctxt - [(pos, Markup.language_document(Input.is_delimited toks)), - (pos, Markup.plain_text)]; - in thy end - - in - (* ... level-attribute information management *) - ( create_and_check_docitem {is_monitor=false} - {is_inline=is_inline} - oid pos (cid_transform cid_pos) - (attr_transform doc_attrs) - (* checking and markup generation *) - #> check ) - (* Thanks Frederic Tuong for the hints concerning toplevel ! ! ! *) - end; -*) - -fun gen_enriched_document_cmd {inline=is_inline} cid_transform attr_transform - markdown - (((((oid,pos),cid_pos), doc_attrs) : meta_args_t, - xstring_opt:(xstring * Position.T) option), - toks:Input.source) - : theory -> theory = - let val toplvl = Toplevel.theory_toplevel - - (* as side-effect, generates markup *) - fun check_n_tex_text thy = let val ctxt = Toplevel.presentation_context (toplvl thy); - val pos = Input.pos_of toks; - val _ = Context_Position.reports ctxt - [(pos, Markup.language_document (Input.is_delimited toks)), - (pos, Markup.plain_text)]; - - val text = Thy_Output.output_document - (Proof_Context.init_global thy) - markdown toks - - (* val file = {path = Path.make [oid ^ "_snippet.tex"], - pos = @{here}, - content = Latex.output_text text} - - val _ = Generated_Files.write_file (Path.make ["latex_test"]) - file - val _ = writeln (Latex.output_text text) *) - in thy end - - (* ... generating the level-attribute syntax *) - in - (* ... level-attribute information management *) - ( create_and_check_docitem - {is_monitor = false} {is_inline = is_inline} - oid pos (cid_transform cid_pos) (attr_transform doc_attrs) - (* checking and markup generation *) - #> check_n_tex_text ) - (* Thanks Frederic Tuong for the hints concerning toplevel ! ! ! *) - end; - - - (* General criticism : attributes like "level" were treated here in the kernel instead of dragging them out into the COL -- bu *) @@ -1601,8 +1529,115 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos), |> delete_monitor_entry end -(* Core Command Definitions *) +fun meta_args_2_latex thy ((((lab, _), cid_opt), attr_list) : meta_args_t) = + (* for the moment naive, i.e. without textual normalization of + attribute names and adapted term printing *) + let val l = "label = "^ (enclose "{" "}" lab) + (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *) + val cid_long = case cid_opt of + NONE => (case DOF_core.get_object_global lab thy of + NONE => DOF_core.default_cid + | SOME X => #cid X) + | SOME(cid,_) => DOF_core.parse_cid_global thy cid + (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *) + val cid_txt = "type = " ^ (enclose "{" "}" cid_long); + + fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) + = HOLogic.dest_string (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) + | ltx_of_term _ _ (Const ("List.list.Nil", _)) = "" + | ltx_of_term _ _ (@{term "numeral :: _ \ _"} $ t) = Int.toString(HOLogic.dest_numeral t) + | ltx_of_term ctx encl ((Const ("List.list.Cons", _) $ t1) $ t2) = + let val inner = (case t2 of + Const ("List.list.Nil", _) => (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 ("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) + + + fun ltx_of_term_dbg ctx encl term = let + val t_str = ML_Syntax.print_term term + handle (TERM _) => "Exception TERM in ltx_of_term_dbg (print_term)" + val ltx = ltx_of_term ctx encl term + val _ = writeln(""^(Sledgehammer_Util.hackish_string_of_term ctx term)^"") + val _ = writeln(""^ltx^"") + val _ = writeln(""^t_str^"") + in ltx end + + + fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) + (Symbol.explode (YXML.content_of s))) + fun ltx_of_markup ctxt s = let + val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s + val str_of_term = ltx_of_term ctxt true term + handle _ => "Exception in ltx_of_term" + in + str_of_term + end + fun toLong n = #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy)) + + val ctxt = Proof_Context.init_global thy + val actual_args = map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs)) + attr_list + 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) + + val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a) + (map (fn (c,_) => c) actual_args))) default_args + val str_args = map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs)) + (actual_args@default_args_filtered) + 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), "}"])) + end + +(* level-attribute information management *) +fun gen_enriched_document_cmd {inline} cid_transform attr_transform + ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) : theory -> theory = + create_and_check_docitem {is_monitor = false} {is_inline = inline} + oid pos (cid_transform cid_pos) (attr_transform doc_attrs); + + +(* markup reports and document output *) + +(* {markdown = true} sets the parsing process such that in the text-core + markdown elements are accepted. *) + +fun document_output {markdown: bool, markup: Latex.text -> Latex.text} meta_args text ctxt = + let + val thy = Proof_Context.theory_of ctxt; + val _ = Context_Position.reports ctxt (Document_Output.document_reports text); + val output_meta = meta_args_2_latex thy meta_args; + val output_text = Document_Output.output_document ctxt {markdown = markdown} text; + in markup (output_meta @ output_text) end; + +fun document_output_reports name {markdown, body} meta_args text ctxt = + let + val pos = Input.pos_of text; + val _ = + Context_Position.reports ctxt + [(pos, Markup.language_document (Input.is_delimited text)), + (pos, Markup.plain_text)]; + fun markup xml = + let val m = if body then Markup.latex_body else Markup.latex_heading + in [XML.Elem (m (Latex.output_name name), xml)] end; + in document_output {markdown = markdown, markup = markup} meta_args text ctxt end; + +fun document_command (name, pos) descr mark cmd = + Outer_Syntax.command (name, pos) descr + (attributes -- Parse.document_source >> + (fn (meta_args, text) => + Toplevel.present_theory (cmd meta_args) + (Toplevel.presentation_context #> document_output_reports name mark meta_args text))); + + + +(* Core Command Definitions *) val _ = Outer_Syntax.command @{command_keyword "open_monitor*"} @@ -1620,11 +1655,9 @@ val _ = "update meta-attributes of an instance of a document class" (attributes_upd >> (Toplevel.theory o update_instance_command)); - val _ = - Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" - (attributes -- Parse.opt_target -- Parse.document_source - >> (Toplevel.theory o (gen_enriched_document_cmd {inline=true} I I {markdown = true} ))); + document_command ("text*", @{here}) "formal comment (primary style)" + {markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I); (* term* command uses the same code as term command @@ -1661,10 +1694,9 @@ Outer_Syntax.command \<^command_keyword>\term*\ "read and print ter (* This is just a stub at present *) val _ = - Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro" - (attributes -- Parse.opt_target -- Parse.document_source - >> (Toplevel.theory o (gen_enriched_document_cmd {inline=false} (* declare as macro *) - I I {markdown = true} ))); + document_command ("text-macro*", @{here}) "formal comment macro" + {markdown = true, body = true} + (gen_enriched_document_cmd {inline=false} (* declare as macro *) I I); val _ = Outer_Syntax.command @{command_keyword "declare_reference*"} @@ -1767,10 +1799,10 @@ val _ = (opt_evaluator -- opt_modes -- Parse.term >> pass_trans_to_value_cmd); val _ = Theory.setup - (Thy_Output.antiquotation_pretty_source_embedded \<^binding>\value*\ + (Document_Output.antiquotation_pretty_source_embedded \<^binding>\value*\ (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term) (fn ctxt => fn ((name, style), t) => - Thy_Output.pretty_term ctxt (style (value_select name ctxt t))) + Document_Output.pretty_term ctxt (style (value_select name ctxt t))) #> add_evaluator (\<^binding>\simp\, Code_Simp.dynamic_value) #> snd #> add_evaluator (\<^binding>\nbe\, Nbe.dynamic_value) #> snd #> add_evaluator (\<^binding>\code\, Code_Evaluation.dynamic_value_strict) #> snd); @@ -1778,98 +1810,14 @@ val _ = Theory.setup end; \ -ML\ -structure ODL_LTX_Converter = -struct -fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parser.meta_args_t) = - (* for the moment naive, i.e. without textual normalization of - attribute names and adapted term printing *) - let val l = "label = "^ (enclose "{" "}" lab) - (* val _ = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *) - val cid_long = case cid_opt of - NONE => (case DOF_core.get_object_global lab thy of - NONE => DOF_core.default_cid - | SOME X => #cid X) - | SOME(cid,_) => DOF_core.parse_cid_global thy cid - (* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *) - val cid_txt = "type = " ^ (enclose "{" "}" cid_long); - - fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) - = HOLogic.dest_string (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) - | ltx_of_term _ _ (Const ("List.list.Nil", _)) = "" - | ltx_of_term _ _ (@{term "numeral :: _ \ _"} $ t) = Int.toString(HOLogic.dest_numeral t) - | ltx_of_term ctx encl ((Const ("List.list.Cons", _) $ t1) $ t2) = - let val inner = (case t2 of - Const ("List.list.Nil", _) => (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 ("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) - - - fun ltx_of_term_dbg ctx encl term = let - val t_str = ML_Syntax.print_term term - handle (TERM _) => "Exception TERM in ltx_of_term_dbg (print_term)" - val ltx = ltx_of_term ctx encl term - val _ = writeln(""^(Sledgehammer_Util.hackish_string_of_term ctx term)^"") - val _ = writeln(""^ltx^"") - val _ = writeln(""^t_str^"") - in ltx end - - - fun markup2string s = String.concat (List.filter (fn c => c <> Symbol.DEL) - (Symbol.explode (YXML.content_of s))) - fun ltx_of_markup ctxt s = let - val term = (Syntax.check_term ctxt o Syntax.parse_term ctxt) s - val str_of_term = ltx_of_term ctxt true term - handle _ => "Exception in ltx_of_term" - in - str_of_term - end - fun toLong n = #long_name(the(DOF_core.get_attribute_info cid_long (markup2string n) thy)) - - val ctxt = Proof_Context.init_global thy - val actual_args = map (fn ((lhs,_),rhs) => (toLong lhs, ltx_of_markup ctxt rhs)) - attr_list - 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) - - val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a) - (map (fn (c,_) => c) actual_args))) default_args - val str_args = map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs)) - (actual_args@default_args_filtered) - val label_and_type = String.concat [ l, ",", cid_txt] - val str_args = label_and_type::str_args - in - (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"])) -end - -end -\ - - -ML\ (* Setting in thy_output.ML a parser for the syntactic handling of the meta-informations of - text elements - so text*[m]\ ... dfgdfg .... \ *) - -val _ = Thy_Output.set_meta_args_parser - (fn thy => (Scan.optional (Document_Source.improper - |-- ODL_Command_Parser.attributes - >> ODL_LTX_Converter.meta_args_2_string thy) "")); \ - - - - section\ Syntax for Ontological Antiquotations (the '' View'' Part II) \ ML\ structure OntoLinkParser = struct -val basic_entity = Thy_Output.antiquotation_pretty_source +val basic_entity = Document_Output.antiquotation_pretty_source : binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_req} pos name = @@ -1921,20 +1869,19 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src val inline = Config.get ctxt Document_Antiquotation.thy_output_display val _ = check_and_mark ctxt cid_decl {strict_checking = not unchecked} {inline = inline} pos str - val enc = Latex.enclose_block in (case (define,inline) of - (true,false) => enc("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}] {")"}" - |(false,false)=> enc("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}] {")"}" - |(true,true) => enc("\\csname isaDof.macroDef\\endcsname[type={"^cid_decl^"}]{")"}" - |(false,true) => enc("\\csname isaDof.macroExp\\endcsname[type={"^cid_decl^"}]{")"}" + (true,false) => XML.enclose("\\csname isaDof.label\\endcsname[type={"^cid_decl^"}] {")"}" + |(false,false)=> XML.enclose("\\csname isaDof.ref\\endcsname[type={"^cid_decl^"}] {")"}" + |(true,true) => XML.enclose("\\csname isaDof.macroDef\\endcsname[type={"^cid_decl^"}]{")"}" + |(false,true) => XML.enclose("\\csname isaDof.macroExp\\endcsname[type={"^cid_decl^"}]{")"}" ) - [Latex.text (Input.source_content src)] + (Latex.text (Input.source_content src)) end fun docitem_antiquotation bind cid = - Thy_Output.antiquotation_raw bind docitem_antiquotation_parser + Document_Output.antiquotation_raw bind docitem_antiquotation_parser (pretty_docitem_antiquotation_generic cid); @@ -1973,7 +1920,7 @@ ML\ structure AttributeAccess = struct -val basic_entity = Thy_Output.antiquotation_pretty_source +val basic_entity = Document_Output.antiquotation_pretty_source : binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; fun symbex_attr_access0 ctxt proj_term term = @@ -2061,13 +2008,13 @@ fun compute_cid_repr ctxt cid pos = local fun pretty_attr_access_style ctxt (style, ((oid,pos),(attr,pos'))) = - Thy_Output.pretty_term ctxt (style (compute_attr_access (Context.Proof ctxt) + Document_Output.pretty_term ctxt (style (compute_attr_access (Context.Proof ctxt) attr oid pos pos')); fun pretty_trace_style ctxt (style, (oid,pos)) = - Thy_Output.pretty_term ctxt (style (compute_attr_access (Context.Proof ctxt) + Document_Output.pretty_term ctxt (style (compute_attr_access (Context.Proof ctxt) "trace" oid pos pos)); fun pretty_cid_style ctxt (style, (cid,pos)) = - Thy_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos)); + Document_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos)); in val _ = Theory.setup @@ -2087,7 +2034,7 @@ end text\ Note that the functions \<^verbatim>\basic_entities\ and \<^verbatim>\basic_entity\ in @{ML_structure AttributeAccess} are copied from - @{file "$ISABELLE_HOME/src/Pure/Thy/thy_output.ML"} \ + @{file "$ISABELLE_HOME/src/Pure/Thy/document_output.ML"} \ section\ Syntax for Ontologies (the '' View'' Part III) \ @@ -2128,7 +2075,15 @@ fun read_fields raw_fields ctxt = val trace_attr = ((Binding.make("trace",@{here}), "(doc_class rexp \ string) list",Mixfix.NoSyn), SOME "[]"): ((binding * string * mixfix) * string option) -fun def_cmd (decl, spec, prems, params) = #2 oo Specification.definition' decl params prems spec +fun def_cmd (decl, spec, prems, params) lthy = + let + val ((lhs as Free (x, T), _), lthy') = Specification.definition decl params prems spec lthy; + val lhs' = Morphism.term (Local_Theory.target_morphism lthy') lhs; + val _ = + Proof_Display.print_consts true (Position.thread_data ()) lthy' + (Frees.defined (Frees.build (Frees.add_frees lhs'))) [(x, T)] + in lthy' end + fun meta_eq_const T = Const (\<^const_name>\Pure.eq\, T --> T --> propT); fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u; @@ -2136,7 +2091,7 @@ fun define_cond binding f_sty cond_suffix read_cond (ctxt:local_theory) = let val bdg = Binding.suffix_name cond_suffix binding val eq = mk_meta_eq(Free(Binding.name_of bdg, f_sty),read_cond ctxt) val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[]) - in def_cmd args true ctxt end + in def_cmd args ctxt end fun define_inv cid_long ((lbl, pos), inv) thy = let val bdg = (* Binding.suffix_name cid_long *) (Binding.make (lbl,pos)) @@ -2275,34 +2230,34 @@ ML\ structure DOF_lib = struct fun define_shortcut name latexshcut = - Thy_Output.antiquotation_raw name (Scan.succeed ()) + Document_Output.antiquotation_raw name (Scan.succeed ()) (fn _ => fn () => Latex.string latexshcut) (* This is a generalization of the Isabelle2020 function "control_antiquotation" from document_antiquotations.ML. (Thanks Makarius!) *) fun define_macro name s1 s2 reportNtest = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input) (fn ctxt => fn src => let val () = reportNtest ctxt src - in src |> Latex.enclose_block s1 s2 - o Thy_Output.output_document ctxt {markdown = false} + in src |> XML.enclose s1 s2 + o Document_Output.output_document ctxt {markdown = false} end); local (* hide away really strange local construction *) fun enclose_body2 front body1 middle body2 post = - (if front = "" then [] else [Latex.string front]) @ body1 @ - (if middle = "" then [] else [Latex.string middle]) @ body2 @ - (if post = "" then [] else [Latex.string post]); + (if front = "" then [] else Latex.string front) @ body1 @ + (if middle = "" then [] else Latex.string middle) @ body2 @ + (if post = "" then [] else Latex.string post); in fun define_macro2 name front middle post reportNtest1 reportNtest2 = - Thy_Output.antiquotation_raw_embedded name (Scan.lift ( Args.cartouche_input + Document_Output.antiquotation_raw_embedded name (Scan.lift ( Args.cartouche_input -- Args.cartouche_input)) (fn ctxt => fn (src1,src2) => let val () = reportNtest1 ctxt src1 val () = reportNtest2 ctxt src2 - val T1 = Thy_Output.output_document ctxt {markdown = false} src1 - val T2 = Thy_Output.output_document ctxt {markdown = false} src2 - in Latex.block(enclose_body2 front T1 middle T2 post) + val T1 = Document_Output.output_document ctxt {markdown = false} src1 + val T2 = Document_Output.output_document ctxt {markdown = false} src2 + in enclose_body2 front T1 middle T2 post end); end @@ -2330,8 +2285,8 @@ fun prepare_text ctxt = fun string_2_text_antiquotation ctxt text = prepare_text ctxt text - |> Thy_Output.output_source ctxt - |> Thy_Output.isabelle ctxt + |> Document_Output.output_source ctxt + |> Document_Output.isabelle ctxt fun string_2_theory_text_antiquotation ctxt text = let @@ -2339,12 +2294,12 @@ fun string_2_theory_text_antiquotation ctxt text = in prepare_text ctxt text |> Token.explode0 keywords - |> maps (Thy_Output.output_token ctxt) - |> Thy_Output.isabelle ctxt + |> maps (Document_Output.output_token ctxt) + |> Document_Output.isabelle ctxt end fun gen_text_antiquotation name reportNcheck compile = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input) (fn ctxt => fn text:Input.source => let val _ = reportNcheck ctxt text; @@ -2398,15 +2353,15 @@ fun environment_delim name = ("%\n\\begin{" ^ Latex.output_name name ^ "}\n", "\n\\end{" ^ Latex.output_name name ^ "}"); -fun environment_block name = environment_delim name |-> Latex.enclose_body #> Latex.block; +fun environment_block name = environment_delim name |-> XML.enclose; fun enclose_env verbatim ctxt block_env body = if Config.get ctxt Document_Antiquotation.thy_output_display then if verbatim - then environment_block block_env [body] - else Latex.environment_block block_env [body] - else Latex.block ([Latex.string ("\\inline"^block_env ^"{")] @ [body] @ [ Latex.string ("}")]); + then environment_block block_env body + else Latex.environment block_env body + else XML.enclose ("\\inline"^block_env ^"{") "}" body; end \ diff --git a/src/ROOT b/src/ROOT index abc6750e..66961d86 100755 --- a/src/ROOT +++ b/src/ROOT @@ -1,5 +1,5 @@ session "Isabelle_DOF" = "Functional-Automata" + - options [document = pdf, document_output = "output"] + options [document = pdf, document_output = "output", document_build = "build"] sessions "Regular-Sets" directories diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 749f381b..5c8a72b2 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -47,23 +47,15 @@ doc_class abstract = ML\ -local open ODL_Command_Parser in -val _ = Outer_Syntax.command ("abstract*", @{here}) "Textual Definition" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (Onto_Macros.enriched_document_cmd_exp - (SOME "abstract") - [] - {markdown = true} ))); +val _ = + ODL_Command_Parser.document_command ("abstract*", @{here}) "Textual Definition" + {markdown = true, body = true} + (Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []); - -val _ = Outer_Syntax.command ("author*", @{here}) "Textual Definition" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (Onto_Macros.enriched_document_cmd_exp - (SOME "author") - [] - {markdown = true} ))); - -end +val _ = + ODL_Command_Parser.document_command ("author*", @{here}) "Textual Definition" + {markdown = true, body = true} + (Onto_Macros.enriched_document_cmd_exp (SOME "author") []); \ text\Scholarly Paper is oriented towards the classical domains in science: @@ -292,45 +284,41 @@ setup\Theorem_default_class_setup\ ML\ local open ODL_Command_Parser in -(* {markdown = true} sets the parsing process such that in the text-core - markdown elements are accepted. *) +val _ = + ODL_Command_Parser.document_command ("Definition*", @{here}) "Textual Definition" + {markdown = true, body = true} + (fn meta_args => fn thy => + let + val ddc = Config.get_global thy Definition_default_class + val use_Definition_default = SOME(((ddc = "") ? (K "math_content")) ddc) + in + Onto_Macros.enriched_formal_statement_command + use_Definition_default [("mcc","defn")] meta_args thy + end); - -val _ = let fun use_Definition_default thy = - let val ddc = Config.get_global thy Definition_default_class - in (SOME(((ddc = "") ? (K "math_content")) ddc)) end - in Outer_Syntax.command ("Definition*", @{here}) "Textual Definition" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (fn args => fn thy => - Onto_Macros.enriched_formal_statement_command - (use_Definition_default thy) - [("mcc","defn")] - {markdown = true} args thy))) - end; +val _ = + ODL_Command_Parser.document_command ("Lemma*", @{here}) "Textual Lemma Outline" + {markdown = true, body = true} + (fn meta_args => fn thy => + let + val ddc = Config.get_global thy Definition_default_class + val use_Lemma_default = SOME(((ddc = "") ? (K "math_content")) ddc) + in + Onto_Macros.enriched_formal_statement_command + use_Lemma_default [("mcc","lem")] meta_args thy + end); -val _ = let fun use_Lemma_default thy = - let val ddc = Config.get_global thy Definition_default_class - in (SOME(((ddc = "") ? (K "math_content")) ddc)) end - in Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (fn args => fn thy => - Onto_Macros.enriched_formal_statement_command - (use_Lemma_default thy) - [("mcc","lem")] - {markdown = true} args thy))) - end; - -val _ = let fun use_Theorem_default thy = - let val ddc = Config.get_global thy Definition_default_class - in (SOME(((ddc = "") ? (K "math_content")) ddc)) end - in Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline" - (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (fn args => fn thy => - Onto_Macros.enriched_formal_statement_command - (use_Theorem_default thy) - [("mcc","thm")] - {markdown = true} args thy))) - end; +val _ = + ODL_Command_Parser.document_command ("Theorem*", @{here}) "Textual Theorem Outline" + {markdown = true, body = true} + (fn meta_args => fn thy => + let + val ddc = Config.get_global thy Definition_default_class + val use_Theorem_default = SOME(((ddc = "") ? (K "math_content")) ddc) + in + Onto_Macros.enriched_formal_statement_command + use_Theorem_default [("mcc","thm")] meta_args thy + end); end \ diff --git a/src/patches/present_theory b/src/patches/present_theory new file mode 100644 index 00000000..94264392 --- /dev/null +++ b/src/patches/present_theory @@ -0,0 +1,36 @@ +# HG changeset patch +# User wenzelm +# Date 1639864289 -3600 +# Sat Dec 18 22:51:29 2021 +0100 +# Node ID fcd643ddbfb2bcc60b301d8630d563ea265f7719 +# Parent 70be57333ea1b0e1866be2e944f2e0f70c437ae4 +Toplevel.present_theory for Isabelle/DOF; + +diff -r 70be57333ea1 -r fcd643ddbfb2 src/Pure/Isar/toplevel.ML +--- a/src/Pure/Isar/toplevel.ML Sun Dec 12 10:42:51 2021 +0100 ++++ b/src/Pure/Isar/toplevel.ML Sat Dec 18 22:51:29 2021 +0100 +@@ -55,6 +55,7 @@ + val ignored: Position.T -> transition + val malformed: Position.T -> string -> transition + val generic_theory: (generic_theory -> generic_theory) -> transition -> transition ++ val present_theory: (theory -> theory) -> (state -> Latex.text) -> transition -> transition + val theory': (bool -> theory -> theory) -> transition -> transition + val theory: (theory -> theory) -> transition -> transition + val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition +@@ -452,6 +453,16 @@ + (fn Theory gthy => node_presentation (Theory (f gthy)) + | _ => raise UNDEF)); + ++fun present_theory f g = present_transaction (fn _ => ++ (fn Theory (Context.Theory thy) => ++ let val thy' = thy ++ |> Sign.new_group ++ |> f ++ |> Sign.reset_group; ++ in node_presentation (Theory (Context.Theory thy')) end ++ | _ => raise UNDEF)) ++ (presentation g); ++ + fun theory' f = transaction (fn int => + (fn Theory (Context.Theory thy) => + let val thy' = thy diff --git a/src/scripts/build_lib.sh b/src/scripts/build_lib.sh index e6b88613..1038a24e 100755 --- a/src/scripts/build_lib.sh +++ b/src/scripts/build_lib.sh @@ -125,12 +125,11 @@ rm -f *.aux sed -i -e 's/<@>/@/g' *.tex -$ISABELLE_TOOL latex -o sty "root.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \ -{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_TOOL latex -o bbl "root.tex"; } && \ -{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_TOOL latex -o idx "root.tex"; } && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" && \ -$ISABELLE_TOOL latex -o "$OUTFORMAT" "root.tex" +$ISABELLE_PDFLATEX root && \ +{ [ ! -f "$ROOT_NAME.bib" ] || $ISABELLE_BIBTEX root; } && \ +{ [ ! -f "$ROOT_NAME.idx" ] || $ISABELLE_MAKEINDEX root; } && \ +$ISABELLE_PDFLATEX root && \ +$ISABELLE_PDFLATEX root MISSING_CITATIONS=`grep 'Warning.*Citation' root.log | awk '{print $5}' | sort -u` if [ "$MISSING_CITATIONS" != "" ]; then From 86b555b56e4419ef63cde344f4a6be507c31ce67 Mon Sep 17 00:00:00 2001 From: Makarius Date: Sat, 18 Dec 2021 23:07:25 +0100 Subject: [PATCH 02/11] Disable TR_my_commented_isabelle for now: does not work with Isabelle2021-1. --- examples/technical_report/ROOTS | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/technical_report/ROOTS b/examples/technical_report/ROOTS index d4b62f18..e8c0ad59 100755 --- a/examples/technical_report/ROOTS +++ b/examples/technical_report/ROOTS @@ -1,2 +1,2 @@ Isabelle_DOF-Manual -TR_my_commented_isabelle +#TR_my_commented_isabelle From bcf784908382176495a98da75db985b0df5fa9d1 Mon Sep 17 00:00:00 2001 From: Makarius Date: Sun, 19 Dec 2021 13:22:07 +0100 Subject: [PATCH 03/11] Proper component setup. --- NOTES.thy | 87 ++++++++++++++++++++++++++++++++++++++++++++++++++++ etc/options | 12 ++++++++ etc/settings | 3 ++ 3 files changed, 102 insertions(+) create mode 100644 NOTES.thy create mode 100644 etc/options create mode 100644 etc/settings diff --git a/NOTES.thy b/NOTES.thy new file mode 100644 index 00000000..a1ab4a52 --- /dev/null +++ b/NOTES.thy @@ -0,0 +1,87 @@ +chapter \Notes on Isabelle/DOF for Isabelle2021-1\ + +theory NOTES + imports Main +begin + +section \Isabelle/DOF component setup\ + +subsection \Terminology\ + +text \ + \<^item> The concept of \<^emph>\Isabelle system component\ is explained in \<^doc>\system\ + section 1.1.1; see also \<^tool>\components\ explained in section 7.3. + + For example: + + \<^verbatim>\isabelle components -l\ + + \<^item> In the private terminology of Burkhart, the word "component" has a + different meaning: a tool implemented in Isabelle/ML that happens to + declare context data (many ML tools do that, it is not very special, + similar to defining a \<^verbatim>\datatype\ or \<^verbatim>\structure\ in ML). +\ + + +subsection \Isabelle/DOF as component\ + +text \ + Formal Isabelle/DOF component setup happens here: + + \<^item> \<^path>\$ISABELLE_HOME_USER/etc/components\ + + \<^item> A suitable directory entry in the file registers our component to + existing Isabelle installation; it also activates the session + directory tree starting at \<^file>\$ISABELLE_DOF_HOME/ROOTS\. + + \<^item> Alternative: use \<^path>\$ISABELLE_HOME/Admin/build_release\ with + option \<^verbatim>\-c\ to produce a derived Isabelle distribution that bundles + our component for end-users (maybe even with AFP entries). + + \<^item> \<^file>\$ISABELLE_DOF_HOME/etc/settings\ + + \<^item> This provides a pervasive Bash process environment (variables, + shell functions etc.). It may refer to \<^verbatim>\$COMPONENT\ for the + component root, e.g. to retain it in variable \<^dir>\$ISABELLE_DOF_HOME\. + + \<^item> Historically, it used to be the main configuration area, but today + we see more and more alternatives, e.g. system options or services in + Isabelle/Scala (see below). + + \<^item> \<^file>\$ISABELLE_DOF_HOME/etc/options\ + + \<^item> options declared as \<^verbatim>\public\ appear in the Isabelle/jEdit dialog + \<^action>\plugin-options\ (according to their \<^verbatim>\section\) + + \<^item> all options (public and non-public) are available for command-line + usage, e.g. \<^verbatim>\isabelle build -o dof_url="..."\ + + \<^item> access to options in Isabelle/ML: + + \<^item> implicit (for the running ML session) + \<^ML>\Options.default_string \<^system_option>\dof_url\\ + + \<^item> explicit (e.g. for each theories section in + \<^file>\$ISABELLE_HOME/src/Pure/Tools/build.ML\): + \<^ML>\fn options => Options.string options \<^system_option>\dof_url\\ + + \<^item> access in Isabelle/Scala is always explicit; the initial options + should be created only once and passed around as explicit argument: + + \<^scala>\{ + val options = isabelle.Options.init(); + options.string("dof_url"); + }\ + + Note: there are no antiquotations in Isabelle/Scala, so the literal + string \<^scala>\"dof_url"\ is unchecked. +\ + + +section \Isabelle/ML\ + +section \Isabelle/Scala\ + +end + +(* :maxLineLen=75: *) \ No newline at end of file diff --git a/etc/options b/etc/options new file mode 100644 index 00000000..bd81e544 --- /dev/null +++ b/etc/options @@ -0,0 +1,12 @@ +(* :mode=isabelle-options: *) + +section "Isabelle/DOF" + +public option dof_url : string = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF" + -- "Isabelle/DOF source repository" + +option dof_artifact_dir : string = "releases/Isabelle_DOF/Isabelle_DOF" + -- "Isabelle/DOF release artifacts" + +option dof_artifact_host : string = "artifacts.logicalhacking.com" + diff --git a/etc/settings b/etc/settings new file mode 100644 index 00000000..3b2549b9 --- /dev/null +++ b/etc/settings @@ -0,0 +1,3 @@ +# -*- shell-script -*- :mode=shellscript: + +ISABELLE_DOF_HOME="$COMPONENT" From ff32bac3fcc64f8f7e9b36c80abf887d981dbd2d Mon Sep 17 00:00:00 2001 From: Makarius Date: Sun, 19 Dec 2021 13:48:45 +0100 Subject: [PATCH 04/11] Miscellaneous NEWS and Notes. --- NOTES.thy | 62 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/NOTES.thy b/NOTES.thy index a1ab4a52..8f3463c3 100644 --- a/NOTES.thy +++ b/NOTES.thy @@ -80,8 +80,70 @@ text \ section \Isabelle/ML\ + section \Isabelle/Scala\ + +section \Miscellaneous NEWS and Notes\ + +text \ + \<^item> Document preparation: there are many new options etc. that might help + to fine-tune DOF output, e.g. \<^system_option>\document_comment_latex\. + + \<^item> ML: Theory_Data / Generic_Data: "val extend = I" has been removed; + obsolete since Isabelle2021. + + \<^item> ML: \<^ML>\Thm.instantiate\ and related operations now use explicit + abstract types for the instantiate, see \<^file>\~~/src/Pure/term_items.ML\ + + \<^item> ML: new antiquotation "instantiate" allows to instantiate formal + entities (types, terms, theorems) with values given ML. For example: + + \<^ML>\fn (A, B) => + \<^instantiate>\'a = A and 'b = B in typ \('a \ 'b) list\\\ + + \<^ML>\fn A => + \<^instantiate>\'a = A in + lemma (schematic) \x = y \ y = x\ for x y :: 'a by simp\\ + + \<^item> ML: new antiquotations for type constructors and term constants. For + example: + + \<^ML>\\<^Type>\nat\\ + \<^ML>\fn (A, B) => \<^Type>\fun A B\\ + \<^ML>\\<^Type_fn>\fun A B => \(A, B)\\\ + + \<^ML>\fn (A, B) => \<^Const>\conj for A B\\ + \<^ML>\\<^Const_fn>\conj for A B => \(A, B)\\\ + + \<^ML>\fn t => + case t of + \<^Const_>\plus T for x y\ => ("+", T, x, y) + | \<^Const_>\minus T for x y\ => ("-", T, x, y) + | \<^Const_>\times T for x y\ => ("*", T, x, y)\ + + Note: do not use unchecked things like + \<^ML>\Const ("List.list.Nil", Type ("Nat.nat", []))\ + + \<^item> ML: antiquotations "try" and "can" operate directly on the given ML + expression, in contrast to functions "try" and "can" that modify + application of a function. + + Note: instead of semantically ill-defined "handle _ => ...", use + something like this: + + \<^ML>\ + fn (x, y) => + (case \<^try>\x div y\ of + SOME z => z + | NONE => 0) + \ + + \<^ML>\ + fn (x, y) => \<^try>\x div y\ |> the_default 0 + \ +\ + end (* :maxLineLen=75: *) \ No newline at end of file From 2e4d37e3ca6bf5e655d900af570d65d681f486dd Mon Sep 17 00:00:00 2001 From: Makarius Date: Sun, 19 Dec 2021 15:23:33 +0100 Subject: [PATCH 05/11] More on Document preparation in Isabelle/ML. --- NOTES.thy | 50 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 49 insertions(+), 1 deletion(-) diff --git a/NOTES.thy b/NOTES.thy index 8f3463c3..4fbb6773 100644 --- a/NOTES.thy +++ b/NOTES.thy @@ -78,7 +78,55 @@ text \ \ -section \Isabelle/ML\ +section \Document preparation in Isabelle/ML\ + +subsection \Theory presentation hook\ + +text \ + \<^ML>\Thy_Info.add_presentation\ installs a hook to be invoked at the + end of successful loading of theories; the provided context + \<^ML_type>\Thy_Info.presentation_context\ provides access to + \<^ML_type>\Options.T\ and \<^ML_type>\Document_Output.segment\ with + command-spans and semantic states. + + An example is regular Latex output in + \<^file>\$ISABELLE_HOME/src/Pure/Thy/thy_info.ML\ where \<^ML>\Export.export\ + is used to produce export artifacts in the session build database, for + retrieval via Isabelle/Scala. +\ + + +subsection \Document commands\ + +text \ + Isar toplevel commands now support a uniform concept for + \<^ML_type>\Toplevel.presentation\, but the exported interfaces are + limited to commands that do not change the semantic state: see + \<^ML>\Toplevel.present\ and \<^ML>\Toplevel.present_local_theory\. + + There is an adhoc change to support \<^verbatim>\Toplevel.present_theory\ in + \<^file>\$ISABELLE_DOF_HOME/src/patches/present_theory\. + + An alternative, without patching Isabelle2021-1 in production, is to use + the presentation hook together with a function like this: +\ + +ML \ + fun present_segment pr (segment: Document_Output.segment) = + (case #span segment of + Command_Span.Span (Command_Span.Command_Span (name, _), toks) => + let + val {span, command = tr, prev_state = st, state = st'} = segment; + val tr' = + Toplevel.empty + |> Toplevel.name (Toplevel.name_of tr) + |> Toplevel.position (Toplevel.pos_of tr) + |> Toplevel.present (pr name toks); + val st'' = Toplevel.command_exception false tr' st' + handle Runtime.EXCURSION_FAIL (exn, _) => Exn.reraise exn; + in {span = span, command = tr, prev_state = st, state = st''} end + | _ => segment); +\ section \Isabelle/Scala\ From 4e4995bde5f0ebbed3628012067714645b298c26 Mon Sep 17 00:00:00 2001 From: Makarius Date: Sun, 19 Dec 2021 16:50:21 +0100 Subject: [PATCH 06/11] Isabelle/Scala build.props with some pro-forma services (unusual package name prevents problems with Maven/IntelliJ). --- etc/build.props | 12 ++++ examples/CENELEC_50128/mini_odo/ROOT | 2 +- examples/math_exam/MathExam/ROOT | 2 +- .../2018-cicm-isabelle_dof-applications/ROOT | 2 +- examples/scholarly_paper/2020-iFM-CSP/ROOT | 2 +- examples/scholarly_paper/2021-ITP-PMTI/ROOT | 2 +- .../technical_report/Isabelle_DOF-Manual/ROOT | 2 +- .../TR_my_commented_isabelle/ROOT | 2 +- src/ROOT | 2 +- src/scala/dof_document_build.scala | 17 +++++ src/scala/dof_mkroot.scala | 69 +++++++++++++++++++ src/scala/dof_tools.scala | 13 ++++ 12 files changed, 119 insertions(+), 8 deletions(-) create mode 100644 etc/build.props create mode 100644 src/scala/dof_document_build.scala create mode 100644 src/scala/dof_mkroot.scala create mode 100644 src/scala/dof_tools.scala diff --git a/etc/build.props b/etc/build.props new file mode 100644 index 00000000..af46f5ed --- /dev/null +++ b/etc/build.props @@ -0,0 +1,12 @@ +title = Isabelle/DOF +module = $ISABELLE_HOME_USER/DOF/isabelle_dof.jar +no_build = false +requirements = \ + env:ISABELLE_SCALA_JAR +sources = \ + src/scala/dof_document_build.scala \ + src/scala/dof_mkroot.scala \ + src/scala/dof_tools.scala +services = \ + isabelle_dof.DOF_Tools \ + isabelle_dof.DOF_Document_Build$Engine diff --git a/examples/CENELEC_50128/mini_odo/ROOT b/examples/CENELEC_50128/mini_odo/ROOT index 34c7fe80..0dec6927 100755 --- a/examples/CENELEC_50128/mini_odo/ROOT +++ b/examples/CENELEC_50128/mini_odo/ROOT @@ -1,5 +1,5 @@ session "mini_odo" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = "build"] + options [document = pdf, document_output = "output", document_build = dof] theories "mini_odo" document_files diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT index 21668d02..c8df95d5 100755 --- a/examples/math_exam/MathExam/ROOT +++ b/examples/math_exam/MathExam/ROOT @@ -1,5 +1,5 @@ session "MathExam" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = "build"] + options [document = pdf, document_output = "output", document_build = dof] theories MathExam document_files diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT index a3017a2b..ca893890 100755 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT @@ -1,5 +1,5 @@ session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = "build", + options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true] theories IsaDofApplications diff --git a/examples/scholarly_paper/2020-iFM-CSP/ROOT b/examples/scholarly_paper/2020-iFM-CSP/ROOT index f5388f29..2b41c73d 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/ROOT +++ b/examples/scholarly_paper/2020-iFM-CSP/ROOT @@ -1,5 +1,5 @@ session "2020-iFM-csp" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = "build"] + options [document = pdf, document_output = "output", document_build = dof] theories "paper" document_files diff --git a/examples/scholarly_paper/2021-ITP-PMTI/ROOT b/examples/scholarly_paper/2021-ITP-PMTI/ROOT index 0cfda600..1771c955 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/ROOT +++ b/examples/scholarly_paper/2021-ITP-PMTI/ROOT @@ -1,5 +1,5 @@ session "2021-ITP-PMTI" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = "build"] + options [document = pdf, document_output = "output", document_build = dof] theories "paper" document_files diff --git a/examples/technical_report/Isabelle_DOF-Manual/ROOT b/examples/technical_report/Isabelle_DOF-Manual/ROOT index 6e759f0e..466cb2a1 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/ROOT +++ b/examples/technical_report/Isabelle_DOF-Manual/ROOT @@ -1,5 +1,5 @@ session "Isabelle_DOF-Manual" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = "build", + options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true] theories "Isabelle_DOF-Manual" diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index ffc5b145..6f1863e5 100755 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -1,5 +1,5 @@ session "TR_MyCommentedIsabelle" = "Isabelle_DOF" + - options [document = pdf, document_output = "output", document_build = "build", + options [document = pdf, document_output = "output", document_build = dof, quick_and_dirty = true] theories "TR_MyCommentedIsabelle" diff --git a/src/ROOT b/src/ROOT index 66961d86..df02fb01 100755 --- a/src/ROOT +++ b/src/ROOT @@ -1,5 +1,5 @@ session "Isabelle_DOF" = "Functional-Automata" + - options [document = pdf, document_output = "output", document_build = "build"] + options [document = pdf, document_output = "output", document_build = dof] sessions "Regular-Sets" directories diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala new file mode 100644 index 00000000..58e77243 --- /dev/null +++ b/src/scala/dof_document_build.scala @@ -0,0 +1,17 @@ +/* Author: Makarius + +Build theory document (PDF) from session database. +*/ + +package isabelle_dof + +import isabelle._ + + +object DOF_Document_Build +{ + class Engine extends Document_Build.Bash_Engine("dof") + { + override def use_build_script: Boolean = true + } +} diff --git a/src/scala/dof_mkroot.scala b/src/scala/dof_mkroot.scala new file mode 100644 index 00000000..81c0b846 --- /dev/null +++ b/src/scala/dof_mkroot.scala @@ -0,0 +1,69 @@ +/* Author: Makarius + +Prepare session root directory for Isabelle/DOF. +*/ + +package isabelle_dof + +import isabelle._ + + +object DOF_Mkroot +{ + /** mkroot **/ + + def mkroot( + session_name: String = "", + session_dir: Path = Path.current, + session_parent: String = "", + init_repos: Boolean = false, + title: String = "", + author: String = "", + progress: Progress = new Progress): Unit = + { + Mkroot.mkroot(session_name = session_name, session_dir = session_dir, + session_parent = session_parent, init_repos = init_repos, + title = title, author = author, progress = progress) + } + + + + /** Isabelle tool wrapper **/ + + val isabelle_tool = Isabelle_Tool("dof_mkroot", "prepare session root directory for Isabelle/DOF", + Scala_Project.here, args => + { + var author = "" + var init_repos = false + var title = "" + var session_name = "" + + val getopts = Getopts(""" +Usage: isabelle dof_mkroot [OPTIONS] [DIRECTORY] + + Options are: + -A LATEX provide author in LaTeX notation (default: user name) + -I init Mercurial repository and add generated files + -T LATEX provide title in LaTeX notation (default: session name) + -n NAME alternative session name (default: directory base name) + + Prepare session root directory (default: current directory). +""", + "A:" -> (arg => author = arg), + "I" -> (arg => init_repos = true), + "T:" -> (arg => title = arg), + "n:" -> (arg => session_name = arg)) + + val more_args = getopts(args) + + val session_dir = + more_args match { + case Nil => Path.current + case List(dir) => Path.explode(dir) + case _ => getopts.usage() + } + + mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos, + author = author, title = title, progress = new Console_Progress) + }) +} diff --git a/src/scala/dof_tools.scala b/src/scala/dof_tools.scala new file mode 100644 index 00000000..a889bac7 --- /dev/null +++ b/src/scala/dof_tools.scala @@ -0,0 +1,13 @@ +/* Author: Makarius + +Isabelle/DOF command-line tools. +*/ + +package isabelle_dof + +import isabelle._ + + +class DOF_Tools extends Isabelle_Scala_Tools( + DOF_Mkroot.isabelle_tool +) From fadd9822858d299faae13e6139a1f7b79864fc29 Mon Sep 17 00:00:00 2001 From: Makarius Date: Sun, 19 Dec 2021 17:16:37 +0100 Subject: [PATCH 07/11] More on Isabelle/Scala services, notably document preparation. --- NOTES.thy | 43 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/NOTES.thy b/NOTES.thy index 4fbb6773..a689bd3c 100644 --- a/NOTES.thy +++ b/NOTES.thy @@ -129,7 +129,48 @@ ML \ \ -section \Isabelle/Scala\ +section \Isabelle/Scala services\ + +subsection \Isabelle/DOF/Scala module\ + +text \ + \<^item> \<^file>\$ISABELLE_DOF_HOME/etc/build.props\ is the main specification for + the Isabelle/DOF/Scala module. It is built on the spot as required, e.g. + for \<^verbatim>\isabelle scala\ or \<^verbatim>\isabelle jedit\; an alternative is to invoke + \<^verbatim>\isabelle scala_build\ manually. See also \<^doc>\system\, chapter 5, + especially section 5.2. + + \<^item> \<^verbatim>\isabelle scala_project\ helps to develop Isabelle/Scala tools with + proper IDE support, notably IntelliJ IDEA: the generated project uses + Maven. See also \<^doc>\system\, section 5.2.3. + + \<^item> Command-line tools should be always implemented in Scala; old-fashioned + shell scripts are no longer required (and more difficult to implement + properly). Only a few low-level tools are outside the Scala environment, + e.g. \<^verbatim>\isabelle getenv\. Add-on components should always use a name + prefix for their tools, e.g. \<^verbatim>\isabelle dof_mkroot\ as defined in + \<^file>\$ISABELLE_DOF_HOME/src/scala/dof_mkroot.scala\. +\ + + +subsection \Document preparation\ + +text \ + \<^item> \<^scala_type>\isabelle.Document_Build.Engine\ is the main entry-point + for user-defined document preparation; existing templates and examples + are defined in the same module \<^file>\~~/src/Pure/Thy/document_build.scala\. + There are two stages: + + \<^enum> \<^verbatim>\prepare_directory\: populate the document output directory (e.g. + copy static document files, collect generated document sources from the + session build database). + + \<^enum> \<^verbatim>\build_document\: produce the final PDF within the document output + directory (e.g. via standard LaTeX tools). + + See also \<^system_option>\document_build\ as explained in \<^doc>\system\, + section 3.3. +\ section \Miscellaneous NEWS and Notes\ From 70617f59fe87bd8f0217c7aff4f54559bb16038a Mon Sep 17 00:00:00 2001 From: Makarius Date: Sun, 19 Dec 2021 17:51:38 +0100 Subject: [PATCH 08/11] Avoid pointless Latex comments: as an example of how to re-define document output. --- src/scala/dof_document_build.scala | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index 58e77243..0d2393a7 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -13,5 +13,26 @@ object DOF_Document_Build class Engine extends Document_Build.Bash_Engine("dof") { override def use_build_script: Boolean = true + + override def prepare_directory( + context: Document_Build.Context, + dir: Path, + doc: Document_Build.Document_Variant): Document_Build.Directory = + { + context.prepare_directory(dir, doc, new Latex_Output(context.options)) + } + } + + class Latex_Output(options: Options) extends Latex.Output(options) + { + override def latex_environment( + name: String, + body: Latex.Text, + optional_argument: String = ""): Latex.Text = + { + XML.enclose( + "\n\\begin{" + name + "}" + optional_argument + "\n", + "\n\\end{" + name + "}", body) + } } } From 99264edc02da7a4614ce747ef105707025868565 Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 20 Dec 2021 09:22:13 +0100 Subject: [PATCH 09/11] More NOTES. --- NOTES.thy | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/NOTES.thy b/NOTES.thy index a689bd3c..f45aea38 100644 --- a/NOTES.thy +++ b/NOTES.thy @@ -80,6 +80,17 @@ text \ section \Document preparation in Isabelle/ML\ +subsection \Session presentation hook\ + +text \ + \<^ML>\Build.add_hook\ allows to install a global session presentation + hook. It is used e.g. in Isabelle/Mirabelle to analyze all loaded + theories via Sledgehammer and other tools. Isabelle/DOF could use it to + "wrap-up" the whole session, to check if all document constraints hold + (cf. "monitors"). +\ + + subsection \Theory presentation hook\ text \ @@ -129,6 +140,15 @@ ML \ \ +subsection \Document content\ + +text \ + XML is now used uniformly (sometimes as inlined YXML). The meaning of + markup elements and properties is defined in + \<^scala_type>\isabelle.Latex.Output\ (or user-defined subclasses). +\ + + section \Isabelle/Scala services\ subsection \Isabelle/DOF/Scala module\ From 2547b2324ec65075365606e536648d8cc203150c Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 20 Dec 2021 16:27:16 +0100 Subject: [PATCH 10/11] Adhoc examples for ML antiquotations. --- NOTES.thy | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/NOTES.thy b/NOTES.thy index f45aea38..32ab328f 100644 --- a/NOTES.thy +++ b/NOTES.thy @@ -253,6 +253,22 @@ text \ \ \ +text \Adhoc examples:\ + +ML \ + fun mk_plus x y = \<^Const>\plus \<^Type>\nat\ for x y\; + + fn \<^Const_>\plus \<^Type>\nat\ for \<^Const_>\Groups.zero \<^Type>\nat\\ y\ => y; +\ + +ML \ + fn (A, B) => + \<^instantiate>\A and B in term \A \ B \ B \ A\\; + + fn (A, B) => + \<^instantiate>\A and B in lemma \A \ B \ B \ A\ by simp\; +\ + end (* :maxLineLen=75: *) \ No newline at end of file From 4352691e9553bd990f5cb900ca8dac916cb32d8f Mon Sep 17 00:00:00 2001 From: Makarius Date: Mon, 20 Dec 2021 21:02:57 +0100 Subject: [PATCH 11/11] Support Isabelle2021-1 without patches: in the next release it will be simpler again. --- NOTES.thy | 25 ++------- src/DOF/Isa_DOF.thy | 84 ++++++++++++++++++++++++++++-- src/patches/present_theory | 36 ------------- src/scala/dof_document_build.scala | 16 +++++- 4 files changed, 99 insertions(+), 62 deletions(-) delete mode 100644 src/patches/present_theory diff --git a/NOTES.thy b/NOTES.thy index 32ab328f..737fb3d2 100644 --- a/NOTES.thy +++ b/NOTES.thy @@ -115,28 +115,9 @@ text \ limited to commands that do not change the semantic state: see \<^ML>\Toplevel.present\ and \<^ML>\Toplevel.present_local_theory\. - There is an adhoc change to support \<^verbatim>\Toplevel.present_theory\ in - \<^file>\$ISABELLE_DOF_HOME/src/patches/present_theory\. - - An alternative, without patching Isabelle2021-1 in production, is to use - the presentation hook together with a function like this: -\ - -ML \ - fun present_segment pr (segment: Document_Output.segment) = - (case #span segment of - Command_Span.Span (Command_Span.Command_Span (name, _), toks) => - let - val {span, command = tr, prev_state = st, state = st'} = segment; - val tr' = - Toplevel.empty - |> Toplevel.name (Toplevel.name_of tr) - |> Toplevel.position (Toplevel.pos_of tr) - |> Toplevel.present (pr name toks); - val st'' = Toplevel.command_exception false tr' st' - handle Runtime.EXCURSION_FAIL (exn, _) => Exn.reraise exn; - in {span = span, command = tr, prev_state = st, state = st''} end - | _ => segment); + Since \<^verbatim>\Toplevel.present_theory\ is missing in Isabelle2021-1, we use a + workaround with an alternative presentation hook: it exports + \<^verbatim>\document/latex_dof\ files instead of regular \<^verbatim>\document/latex_dof\. \ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 5b168928..459246ef 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1628,13 +1628,91 @@ fun document_output_reports name {markdown, body} meta_args text ctxt = in [XML.Elem (m (Latex.output_name name), xml)] end; in document_output {markdown = markdown, markup = markup} meta_args text ctxt end; + +(* document output commands *) + +local + +(* alternative presentation hook (workaround for missing Toplevel.present_theory) *) + +structure Document_Commands = Theory_Data +( + type T = (string * (meta_args_t -> Input.source -> Proof.context -> Latex.text)) list; + val empty = []; + val merge = AList.merge (op =) (K true); +); + +fun get_document_command thy name = + AList.lookup (op =) (Document_Commands.get thy) name; + +fun document_segment (segment: Document_Output.segment) = + (case #span segment of + Command_Span.Span (Command_Span.Command_Span (name, _), _) => + (case try Toplevel.theory_of (#state segment) of + SOME thy => get_document_command thy name + | _ => NONE) + | _ => NONE); + +fun present_segment (segment: Document_Output.segment) = + (case document_segment segment of + SOME pr => + let + val {span, command = tr, prev_state = st, state = st'} = segment; + val src = Command_Span.content (#span segment) |> filter_out Document_Source.is_improper; + val parse = attributes -- Parse.document_source; + fun present ctxt = + let val (meta_args, text) = #1 (Token.syntax (Scan.lift parse) src ctxt); + in pr meta_args text ctxt end; + val tr' = + Toplevel.empty + |> Toplevel.name (Toplevel.name_of tr) + |> Toplevel.position (Toplevel.pos_of tr) + |> Toplevel.present (Toplevel.presentation_context #> present); + val st'' = Toplevel.command_exception false tr' st' + handle Runtime.EXCURSION_FAIL (exn, _) => Exn.reraise exn; + val FIXME = + Toplevel.setmp_thread_position tr (fn () => + writeln ("present_segment" ^ Position.here (Toplevel.pos_of tr) ^ "\n" ^ + XML.string_of (XML.Elem (Markup.empty, the_default [] (Toplevel.output_of st'))) ^ "\n---\n" ^ + XML.string_of (XML.Elem (Markup.empty, the_default [] (Toplevel.output_of st''))))) () + in {span = span, command = tr, prev_state = st, state = st''} end + | _ => segment); + +val _ = + Theory.setup (Thy_Info.add_presentation (fn {options, segments, ...} => fn thy => + if exists (Toplevel.is_skipped_proof o #state) segments then () + else + let + val segments' = map present_segment segments; + val body = Document_Output.present_thy options thy segments'; + in + if Options.string options "document" = "false" orelse + forall (is_none o document_segment) segments' then () + else + let + val thy_name = Context.theory_name thy; + val latex = Latex.isabelle_body thy_name body; + in Export.export thy \<^path_binding>\document/latex_dof\ latex end + end)); + +in + fun document_command (name, pos) descr mark cmd = - Outer_Syntax.command (name, pos) descr + (Outer_Syntax.command (name, pos) descr (attributes -- Parse.document_source >> (fn (meta_args, text) => - Toplevel.present_theory (cmd meta_args) - (Toplevel.presentation_context #> document_output_reports name mark meta_args text))); + Toplevel.theory (fn thy => + let + val thy' = cmd meta_args thy; + val _ = + (case get_document_command thy' name of + SOME pr => ignore (pr meta_args text (Proof_Context.init_global thy')) + | NONE => ()); + in thy' end))); + (Theory.setup o Document_Commands.map) + (AList.update (op =) (name, document_output_reports name mark))); +end; (* Core Command Definitions *) diff --git a/src/patches/present_theory b/src/patches/present_theory deleted file mode 100644 index 94264392..00000000 --- a/src/patches/present_theory +++ /dev/null @@ -1,36 +0,0 @@ -# HG changeset patch -# User wenzelm -# Date 1639864289 -3600 -# Sat Dec 18 22:51:29 2021 +0100 -# Node ID fcd643ddbfb2bcc60b301d8630d563ea265f7719 -# Parent 70be57333ea1b0e1866be2e944f2e0f70c437ae4 -Toplevel.present_theory for Isabelle/DOF; - -diff -r 70be57333ea1 -r fcd643ddbfb2 src/Pure/Isar/toplevel.ML ---- a/src/Pure/Isar/toplevel.ML Sun Dec 12 10:42:51 2021 +0100 -+++ b/src/Pure/Isar/toplevel.ML Sat Dec 18 22:51:29 2021 +0100 -@@ -55,6 +55,7 @@ - val ignored: Position.T -> transition - val malformed: Position.T -> string -> transition - val generic_theory: (generic_theory -> generic_theory) -> transition -> transition -+ val present_theory: (theory -> theory) -> (state -> Latex.text) -> transition -> transition - val theory': (bool -> theory -> theory) -> transition -> transition - val theory: (theory -> theory) -> transition -> transition - val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition -@@ -452,6 +453,16 @@ - (fn Theory gthy => node_presentation (Theory (f gthy)) - | _ => raise UNDEF)); - -+fun present_theory f g = present_transaction (fn _ => -+ (fn Theory (Context.Theory thy) => -+ let val thy' = thy -+ |> Sign.new_group -+ |> f -+ |> Sign.reset_group; -+ in node_presentation (Theory (Context.Theory thy')) end -+ | _ => raise UNDEF)) -+ (presentation g); -+ - fun theory' f = transaction (fn int => - (fn Theory (Context.Theory thy) => - let val thy' = thy diff --git a/src/scala/dof_document_build.scala b/src/scala/dof_document_build.scala index 0d2393a7..471c972d 100644 --- a/src/scala/dof_document_build.scala +++ b/src/scala/dof_document_build.scala @@ -19,7 +19,21 @@ object DOF_Document_Build dir: Path, doc: Document_Build.Document_Variant): Document_Build.Directory = { - context.prepare_directory(dir, doc, new Latex_Output(context.options)) + val latex_output = new Latex_Output(context.options) + val directory = context.prepare_directory(dir, doc, latex_output) + + // produced by alternative presentation hook (workaround for missing Toplevel.present_theory) + for (name <- context.document_theories) { + val path = Path.basic(Document_Build.tex_name(name)) + val xml = + YXML.parse_body(context.get_export(name.theory, Export.DOCUMENT_LATEX + "_dof").text) + if (xml.nonEmpty) { + File.Content(path, xml).output(latex_output(_, file_pos = path.implode_symbolic)) + .write(directory.doc_dir) + } + } + + directory } }