nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

re-localization of onto macros. Tested.

This commit is contained in:
Burkhart Wolff 2020-04-23 18:30:46 +02:00
parent 6f8cd88623
commit fa931b45e2
4 changed files with 146 additions and 117 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

85
src/DOF/Isa_COL.thy
View File

@ -19,6 +19,13 @@ text\<open> Building a fundamental infrastructure for common document elements s
theory Isa_COL
imports Isa_DOF
keywords "title*" "subtitle*"
"chapter*" "section*" "subsection*" "subsubsection*"
"paragraph*" "subparagraph*" :: document_body
and "figure*" "side_by_side_figure*" :: document_body
begin
section\<open>Basic Text and Text-Structuring Elements\<close>
@ -49,6 +56,60 @@ doc_class "subsubsection" = text_element +
level :: "int option" <= "Some 3"
subsection\<open>Ontological Macros\<close>
ML\<open> local open ODL_Command_Parser in
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
(* {markdown = true} sets the parsing process such that in the text-core markdown elements are
accepted. *)
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} ))) ;
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} )));
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} )));
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} )));
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} )));
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} )));
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} )));
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} )));
end
\<close>
section\<open> Library of Standard Text Ontology \<close>
datatype placement = pl_h | (*here*)
@ -88,6 +149,28 @@ doc_class figure_group =
print_doc_classes
subsection\<open>Ontological Macros\<close>
ML\<open> local open ODL_Command_Parser in
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
val _ =
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command 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 (enriched_document_command NONE {markdown = false} )));
end
\<close>
section\<open>Tables\<close>
(* TODO ! ! ! *)
@ -101,6 +184,8 @@ ML\<open>@{term "side_by_side_figure"};
DOF_core.SPY;
\<close>
section\<open>DEPRECATED : An attempt to model Standard Isabelle Formal Content\<close>
doc_class assertions =

139
src/DOF/Isa_DOF.thy
View File

@ -35,24 +35,19 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
Assert
keywords "+=" ":=" "accepts" "rejects" "invariant"
and "title*" "subtitle*"
"chapter*" "section*" "subsection*" "subsubsection*"
"paragraph*" "subparagraph*"
"text*" "text-macro*"
"figure*"
"side_by_side_figure*"
"Definition*" "Lemma*" "Theorem*"
:: document_body
and "open_monitor*" "close_monitor*" "declare_reference*"
"update_instance*" "doc_class" ::thy_decl
and (* "definition*" *) "corrollary*" "proposition*" "schematic_goal*"
and "text*" "text-macro*" :: document_body
and "print_doc_classes" "print_doc_items" "check_doc_global" :: diag
(* experimental *)
and "corrollary*" "proposition*" "schematic_goal*"
"lemma*" "theorem*" (* -- intended replacement of Isar std commands.*)
"assert*" ::thy_decl
and "print_doc_classes" "print_doc_items" "check_doc_global" :: diag
begin
@ -1246,7 +1241,7 @@ val enriched_document_command_macro = enriched_document_command (* TODO ... *)
fun enriched_formal_statement_command (cat:string,tag:string) =
let fun transform doc_attrs = (("mcc",@{here}),tag) ::
let fun transform doc_attrs = ((cat,@{here}),tag) ::
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
in gen_enriched_document_command transform end;
@ -1312,105 +1307,8 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|> delete_monitor_entry
end
end
\<close>
(* Core Command Definitions *)
ML\<open>
structure Macros =
struct
local open ODL_Command_Parser in
(* *********************************************************************** *)
(* Textual Command Support *)
(* *********************************************************************** *)
(* {markdown = true} sets the parsing process such that in the text-core markdown elements are
accepted. *)
val _ =
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","defn") {markdown = true} )));
val _ =
Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","lem") {markdown = true} )));
val _ =
Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","thm") {markdown = true} )));
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} ))) ;
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} )));
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} )));
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} )));
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} )));
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} )));
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} )));
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} )));
val _ =
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_document_command 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 (enriched_document_command NONE {markdown = false} )));
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (enriched_document_command NONE {markdown = true} )));
val _ =
Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro"
(attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (enriched_document_command_macro NONE {markdown = true} )));
val _ =
Outer_Syntax.command @{command_keyword "declare_reference*"}
"declare document reference"
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
(Toplevel.theory (DOF_core.declare_object_global oid))));
val _ =
Outer_Syntax.command @{command_keyword "open_monitor*"}
@ -1429,15 +1327,32 @@ val _ =
(attributes_upd >> (Toplevel.theory o update_instance_command));
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (enriched_document_command NONE {markdown = true} )));
val _ =
Outer_Syntax.command ("text-macro*", @{here}) "formal comment macro"
(attributes -- Parse.opt_target -- Parse.document_source
>> (Toplevel.theory o (enriched_document_command_macro NONE {markdown = true} )));
val _ =
Outer_Syntax.command @{command_keyword "declare_reference*"}
"declare document reference"
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
(Toplevel.theory (DOF_core.declare_object_global oid))));
val _ =
Outer_Syntax.command @{command_keyword "assert*"}
"evaluate and print term"
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');
end
end (* struct *)
end
\<close>
ML\<open>
structure ODL_LTX_Converter =
struct

4
src/ontologies/math_paper/math_paper.thy
View File

@ -26,8 +26,8 @@ proving environment after all ! So this ontology provides:
theory math_paper
imports "../../DOF/Isa_DOF"
begin
begin
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>

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

@ -14,7 +14,10 @@
section\<open>An example ontology for a scholarly paper\<close>
theory scholarly_paper
imports "../../DOF/Isa_COL"
imports "../../DOF/Isa_COL"
keywords "Definition*" "Lemma*" "Theorem*" :: document_body
begin
text\<open>Scholarly Paper provides a number of standard text - elements for scientific papers.
@ -192,7 +195,7 @@ type_synonym math_sfc = math_semiformal
subsection\<open>Instances of the abstract classes Definition / Class / Lemma etc.\<close>
text\<open>The key class definitions are motivated \<close>
text\<open>The key class definitions are motivated by the AMS style.\<close>
doc_class "definition" = math_content +
referentiable :: bool <= True
@ -204,7 +207,6 @@ doc_class "theorem" = math_content +
mcc :: "math_content_class" <= "thm"
invariant d2 :: "\<lambda> \<sigma>::theorem. mcc \<sigma> = thm"
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
doc_class "lemma" = math_content +
referentiable :: bool <= "True"
mcc :: "math_content_class" <= "lem"
@ -220,6 +222,32 @@ doc_class "math_example" = math_content +
mcc :: "math_content_class" <= "expl"
invariant d5 :: "\<lambda> \<sigma>::math_example. mcc \<sigma> = expl"
subsection\<open>Ontological Macros\<close>
ML\<open> local open ODL_Command_Parser in
(* *********************************************************************** *)
(* Ontological Macro Command Support *)
(* *********************************************************************** *)
(* {markdown = true} sets the parsing process such that in the text-core markdown elements are
accepted. *)
val _ =
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","defn") {markdown = true} )));
val _ =
Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","lem") {markdown = true} )));
val _ =
Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","thm") {markdown = true} )));
end
\<close>
subsection\<open>Example Statements\<close>
@ -402,5 +430,6 @@ fun check_group a = map (check_group_elem (check_level_hd (hd a))) (tl a) ;
\<close>
end