diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index c35d15a..64b5d21 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -20,11 +20,11 @@ text*[safouan::author, email="''safouan.taha@lri.fr''", affiliation="\LRI, \Safouan Taha\ text*[bu::author, email= "''wolff@lri.fr''",affiliation = "\LRI, Université Paris-Saclay\"] \Burkhart Wolff\ -text*[lina:: author,email="''lina.ye@lri.fr''", affiliation="\LRI, Inria, LSV, CentraleSupelec\"] +text*[lina::author,email="''lina.ye@lri.fr''", affiliation="\LRI, Inria, LSV, CentraleSupelec\"] \Lina Ye\ -text*[abs::abstract, - keywordlist="[\Shallow Embedding\,\Process-Algebra\,\Concurrency\,\Computational Models\]"] +text*[abs::abstract, keywordlist="[\Shallow Embedding\,\Process-Algebra\, + \Concurrency\,\Computational Models\]"] \ The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today one of the reference theories for concurrent specification and computing. In 1997, a first formalization in \<^isabelle> of the denotational semantics of the diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 07c7622..ed655c3 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -82,7 +82,9 @@ fun enriched_document_command level = | SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs in gen_enriched_document_command {inline=true} I transform end; -val enriched_document_command_macro = enriched_document_command (* TODO ... *) +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; fun enriched_formal_statement_command ncid (S: (string * string) list) = @@ -94,6 +96,13 @@ fun enriched_formal_statement_command ncid (S: (string * string) list) = (("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 val transform_cid = case ncid of NONE => I + | SOME(ncid) => + (fn X => case X of NONE => (SOME(ncid,@{here})) + | _ => X) + in gen_enriched_document_command {inline=true} transform_cid I end; + fun assertion_cmd'((((((oid,pos),cid_pos),doc_attrs),name_opt:string option),modes : string list), prop) = diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 8c9668a..06f8433 100755 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -15,7 +15,8 @@ section\An example ontology for a scholarly paper\ theory scholarly_paper imports "../../DOF/Isa_COL" - keywords "Definition*" "Lemma*" "Theorem*" :: document_body + keywords "author*" "abstract*" + "Definition*" "Lemma*" "Theorem*" :: document_body begin @@ -43,6 +44,27 @@ doc_class abstract = keywordlist :: "string list" <= "[]" principal_theorems :: "thm list" + +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 + (SOME "abstract") + [] + {markdown = true} ))); + + +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 + (SOME "author") + [] + {markdown = true} ))); + +end +\ + text\Scholarly Paper is oriented towards the classical domains in science: \<^enum> mathematics \<^enum> informatics