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

macro-arrangement ...

This commit is contained in:
Burkhart Wolff 2020-11-02 18:30:40 +01:00
parent e59ac46299
commit fe8f63690d
3 changed files with 36 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
examples/scholarly_paper/2020-iFM-CSP/paper.thy
View File

@ -20,11 +20,11 @@ text*[safouan::author, email="''safouan.taha@lri.fr''", affiliation="\<open>LRI,
\<open>Safouan Taha\<close>
text*[bu::author, email= "''wolff@lri.fr''",affiliation = "\<open>LRI, Université Paris-Saclay\<close>"]
\<open>Burkhart Wolff\<close>
text*[lina:: author,email="''lina.ye@lri.fr''", affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]
text*[lina::author,email="''lina.ye@lri.fr''", affiliation="\<open>LRI, Inria, LSV, CentraleSupelec\<close>"]
\<open>Lina Ye\<close>
text*[abs::abstract,
keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,\<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
text*[abs::abstract, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
\<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
\<open> 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

11
src/DOF/Isa_COL.thy
View File

@ -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) =

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

@ -15,7 +15,8 @@ section\<open>An example ontology for a scholarly paper\<close>
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\<open>
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
\<close>
text\<open>Scholarly Paper is oriented towards the classical domains in science:
\<^enum> mathematics
\<^enum> informatics