Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

more steps to reform document macro mechanism

This commit is contained in:
Burkhart Wolff 2020-11-04 13:13:24 +01:00
parent 7f4b587274
commit da0f3e63f1
4 changed files with 51 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -382,10 +382,11 @@ FORMAL_STATEMENT_ALIKE =
\<close>} \<close>}
These shadow-classes correspond to semantic macros These shadow-classes correspond to semantic macros
\<^ML>\<open>Onto_Macros.enriched_document_command\<close>, \<^ML>\<open>Onto_Macros.enriched_document_cmd_exp\<close>,
\<^ML>\<open>Onto_Macros.assertion_cmd'\<close>, and \<^ML>\<open>Onto_Macros.assertion_cmd'\<close>, and
\<^ML>\<open>Onto_Macros.enriched_formal_statement_command\<close>.\<close> \<^ML>\<open>Onto_Macros.enriched_formal_statement_command\<close>.\<close>
text\<open> \<^isadof> provides a Common Ontology Library (COL)\<^index>\<open>Common Ontology Library@see COL\<close> text\<open> \<^isadof> provides a Common Ontology Library (COL)\<^index>\<open>Common Ontology Library@see COL\<close>
\<^bindex>\<open>COL\<close> that introduces ontology concepts that are either sample instances for shadow \<^bindex>\<open>COL\<close> 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 classes as we use them in our own document generation processes or, in some cases, are

68
src/DOF/Isa_COL.thy
View File

@ -75,34 +75,50 @@ local open ODL_Command_Parser in
accepted. *) accepted. *)
fun enriched_document_command level = fun enriched_text_element_cmd level =
let fun transform doc_attrs = case level of let fun transform doc_attrs = case level of
NONE => doc_attrs NONE => doc_attrs
| SOME(NONE) => (("level",@{here}),"None")::doc_attrs | SOME(NONE) => (("level",@{here}),"None")::doc_attrs
| SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::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 = val enriched_document_command_macro =
let fun transform_cid X = (writeln (@{make_string} X); X) let fun transform_cid X = (writeln (@{make_string} X); X)
in gen_enriched_document_command {inline=true} transform_cid I end; 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) = fun enriched_formal_statement_command ncid (S: (string * string) list) =
let val transform_cid = case ncid of NONE => I let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @
| SOME(ncid) => (("formal_results",@{here}),"([]::thm list)")::doc_attrs
(fn X => case X of NONE => (SOME(ncid,@{here})) in fn md => fn margs => fn thy =>
| _ => X) gen_enriched_document_cmd {inline=true}
fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ (transform_cid thy ncid) transform_attr md margs thy
(("formal_results",@{here}),"([]::thm list)")::doc_attrs end;
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;
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), fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list),
prop) = prop) =
@ -132,43 +148,43 @@ val _ =
val _ = val _ =
Outer_Syntax.command ("title*", @{here}) "section heading" Outer_Syntax.command ("title*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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 _ = val _ =
Outer_Syntax.command ("subtitle*", @{here}) "section heading" Outer_Syntax.command ("subtitle*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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 _ = val _ =
Outer_Syntax.command ("chapter*", @{here}) "section heading" Outer_Syntax.command ("chapter*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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 _ = val _ =
Outer_Syntax.command ("section*", @{here}) "section heading" Outer_Syntax.command ("section*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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 _ = val _ =
Outer_Syntax.command ("subsection*", @{here}) "subsection heading" Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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 _ = val _ =
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading" Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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 _ = val _ =
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading" Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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 _ = val _ =
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading" Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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
end end
@ -223,12 +239,12 @@ ML\<open> local open ODL_Command_Parser in
val _ = val _ =
Outer_Syntax.command ("figure*", @{here}) "figure" Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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 _ = val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures" Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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} )));

9
src/DOF/Isa_DOF.thy
View File

@ -1255,7 +1255,7 @@ fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transfor
end; 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 markdown
(((((oid,pos),cid_pos), doc_attrs) : meta_args_t, (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
xstring_opt:(xstring * Position.T) option), xstring_opt:(xstring * Position.T) option),
@ -1368,15 +1368,14 @@ val _ =
val _ = val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)" Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source (attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (gen_enriched_document_command {inline=true} >> (Toplevel.theory o (gen_enriched_document_cmd {inline=true} I I {markdown = true} )));
I I {markdown = true} )));
(* This is just a stub at present *) (* This is just a stub at present *)
val _ = val _ =
Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro" Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro"
(attributes -- Parse.opt_target -- Parse.document_source (attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (gen_enriched_document_command {inline=false} (* declare as macro *) >> (Toplevel.theory o (gen_enriched_document_cmd {inline=false} (* declare as macro *)
I I {markdown = true} ))); I I {markdown = true} )));
val _ = val _ =
Outer_Syntax.command @{command_keyword "declare_reference*"} Outer_Syntax.command @{command_keyword "declare_reference*"}

6
src/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -49,7 +49,7 @@ ML\<open>
local open ODL_Command_Parser in local open ODL_Command_Parser in
val _ = Outer_Syntax.command ("abstract*", @{here}) "Textual Definition" val _ = Outer_Syntax.command ("abstract*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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") (SOME "abstract")
[] []
{markdown = true} ))); {markdown = true} )));
@ -57,7 +57,7 @@ val _ = Outer_Syntax.command ("abstract*", @{here}) "Textual Definition"
val _ = Outer_Syntax.command ("author*", @{here}) "Textual Definition" val _ = Outer_Syntax.command ("author*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi (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") (SOME "author")
[] []
{markdown = true} ))); {markdown = true} )));
@ -456,8 +456,8 @@ subsection\<open>Common Abbreviations\<close>
setup \<open> DOF_lib.define_shortcut \<^binding>\<open>eg\<close> "\\eg" setup \<open> DOF_lib.define_shortcut \<^binding>\<open>eg\<close> "\\eg"
(* Latin: „exempli gratia“ meaning „for example“. *) (* Latin: „exempli gratia“ meaning „for example“. *)
#> DOF_lib.define_shortcut \<^binding>\<open>ie\<close> "\\ie" #> DOF_lib.define_shortcut \<^binding>\<open>ie\<close> "\\ie"
#> DOF_lib.define_shortcut \<^binding>\<open>etc\<close> "\\etc"\<close>
(* Latin: „id est“ meaning „that is to say“. *) (* Latin: „id est“ meaning „that is to say“. *)
#> DOF_lib.define_shortcut \<^binding>\<open>etc\<close> "\\etc"\<close>
(* this is an alternative style for macro definitions equivalent to setup ... setup ...*) (* this is an alternative style for macro definitions equivalent to setup ... setup ...*)