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