forked from Isabelle_DOF/Isabelle_DOF
restructuring of COL, scholarly_paper, etc. Facturong out Macros.
This commit is contained in:
parent
c320b58dd3
commit
2e0d88a3f7
|
@ -13,39 +13,61 @@
|
||||||
|
|
||||||
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
|
chapter \<open>The Document Ontology Common Library for the Isabelle Ontology Framework\<close>
|
||||||
|
|
||||||
text\<open> Offering
|
text\<open> Building a fundamental infrastructure for common document elements such as
|
||||||
\<^item> ...
|
Structuring Text-Elements (the top classes), Figures, Tables (yet todo)
|
||||||
\<^item>
|
\<close>
|
||||||
\<^item> LaTeX support. \<close>
|
|
||||||
|
|
||||||
|
|
||||||
theory Isa_COL
|
theory Isa_COL
|
||||||
imports Isa_DOF
|
imports Isa_DOF
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
section\<open>Basic Text and Text-Structuring Elements\<close>
|
||||||
|
|
||||||
|
text\<open> The attribute @{term "level"} in the subsequent enables doc-notation support section* etc.
|
||||||
|
we follow LaTeX terminology on levels
|
||||||
|
\<^enum> part = Some -1
|
||||||
|
\<^enum> chapter = Some 0
|
||||||
|
\<^enum> section = Some 1
|
||||||
|
\<^enum> subsection = Some 2
|
||||||
|
\<^enum> subsubsection = Some 3
|
||||||
|
\<^enum> ...
|
||||||
|
|
||||||
|
for scholarly paper: invariant level > 0. \<close>
|
||||||
|
|
||||||
|
doc_class text_element =
|
||||||
|
level :: "int option" <= "None"
|
||||||
|
referentiable :: bool <= "False"
|
||||||
|
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
||||||
|
|
||||||
|
doc_class "chapter" = text_element +
|
||||||
|
level :: "int option" <= "Some 0"
|
||||||
|
doc_class "section" = text_element +
|
||||||
|
level :: "int option" <= "Some 1"
|
||||||
|
doc_class "subsection" = text_element +
|
||||||
|
level :: "int option" <= "Some 2"
|
||||||
|
doc_class "subsubsection" = text_element +
|
||||||
|
level :: "int option" <= "Some 3"
|
||||||
|
|
||||||
|
|
||||||
section\<open> Library of Standard Text Ontology \<close>
|
section\<open> Library of Standard Text Ontology \<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
datatype placement = pl_h | (*here*)
|
datatype placement = pl_h | (*here*)
|
||||||
pl_t | (*top*)
|
pl_t | (*top*)
|
||||||
pl_b | (*bottom*)
|
pl_b | (*bottom*)
|
||||||
pl_ht | (*here -> top*)
|
pl_ht | (*here -> top*)
|
||||||
pl_hb (*here -> bottom*)
|
pl_hb (*here -> bottom*)
|
||||||
|
|
||||||
|
ML\<open>(Symtab.defined (#docclass_tab(DOF_core.get_data_global @{theory}))) "side_by_side_figure"\<close>
|
||||||
|
|
||||||
|
print_doc_classes
|
||||||
|
|
||||||
|
|
||||||
doc_class figure =
|
doc_class figure =
|
||||||
relative_width :: "int" (* percent of textwidth *)
|
relative_width :: "int" (* percent of textwidth *)
|
||||||
src :: "string"
|
src :: "string"
|
||||||
placement :: placement
|
placement :: placement <= "pl_h"
|
||||||
spawn_columns :: bool <= True
|
spawn_columns :: bool <= True
|
||||||
|
|
||||||
ML\<open>(Symtab.defined (#docclass_tab(DOF_core.get_data_global @{theory}))) "side_by_side_figure"\<close>
|
|
||||||
|
|
||||||
|
|
||||||
print_doc_classes
|
|
||||||
|
|
||||||
doc_class side_by_side_figure = figure +
|
doc_class side_by_side_figure = figure +
|
||||||
anchor :: "string"
|
anchor :: "string"
|
||||||
|
@ -57,7 +79,6 @@ doc_class side_by_side_figure = figure +
|
||||||
|
|
||||||
print_doc_classes
|
print_doc_classes
|
||||||
|
|
||||||
|
|
||||||
doc_class figure_group =
|
doc_class figure_group =
|
||||||
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
|
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
|
||||||
caption :: "string"
|
caption :: "string"
|
||||||
|
@ -67,31 +88,22 @@ doc_class figure_group =
|
||||||
|
|
||||||
print_doc_classes
|
print_doc_classes
|
||||||
|
|
||||||
|
section\<open>Tables\<close>
|
||||||
(* dito the future table *)
|
(* TODO ! ! ! *)
|
||||||
|
|
||||||
(* dito the future monitor: table - block *)
|
(* dito the future monitor: table - block *)
|
||||||
|
|
||||||
|
|
||||||
text\<open> The attribute @{term "level"} in the subsequent enables doc-notation support section* etc.
|
section\<open>Tests\<close>
|
||||||
we follow LaTeX terminology on levels
|
|
||||||
\<^enum> part = Some -1
|
ML\<open>@{term "side_by_side_figure"};
|
||||||
\<^enum> chapter = Some 0
|
@{typ "doc_class rexp"};
|
||||||
\<^enum> section = Some 1
|
DOF_core.SPY;
|
||||||
\<^enum> subsection = Some 2
|
\<close>
|
||||||
\<^enum> subsubsection = Some 3
|
|
||||||
\<^enum> ...
|
|
||||||
|
|
||||||
for scholarly paper: invariant level > 0 \<close>
|
section\<open>DEPRECATED : An attempt to model Standard Isabelle Formal Content\<close>
|
||||||
|
|
||||||
doc_class text_element =
|
doc_class assertions =
|
||||||
level :: "int option" <= "None"
|
|
||||||
referentiable :: bool <= "False"
|
|
||||||
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
|
||||||
|
|
||||||
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
|
|
||||||
(* Deprecated *)
|
|
||||||
doc_class assertions =
|
|
||||||
properties :: "term list"
|
properties :: "term list"
|
||||||
|
|
||||||
doc_class "thms" =
|
doc_class "thms" =
|
||||||
|
@ -112,12 +124,5 @@ doc_class concept =
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
properties :: "thm list" <= "[]"
|
properties :: "thm list" <= "[]"
|
||||||
|
|
||||||
section\<open>Tests\<close>
|
|
||||||
|
|
||||||
ML\<open>@{term "side_by_side_figure"};
|
|
||||||
@{typ "doc_class rexp"};
|
|
||||||
DOF_core.SPY;
|
|
||||||
\<close>
|
|
||||||
|
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -42,7 +42,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||||
"text*" "text-macro*"
|
"text*" "text-macro*"
|
||||||
"figure*"
|
"figure*"
|
||||||
"side_by_side_figure*"
|
"side_by_side_figure*"
|
||||||
"Definition*" "Lemma*" "Theorem*" "Conjecture*"
|
"Definition*" "Lemma*" "Theorem*"
|
||||||
:: document_body
|
:: document_body
|
||||||
|
|
||||||
and "open_monitor*" "close_monitor*" "declare_reference*"
|
and "open_monitor*" "close_monitor*" "declare_reference*"
|
||||||
|
@ -1245,9 +1245,9 @@ fun enriched_document_command level =
|
||||||
val enriched_document_command_macro = enriched_document_command (* TODO ... *)
|
val enriched_document_command_macro = enriched_document_command (* TODO ... *)
|
||||||
|
|
||||||
|
|
||||||
fun enriched_formal_statement_command (tag:string) =
|
fun enriched_formal_statement_command (cat:string,tag:string) =
|
||||||
let fun transform doc_attrs = (("tag",@{here}),"''"^tag^"''") ::
|
let fun transform doc_attrs = (("mcc",@{here}),tag) ::
|
||||||
(("properties",@{here}),"([]::thm list)")::doc_attrs
|
(("formal_results",@{here}),"([]::thm list)")::doc_attrs
|
||||||
in gen_enriched_document_command transform end;
|
in gen_enriched_document_command transform end;
|
||||||
|
|
||||||
|
|
||||||
|
@ -1295,6 +1295,15 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
||||||
|> delete_monitor_entry
|
|> delete_monitor_entry
|
||||||
end
|
end
|
||||||
|
|
||||||
|
end
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
ML\<open>
|
||||||
|
|
||||||
|
structure Macros =
|
||||||
|
struct
|
||||||
|
|
||||||
|
local open ODL_Command_Parser in
|
||||||
(* *********************************************************************** *)
|
(* *********************************************************************** *)
|
||||||
(* Textual Command Support *)
|
(* Textual Command Support *)
|
||||||
(* *********************************************************************** *)
|
(* *********************************************************************** *)
|
||||||
|
@ -1305,22 +1314,17 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
||||||
val _ =
|
val _ =
|
||||||
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
|
Outer_Syntax.command ("Definition*", @{here}) "Textual Definition"
|
||||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||||
>> (Toplevel.theory o (enriched_formal_statement_command "definition" {markdown = true} )));
|
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","defn") {markdown = true} )));
|
||||||
|
|
||||||
val _ =
|
val _ =
|
||||||
Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
|
Outer_Syntax.command ("Lemma*", @{here}) "Textual Lemma Outline"
|
||||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||||
>> (Toplevel.theory o (enriched_formal_statement_command "lemma" {markdown = true} )));
|
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","lem") {markdown = true} )));
|
||||||
|
|
||||||
val _ =
|
val _ =
|
||||||
Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
|
Outer_Syntax.command ("Theorem*", @{here}) "Textual Theorem Outline"
|
||||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
||||||
>> (Toplevel.theory o (enriched_formal_statement_command "theorem" {markdown = true} )));
|
>> (Toplevel.theory o (enriched_formal_statement_command ("mcc","thm") {markdown = true} )));
|
||||||
|
|
||||||
val _ =
|
|
||||||
Outer_Syntax.command ("Conjecture*", @{here}) "Textual Theorem Outline"
|
|
||||||
(attributes -- Parse.opt_target -- Parse.document_source --| semi
|
|
||||||
>> (Toplevel.theory o (enriched_formal_statement_command "conjecture" {markdown = true} )));
|
|
||||||
|
|
||||||
|
|
||||||
val _ =
|
val _ =
|
||||||
|
@ -1429,7 +1433,7 @@ val _ =
|
||||||
"evaluate and print term"
|
"evaluate and print term"
|
||||||
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');
|
(attributes -- opt_evaluator -- opt_modes -- Parse.term >> assertion_cmd');
|
||||||
|
|
||||||
|
end
|
||||||
end (* struct *)
|
end (* struct *)
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
|
@ -106,17 +106,16 @@ text\<open>The class \<^verbatim>\<open>technical\<close> regroups a number of t
|
||||||
(* OPEN PROBLEM: connection between referentiable and status. This should be explicit
|
(* OPEN PROBLEM: connection between referentiable and status. This should be explicit
|
||||||
and computable. *)
|
and computable. *)
|
||||||
|
|
||||||
(* TODO : RENAME "tag" by "short_name" *)
|
|
||||||
|
|
||||||
doc_class technical = text_section +
|
doc_class technical = text_section +
|
||||||
definition_list :: "string list" <= "[]"
|
definition_list :: "string list" <= "[]"
|
||||||
status :: status <= "description"
|
status :: status <= "description"
|
||||||
formal_results :: "thm list"
|
formal_results :: "thm list"
|
||||||
|
invariant L1 :: "\<lambda>\<sigma>::technical. the (level \<sigma>) > 0"
|
||||||
|
|
||||||
type_synonym tc = technical (* technical content *)
|
type_synonym tc = technical (* technical content *)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
subsection\<open>Mathematical Content\<close>
|
subsection\<open>Mathematical Content\<close>
|
||||||
|
|
||||||
text\<open>We follow in our enumeration referentiable mathematical content class the AMS style and its
|
text\<open>We follow in our enumeration referentiable mathematical content class the AMS style and its
|
||||||
|
@ -124,8 +123,8 @@ provided \<^emph>\<open>theorem environments\<close> (see \<^verbatim>\<open>tex
|
||||||
\<^verbatim>\<open>axiom\<close>, \<^verbatim>\<open>rule\<close> and \<^verbatim>\<open>assertion\<close> to the list. A particular advantage of \<^verbatim>\<open>texdoc amslatex\<close> is
|
\<^verbatim>\<open>axiom\<close>, \<^verbatim>\<open>rule\<close> and \<^verbatim>\<open>assertion\<close> to the list. A particular advantage of \<^verbatim>\<open>texdoc amslatex\<close> is
|
||||||
that it is well-established and compatible with many LaTeX - styles.\<close>
|
that it is well-established and compatible with many LaTeX - styles.\<close>
|
||||||
|
|
||||||
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop"
|
datatype math_content_class = "defn" | "axm" | "thm" | "lem" | "cor" | "prop"
|
||||||
| "ex" | "rule" | "assn"
|
| "ex" | "rule" | "assn"
|
||||||
|
|
||||||
(*
|
(*
|
||||||
thm Theorem Italic
|
thm Theorem Italic
|
||||||
|
@ -183,26 +182,22 @@ doc_class math_semiformal = math_content +
|
||||||
referentiable :: bool <= True
|
referentiable :: bool <= True
|
||||||
type_synonym math_sfc = math_semiformal
|
type_synonym math_sfc = math_semiformal
|
||||||
|
|
||||||
subsection\<open>old style onto model.\<close>
|
subsection\<open>Instances of the abstract classes Definition / Class / Lemma etc.\<close>
|
||||||
|
|
||||||
text\<open>A rough structuring is modeled as follows:\<close>
|
text\<open>A rough structuring is modeled as follows:\<close>
|
||||||
(* non-evident-statement *)
|
|
||||||
doc_class "definition" = tc +
|
|
||||||
referentiable :: bool <= True
|
|
||||||
tag :: "string" <= "''''"
|
|
||||||
|
|
||||||
doc_class "theorem" = tc +
|
doc_class "definition" = math_content +
|
||||||
|
referentiable :: bool <= True
|
||||||
|
|
||||||
|
doc_class "theorem" = math_content +
|
||||||
referentiable :: bool <= True
|
referentiable :: bool <= True
|
||||||
tag :: "string" <= "''''"
|
|
||||||
|
|
||||||
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
||||||
doc_class "lemma" = tc +
|
doc_class "lemma" = math_content +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= "True"
|
||||||
tag :: "string" <= "''''"
|
|
||||||
|
|
||||||
doc_class "corollary" = tc +
|
doc_class "corollary" = math_content +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= "True"
|
||||||
tag :: "string" <= "''''"
|
|
||||||
|
|
||||||
subsection\<open>Example Statements\<close>
|
subsection\<open>Example Statements\<close>
|
||||||
|
|
||||||
|
|
Reference in New Issue