diff --git a/.ci/Jenkinsfile b/.ci/Jenkinsfile old mode 100644 new mode 100755 diff --git a/.ci/isabelle4isadof/Dockerfile b/.ci/isabelle4isadof/Dockerfile old mode 100644 new mode 100755 diff --git a/.config b/.config old mode 100644 new mode 100755 diff --git a/.gitattributes b/.gitattributes old mode 100644 new mode 100755 diff --git a/.gitignore b/.gitignore old mode 100644 new mode 100755 diff --git a/CHANGELOG.md b/CHANGELOG.md old mode 100644 new mode 100755 diff --git a/CITATION b/CITATION old mode 100644 new mode 100755 diff --git a/LICENSE b/LICENSE old mode 100644 new mode 100755 diff --git a/README.md b/README.md old mode 100644 new mode 100755 diff --git a/ROOTS b/ROOTS old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/ROOTS b/examples/CENELEC_50128/ROOTS old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/ROOT b/examples/CENELEC_50128/mini_odo/ROOT old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png b/examples/CENELEC_50128/mini_odo/document/figures/df-numerics-encshaft.png old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg b/examples/CENELEC_50128/mini_odo/document/figures/odometer.jpeg old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf b/examples/CENELEC_50128/mini_odo/document/figures/three-phase-odo.pdf old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png b/examples/CENELEC_50128/mini_odo/document/figures/wheel-df.png old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/isadof.cfg b/examples/CENELEC_50128/mini_odo/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/lstisadof.sty b/examples/CENELEC_50128/mini_odo/document/lstisadof.sty old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/preamble.tex b/examples/CENELEC_50128/mini_odo/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/root.bib b/examples/CENELEC_50128/mini_odo/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/document/root.mst b/examples/CENELEC_50128/mini_odo/document/root.mst old mode 100644 new mode 100755 diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy old mode 100644 new mode 100755 diff --git a/examples/README.md b/examples/README.md old mode 100644 new mode 100755 diff --git a/examples/ROOTS b/examples/ROOTS old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/figures/Polynomialdeg5.png b/examples/math_exam/MathExam/document/figures/Polynomialdeg5.png old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/isadof.cfg b/examples/math_exam/MathExam/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/math_exam/MathExam/document/preamble.tex b/examples/math_exam/MathExam/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/math_exam/ROOTS b/examples/math_exam/ROOTS old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-II-bgnd1.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-III-bgnd-text_section.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-IV-jumpInDocCLass.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-Intro.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-V-attribute.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/Dogfood-figures.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/InteractiveMathSheet.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/antiquotations-PIDE.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/isabelle-architecture.svg old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-as-es-application.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/figures/srac-definition.png old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/lstisadof.sty old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/scholarly_paper/ROOTS b/examples/scholarly_paper/ROOTS old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy b/examples/technical_report/Isabelle_DOF-Manual/Isabelle_DOF-Manual.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/ROOT b/examples/technical_report/Isabelle_DOF-Manual/ROOT old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-II-bgnd1.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-III-bgnd-text_section.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-IV-jumpInDocCLass.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-Intro.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-V-attribute.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Dogfood-figures.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/Isabelle_DOF-logo.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/antiquotations-PIDE.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-combined.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-dof.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/cicm2018-pdf.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg b/examples/technical_report/Isabelle_DOF-Manual/document/figures/document-hierarchy.svg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isabelle-architecture.svg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/isadof.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-as-es-application.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png b/examples/technical_report/Isabelle_DOF-Manual/document/figures/srac-definition.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg b/examples/technical_report/Isabelle_DOF-Manual/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.bib b/examples/technical_report/Isabelle_DOF-Manual/document/root.bib old mode 100644 new mode 100755 diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/root.mst b/examples/technical_report/Isabelle_DOF-Manual/document/root.mst old mode 100644 new mode 100755 diff --git a/examples/technical_report/ROOTS b/examples/technical_report/ROOTS old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/document-model.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/isabelle-architecture.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png b/examples/technical_report/TR_my_commented_isabelle/document/figures/markup-demo.png old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-I.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/pure-inferences-II.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf b/examples/technical_report/TR_my_commented_isabelle/document/figures/text-element.pdf old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg b/examples/technical_report/TR_my_commented_isabelle/document/isadof.cfg old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex b/examples/technical_report/TR_my_commented_isabelle/document/preamble.tex old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty b/examples/technical_report/TR_my_commented_isabelle/document/prooftree.sty old mode 100644 new mode 100755 diff --git a/examples/technical_report/TR_my_commented_isabelle/document/root.bib b/examples/technical_report/TR_my_commented_isabelle/document/root.bib old mode 100644 new mode 100755 diff --git a/src/DOF/Assert.thy b/src/DOF/Assert.thy old mode 100644 new mode 100755 diff --git a/src/DOF/AssertLong.thy b/src/DOF/AssertLong.thy old mode 100644 new mode 100755 diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy old mode 100644 new mode 100755 index 7a9eacf..c9ca1c9 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -80,7 +80,7 @@ fun enriched_document_command level = NONE => doc_attrs | SOME(NONE) => (("level",@{here}),"None")::doc_attrs | SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs - in gen_enriched_document_command I transform end; + in gen_enriched_document_command {inline=true} I transform end; val enriched_document_command_macro = enriched_document_command (* TODO ... *) @@ -92,7 +92,7 @@ fun enriched_formal_statement_command ncid (S: (string * string) list) = | _ => X) fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ (("formal_results",@{here}),"([]::thm list)")::doc_attrs - in gen_enriched_document_command transform_cid transform_attr end; + in gen_enriched_document_command {inline=true} transform_cid transform_attr end; fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), @@ -104,7 +104,9 @@ fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),mod fun mks thy = case DOF_core.get_object_global_opt oid thy of SOME NONE => (error("update of declared but not created doc_item:" ^ oid)) | SOME _ => (update_instance_command (((oid,pos),cid_pos),conv_attrs' thy) thy) - | NONE => (create_and_check_docitem false oid pos cid_pos (conv_attrs thy) thy) + | NONE => (create_and_check_docitem + {is_monitor = false} {is_inline = false} + oid pos cid_pos (conv_attrs thy) thy) val check = (assert_cmd name_opt modes prop) o Proof_Context.init_global in (* Toplevel.keep (check o Toplevel.context_of) *) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy old mode 100644 new mode 100755 index f76d8ce..6ea0717 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -166,8 +166,10 @@ struct type docobj = {pos : Position.T, thy_name : string, - value : term, - id : serial, cid : string} + value : term, + inline : bool, + id : serial, + cid : string} type docobj_tab ={tab : (docobj option) Symtab.table, maxano : int @@ -570,9 +572,10 @@ fun get_value_local oid ctxt = case get_object_local oid ctxt of (* missing : setting terms to ground (no type-schema vars, no schema vars. )*) fun update_value_global oid upd thy = case get_object_global oid thy of - SOME{pos,thy_name,value,id,cid} => + SOME{pos,thy_name,value,inline,id,cid} => let val tab' = Symtab.update(oid,SOME{pos=pos,thy_name=thy_name, - value=upd value,id=id, cid=cid}) + value=upd value,id=id, + inline=inline,cid=cid}) in map_data_global (upd_docobj_tab(fn{tab,maxano}=>{tab=tab' tab,maxano=maxano})) thy end | NONE => error("undefined doc object: "^oid) @@ -623,11 +626,14 @@ fun writeln_docrefs ctxt = let val {tab,...} = #docobj_tab(get_data ctxt) fun print_doc_items b ctxt = let val {docobj_tab={tab = x, ...},...}= get_data ctxt; - val _ = writeln "====================================="; - fun print_item (n, SOME({cid,id,pos,thy_name,value})) = + val _ = writeln "====================================="; + fun dfg true = "true" + |dfg false= "false" + fun print_item (n, SOME({cid,id,pos,thy_name,inline,value})) = (writeln ("docitem: "^n); writeln (" type: "^cid); writeln (" origine: "^thy_name); + writeln (" inline: "^dfg inline); writeln (" value: "^(Syntax.string_of_term ctxt value)) ) | print_item (n, NONE) = @@ -942,28 +948,8 @@ fun document_command markdown (loc, txt) = *) -ML\ Pure_Syn.document_command; -structure Pure_Syn_Ext = -struct -(* This interface function has not been exported from Pure_Syn (2018); - it should replace - Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string (2017) *) -fun output_document state markdown src = - let - val ctxt = Toplevel.presentation_context state; - val _ = Context_Position.report ctxt - (Input.pos_of src) - (Markup.language_document (Input.is_delimited src)); - in Thy_Output.output_document ctxt markdown src end; - (* this thing converts also source to (latex) string ... *) - -end; - -Pure_Syn_Ext.output_document : Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list; - -\ ML\ structure ODL_Command_Parser = @@ -1038,7 +1024,7 @@ fun cid_2_cidType cid_long thy = fun base_default_term thy cid_long = Const(@{const_name "undefined"},cid_2_cidType thy cid_long) -fun check_classref is_monitor (SOME(cid,pos')) thy = +fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy = let val cid_long = DOF_core.read_cid_global thy cid @@ -1149,7 +1135,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = rejected_cids=rejected_cids, automatas=aS}) tab end fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans mon_oid) - val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) + val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) in thy |> (* update traces of all enabled monitors *) fold (update_trace) (enabled_monitors) |> (* check class invariants of enabled monitors *) @@ -1159,7 +1145,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy = end -fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = +fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy = let val id = serial (); val _ = Position.report pos (docref_markup true oid id pos); (* creates a markup label for this position and reports it to the PIDE framework; @@ -1172,11 +1158,12 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy = fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs) val assns' = map conv_attrs doc_attrs val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults - val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=is_monitor}) + val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor) o Context.Theory in thy |> DOF_core.define_object_global (oid, {pos = pos, thy_name = Context.theory_name thy, value = value_term, + inline = is_inline, id = id, cid = cid_long}) |> register_oid_cid_in_open_monitors oid pos cid_long @@ -1195,7 +1182,7 @@ fun update_instance_command (((oid:string,pos),cid_pos), val _ = Context_Position.report ctxt pos markup; in cid end | NONE => error("undefined doc_class.") - val cid_long = check_classref false cid_pos thy + val cid_long = check_classref {is_monitor = false} cid_pos thy val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long then () else error("incompatible classes:"^cid^":"^cid_long) @@ -1214,29 +1201,37 @@ fun update_instance_command (((oid:string,pos),cid_pos), -fun gen_enriched_document_command cid_transform attr_transform +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 - (* as side-effect, generates markup *) - fun check_text thy = (Pure_Syn_Ext.output_document(Toplevel.theory_toplevel thy) markdown toks; - thy) + let val toplvl = Toplevel.theory_toplevel + (* checking and markup generation *) + fun check thy = let val ctxt = Toplevel.presentation_context (toplvl thy); + val _ = Context_Position.report ctxt + (Input.pos_of toks) + (Markup.language_document (Input.is_delimited toks)); + in thy end + (* ... generating the level-attribute syntax *) in - ( create_and_check_docitem false oid pos (cid_transform cid_pos) (attr_transform doc_attrs) - #> check_text) + ( create_and_check_docitem {is_monitor=false} {is_inline=is_inline} + oid pos (cid_transform cid_pos) (attr_transform doc_attrs) + #> check ) (* Thanks Frederic Tuong! ! ! *) end; + (* General criticism : attributes like "level" were treated here in the kernel instead of dragging them out into the COL -- bu *) fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) = let fun o_m_c oid pos cid_pos doc_attrs thy = create_and_check_docitem - true oid pos cid_pos doc_attrs thy + {is_monitor=true} (* this is a monitor *) + {is_inline=false} (* monitors are always inline *) + oid pos cid_pos doc_attrs thy fun compute_enabled_set cid thy = case DOF_core.get_doc_class_global cid thy of SOME X => let val ralph = RegExpInterface.alphabet (#rejectS X) @@ -1301,13 +1296,15 @@ val _ = val _ = Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" (attributes -- Parse.opt_target -- Parse.document_source - >> (Toplevel.theory o (gen_enriched_document_command I I {markdown = true} ))); + >> (Toplevel.theory o (gen_enriched_document_command {inline=true} + I I {markdown = true} ))); (* 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_command I I {markdown = true} ))); + >> (Toplevel.theory o (gen_enriched_document_command {inline=false} (* declare as macro *) + I I {markdown = true} ))); val _ = Outer_Syntax.command @{command_keyword "declare_reference*"} @@ -1455,12 +1452,15 @@ struct val basic_entity = Thy_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}) pos name = +fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) {inline=inline_req} pos name = let val thy = Proof_Context.theory_of ctxt; in if DOF_core.is_defined_oid_global name thy - then let val {pos=pos_decl,id,cid,...} = the(DOF_core.get_object_global name thy) + then let val {pos=pos_decl,id,cid,inline,...} = the(DOF_core.get_object_global name thy) + val _ = if not inline_req + then if inline then () else error("referred text-element is macro! (try option display)") + else if not inline then () else error("referred text-element is no macro!") val markup = docref_markup false name id pos_decl; val _ = Context_Position.report ctxt pos markup; (* this sends a report for a ref application to the PIDE interface ... *) @@ -1476,7 +1476,8 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = else error("undefined document reference: "^name) end -val _ = check_and_mark : Proof.context -> string -> {strict_checking: bool} -> +val _ = check_and_mark : Proof.context -> string -> + {strict_checking: bool} -> {inline:bool} -> Position.T -> Symtab.key -> unit (* generic syntax for doc_class links. *) @@ -1497,8 +1498,9 @@ val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Args.text_input) fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src ) = let val (str,pos) = Input.source_content src - val _ = check_and_mark ctxt cid_decl ({strict_checking = not unchecked}) pos str 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 @@ -1673,8 +1675,6 @@ fun read_fields raw_fields ctxt = let val Ts = Syntax.read_typs ctxt (map (fn ((_, raw_T, _),_) => raw_T) raw_fields); val terms = map ((map_option (Syntax.read_term ctxt)) o snd) raw_fields - val count = Unsynchronized.ref (0 - 1); - fun incr () = Unsynchronized.inc count fun test t1 t2 = Sign.typ_instance (Proof_Context.theory_of ctxt) (t1, ODL_Command_Parser.generalize_typ 0 t2) fun check_default (ty,SOME trm) = @@ -1740,7 +1740,7 @@ fun add_doc_class_cmd overloaded (raw_params, binding) fun check_n_filter thy (bind,ty,mf) = case DOF_core.get_attribute_info parent_cid_long (Binding.name_of bind) thy of NONE => (* no prior declaration *) SOME(bind,ty,mf) - | SOME{def_occurrence,long_name,typ,def_pos} => if ty = typ + | SOME{def_occurrence,long_name,typ,...} => if ty = typ then (warning("overriding attribute:"^long_name^ " in doc class:" ^ def_occurrence); SOME(bind,ty,mf)) diff --git a/src/DOF/RegExpInterface.thy b/src/DOF/RegExpInterface.thy old mode 100644 new mode 100755 diff --git a/src/DOF/latex/DOF-COL.sty b/src/DOF/latex/DOF-COL.sty old mode 100644 new mode 100755 diff --git a/src/DOF/latex/DOF-core.sty b/src/DOF/latex/DOF-core.sty old mode 100644 new mode 100755 diff --git a/src/ROOT b/src/ROOT old mode 100644 new mode 100755 diff --git a/src/ROOTS b/src/ROOTS old mode 100644 new mode 100755 diff --git a/src/SI/Groups_mult.thy b/src/SI/Groups_mult.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ.thy b/src/SI/ISQ.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Algebra.thy b/src/SI/ISQ_Algebra.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Dimensions.thy b/src/SI/ISQ_Dimensions.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Proof.thy b/src/SI/ISQ_Proof.thy old mode 100644 new mode 100755 diff --git a/src/SI/ISQ_Quantities.thy b/src/SI/ISQ_Quantities.thy old mode 100644 new mode 100755 diff --git a/src/SI/ROOT b/src/SI/ROOT old mode 100644 new mode 100755 diff --git a/src/SI/SI.thy b/src/SI/SI.thy old mode 100644 new mode 100755 diff --git a/src/SI/SIOld.thy b/src/SI/SIOld.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Accepted.thy b/src/SI/SI_Accepted.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Astronomical.thy b/src/SI/SI_Astronomical.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Constants.thy b/src/SI/SI_Constants.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Derived.thy b/src/SI/SI_Derived.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Imperial.thy b/src/SI/SI_Imperial.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Prefix.thy b/src/SI/SI_Prefix.thy old mode 100644 new mode 100755 diff --git a/src/SI/SI_Units.thy b/src/SI/SI_Units.thy old mode 100644 new mode 100755 diff --git a/src/SI/document/adb-long.bib b/src/SI/document/adb-long.bib old mode 100644 new mode 100755 diff --git a/src/SI/document/root.bib b/src/SI/document/root.bib old mode 100644 new mode 100755 diff --git a/src/SI/document/root.tex b/src/SI/document/root.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-eptcs-UNSUPPORTED.tex b/src/document-templates/root-eptcs-UNSUPPORTED.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex b/src/document-templates/root-lipics-v2019-UNSUPPORTED.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-lncs.tex b/src/document-templates/root-lncs.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrartcl.tex b/src/document-templates/root-scrartcl.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrreprt-modern.tex b/src/document-templates/root-scrreprt-modern.tex old mode 100644 new mode 100755 diff --git a/src/document-templates/root-scrreprt.tex b/src/document-templates/root-scrreprt.tex old mode 100644 new mode 100755 diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty b/src/ontologies/CENELEC_50128/DOF-CENELEC_50128.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/DOF-math_exam.sty b/src/ontologies/math_exam/DOF-math_exam.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/Nmath_exam.thy b/src/ontologies/math_exam/Nmath_exam.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_exam/math_exam.thy b/src/ontologies/math_exam/math_exam.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/math_paper/math_paper.thy b/src/ontologies/math_paper/math_paper.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/ontologies.thy b/src/ontologies/ontologies.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty b/src/ontologies/scholarly_paper/DOF-scholarly_paper.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy old mode 100644 new mode 100755 diff --git a/src/ontologies/technical_report/DOF-technical_report.sty b/src/ontologies/technical_report/DOF-technical_report.sty old mode 100644 new mode 100755 diff --git a/src/ontologies/technical_report/technical_report.thy b/src/ontologies/technical_report/technical_report.thy old mode 100644 new mode 100755 diff --git a/src/patches/thy_output.Isabelle2020.ML b/src/patches/thy_output.Isabelle2020.ML old mode 100644 new mode 100755 diff --git a/src/patches/thy_output.ML b/src/patches/thy_output.ML old mode 100644 new mode 100755 diff --git a/src/tests/AssnsLemmaThmEtc.thy b/src/tests/AssnsLemmaThmEtc.thy old mode 100644 new mode 100755 diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy old mode 100644 new mode 100755 diff --git a/src/tests/Concept_Example.thy b/src/tests/Concept_Example.thy old mode 100644 new mode 100755 diff --git a/src/tests/Concept_ExampleInvariant.thy b/src/tests/Concept_ExampleInvariant.thy old mode 100644 new mode 100755 diff --git a/src/tests/InnerSyntaxAntiquotations.thy b/src/tests/InnerSyntaxAntiquotations.thy old mode 100644 new mode 100755 diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy new file mode 100644 index 0000000..3335a4f --- /dev/null +++ b/src/tests/OutOfOrderPresntn.thy @@ -0,0 +1,101 @@ +(************************************************************************* + * Copyright (C) + * 2019 The University of Exeter + * 2018-2019 The University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + +theory + OutOfOrderPresntn +imports + "Isabelle_DOF.Conceptual" +keywords "text-" :: document_body +begin + +section\Elementary Creation of Doc-items and Access of their Attibutes\ + + +text\Current status:\ +print_doc_classes +print_doc_items + +(* this corresponds to low-level accesses : *) +ML\ +val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} + = DOF_core.get_data @{context}; +Symtab.dest docitem_tab; +Symtab.dest docclass_tab; +\ + + + +ML\ +Pure_Syn.document_command; + +fun output_document state markdown src = + let + val ctxt = Toplevel.presentation_context state; + val _ = Context_Position.report ctxt + (Input.pos_of src) + (Markup.language_document (Input.is_delimited src)); + in Thy_Output.output_document ctxt markdown src end; + (* this thing converts also source to (latex) text ... *) + +output_document : Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list; + + +fun gen_enriched_document_command2 cid_transform attr_transform + markdown + (((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.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 text = output_document (toplvl 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 + ( ODL_Command_Parser.create_and_check_docitem + {is_monitor = false} {is_inline = false} + oid pos (cid_transform cid_pos) (attr_transform doc_attrs) + #> check_n_tex_text ) + end; + +val _ = + Outer_Syntax.command ("text-", @{here}) "formal comment macro" + (ODL_Command_Parser.attributes -- Parse.opt_target -- Parse.document_source + >> (Toplevel.theory o (gen_enriched_document_command2 I I {markdown = true} ))); + +\ + + +text\And here a tex - text macro.\ + +text-[dfgdfg::B]\ Lorem ipsum ... @{thm refl} \ + +text\... and here is its application /macro expansion: + @{B [display] "dfgdfg"}\ + + + +(*<*) +text\Final Status:\ +print_doc_items +print_doc_classes + +end +(*>*) diff --git a/src/tests/ROOT b/src/tests/ROOT old mode 100644 new mode 100755 diff --git a/src/tests/figures/A.png b/src/tests/figures/A.png old mode 100644 new mode 100755 diff --git a/src/tests/figures/AnB.odp b/src/tests/figures/AnB.odp old mode 100644 new mode 100755 diff --git a/src/tests/figures/B.png b/src/tests/figures/B.png old mode 100644 new mode 100755