diff --git a/Isa_DOF.thy b/Isa_DOF.thy index cc8a56ea..91cf8829 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -1,8 +1,13 @@ -chapter \The Document-Type Support Framework for Isabelle\ +chapter \The Document Ontology Framework for Isabelle\ -text\ Offering reflection to ML for class hierarchies, objects and object states. - + Isar syntax for these, assuming that classes entities fit to predefined - Isar keywords. \ +text\ Offering +\<^item> text-elements that can be annotated with meta-information +\<^item> typed links to text-elements via specifically generated anti-quotations +\<^item> typed structure of this meta-information specifiable in an Ontology-Language ODL +\<^item> inner-syntax-antiquotations allowing to reference Isabelle-entities such as + types, terms, theorems inside the meta-information +\<^item> monitors allowing to enforce a specific textual structure of an Isabelle Document +\<^item> LaTeX support. \ text\ In this section, we develop on the basis of a management of references Isar-markups that provide direct support in the PIDE framework. \ @@ -484,7 +489,7 @@ ML\ @{term "@{docitem ''''}"}\ thm "refl" ML\@{thm refl}; Facts.named\ -ML\ @{file "Assert.thy"} ; File.check_file; Path.named_root\ +(* ML\ @{file "Assert.thy"} ; File.check_file; Path.named_root\ *) ML\Parse.path : string parser\ subsection\ Semantics \ @@ -525,14 +530,15 @@ end; (* struct *) (* Test *) -ISA_core.ML_isa_antiq (SOME File.check_file) @{theory} ("RegExp.thy",@{here}); - +(* ISA_core.ML_isa_antiq (SOME File.check_file) @{theory} ("RegExp.thy",@{here}); *) + \ -ML\\ +ML\Syntax.parse_typ\ subsection\ Isar - Setup\ setup\DOF_core.update_isa_global("file",ISA_core.ML_isa_string (SOME File.check_file)) \ +setup\DOF_core.update_isa_global("docitem",ISA_core.ML_isa_string (SOME I)) \ diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy index 63a22767..7ab75082 100644 --- a/examples/scholarly/IsaDofApplications.thy +++ b/examples/scholarly/IsaDofApplications.thy @@ -17,7 +17,7 @@ text*[bu::author, email="''wolff@lri.fr''", affiliation="''Universit\\'e Paris-Sud, Paris, France''"] \Burkhart Wolff\ -text*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\ +Text*[abs::abstract,keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\ While Isabelle is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually provides a framework for developing a wide spectrum of applications. A particular strength @@ -29,7 +29,7 @@ for ensuring the structure of different document types (as, e.g., required in certification processes) in general and, in particular, mechanism for linking informal and formal parts of a document. -In this paper, we present \isadof, a novel Document Ontology Framework +In this paper, we present \isadof, a novel Document Ontology Framework on top of Isabelle. \isadof allows for conventional typesetting \<^emph>\as well\ as formal development. We show how to model document ontologies inside \isadof, how to use the resulting meta-information