From da0f3e63f139bb577b952158074c8cb7b41b6b25 Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 4 Nov 2020 13:13:24 +0100 Subject: [PATCH] more steps to reform document macro mechanism --- .../Isabelle_DOF-Manual/04_RefMan.thy | 3 +- src/DOF/Isa_COL.thy | 68 ++++++++++++------- src/DOF/Isa_DOF.thy | 9 ++- .../scholarly_paper/scholarly_paper.thy | 6 +- 4 files changed, 51 insertions(+), 35 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 3bf61a2..4f6b1e0 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -382,10 +382,11 @@ FORMAL_STATEMENT_ALIKE = \} These shadow-classes correspond to semantic macros - \<^ML>\Onto_Macros.enriched_document_command\, + \<^ML>\Onto_Macros.enriched_document_cmd_exp\, \<^ML>\Onto_Macros.assertion_cmd'\, and \<^ML>\Onto_Macros.enriched_formal_statement_command\.\ + text\ \<^isadof> provides a Common Ontology Library (COL)\<^index>\Common Ontology Library@see COL\ \<^bindex>\COL\ that introduces ontology concepts that are either sample instances for shadow classes as we use them in our own document generation processes or, in some cases, are diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 40f1181..1259100 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -75,34 +75,50 @@ local open ODL_Command_Parser in accepted. *) -fun enriched_document_command level = +fun enriched_text_element_cmd level = let fun transform doc_attrs = case level of 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 {inline=true} I transform end; + in gen_enriched_document_cmd {inline=true} I transform end; +(* val enriched_document_command_macro = let fun transform_cid X = (writeln (@{make_string} X); X) in gen_enriched_document_command {inline=true} transform_cid I end; +*) +local +fun transform_cid thy NONE X = X + |transform_cid thy (SOME ncid) NONE = (SOME(ncid,@{here})) + |transform_cid thy (SOME cid) (SOME (sub_cid,pos)) = + let val cid_long = DOF_core.read_cid_global thy cid + val sub_cid_long = DOF_core.read_cid_global thy sub_cid + in if DOF_core.is_subclass_global thy sub_cid_long cid_long + then (SOME (sub_cid,pos)) + else (SOME (sub_cid,pos)) + (* BUG : check does not yet work for + type synonyms. + error("class must be sub-class of "^cid) *) + end +in + fun enriched_formal_statement_command ncid (S: (string * string) list) = - let val transform_cid = case ncid of NONE => I - | SOME(ncid) => - (fn X => case X of NONE => (SOME(ncid,@{here})) - | _ => 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 {inline=true} transform_cid transform_attr end; - -fun enriched_formal_statement_command0 ncid (S: (string * string) list) = - let fun transform_cid NONE X = X - |transform_cid (SOME ncid) NONE = (SOME(ncid,@{here})) - |transform_cid (SOME _) (SOME cid) = (SOME cid) - fun transform_attr attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ attrs - in gen_enriched_document_command {inline=true} (transform_cid ncid) transform_attr end; + 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 => + gen_enriched_document_cmd {inline=true} + (transform_cid thy ncid) transform_attr md 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 + end; +end (* local *) fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), prop) = @@ -132,43 +148,43 @@ val _ = val _ = Outer_Syntax.command ("title*", @{here}) "section heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_document_command NONE {markdown = false} ))) ; + >> (Toplevel.theory o (enriched_text_element_cmd NONE {markdown = false} ))) ; val _ = Outer_Syntax.command ("subtitle*", @{here}) "section heading" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (enriched_document_command NONE {markdown = false} ))); + >> (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_document_command (SOME(SOME 0)) {markdown = false} ))); + >> (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_document_command (SOME(SOME 1)) {markdown = false} ))); + >> (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_document_command (SOME(SOME 2)) {markdown = false} ))); + >> (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_document_command (SOME(SOME 3)) {markdown = false} ))); + >> (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_document_command (SOME(SOME 4)) {markdown = false} ))); + >> (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_document_command (SOME(SOME 5)) {markdown = false} ))); + >> (Toplevel.theory o (enriched_text_element_cmd (SOME(SOME 5)) {markdown = false} ))); end end @@ -223,12 +239,12 @@ ML\ local open ODL_Command_Parser in val _ = Outer_Syntax.command ("figure*", @{here}) "figure" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (Onto_Macros.enriched_document_command NONE {markdown = false} ))); + >> (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_document_command NONE {markdown = false} ))); + >> (Toplevel.theory o (Onto_Macros.enriched_text_element_cmd NONE {markdown = false} ))); diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index ee14601..8d7a1fc 100755 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -1255,7 +1255,7 @@ fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transfor end; *) -fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transform +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), @@ -1368,15 +1368,14 @@ 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 {inline=true} - I I {markdown = true} ))); + >> (Toplevel.theory o (gen_enriched_document_cmd {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 {inline=false} (* declare as macro *) - I I {markdown = true} ))); + >> (Toplevel.theory o (gen_enriched_document_cmd {inline=false} (* declare as macro *) + I I {markdown = true} ))); val _ = Outer_Syntax.command @{command_keyword "declare_reference*"} diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 1357c62..2286221 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -49,7 +49,7 @@ 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_formal_statement_command0 + >> (Toplevel.theory o (Onto_Macros.enriched_document_cmd_exp (SOME "abstract") [] {markdown = true} ))); @@ -57,7 +57,7 @@ val _ = Outer_Syntax.command ("abstract*", @{here}) "Textual Definition" val _ = Outer_Syntax.command ("author*", @{here}) "Textual Definition" (attributes -- Parse.opt_target -- Parse.document_source --| semi - >> (Toplevel.theory o (Onto_Macros.enriched_formal_statement_command0 + >> (Toplevel.theory o (Onto_Macros.enriched_document_cmd_exp (SOME "author") [] {markdown = true} ))); @@ -456,8 +456,8 @@ subsection\Common Abbreviations\ setup \ DOF_lib.define_shortcut \<^binding>\eg\ "\\eg" (* Latin: „exempli gratia“ meaning „for example“. *) #> DOF_lib.define_shortcut \<^binding>\ie\ "\\ie" - #> DOF_lib.define_shortcut \<^binding>\etc\ "\\etc"\ (* Latin: „id est“ meaning „that is to say“. *) + #> DOF_lib.define_shortcut \<^binding>\etc\ "\\etc"\ (* this is an alternative style for macro definitions equivalent to setup ... setup ...*)