diff --git a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy index f998bb06..2b18be2d 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy @@ -16,6 +16,21 @@ theory "00_Frontmatter" imports "Isabelle_DOF.technical_report" begin +section\Document Local Setup.\ +text\Some internal setup, introducing document specific abbreviations and macros.\ + +setup \DOF_lib.define_shortcut ("dof",\<^here>) "\\dof"\ +setup \DOF_lib.define_shortcut ("isadof",\<^here>) "\\isadof"\ +setup \ DOF_lib.define_shortcut ("eg",\<^here>) "\\eg" + #> DOF_lib.define_shortcut ("ie",\<^here>) "\\ie"\ + (* this is an alternative style for macro definitions eauivalent to setup ... setup ...*) +setup \ DOF_lib.define_shortcut ("TeXLive",\<^here>) "\\TeXLife" + #> DOF_lib.define_shortcut ("LaTeX",\<^here>) "\\LaTeX{}"\ + +text\Note that these setups assume that the \<^LaTeX> macros are defined in the + document prelude. \ + + open_monitor*[this::report] (*>*) @@ -34,17 +49,17 @@ text*[bu::author, text*[abs::abstract, keywordlist="[''Ontology'', ''Ontological Modeling'', ''Document Management'', ''Formal Document Development'', ''Document Authoring'', ''Isabelle/DOF'']"] -\ \isadof provides an implementation of \dof on top of Isabelle/HOL. - \dof itself is a novel framework for \<^emph>\defining\ ontologies +\ \<^isadof> provides an implementation of \<^dof> on top of Isabelle/HOL. + \<^dof> itself is a novel framework for \<^emph>\defining\ ontologies and \<^emph>\enforcing\ them during document development and document - evolution. \isadof targets use-cases such as mathematical texts referring + evolution. \<^isadof> targets use-cases such as mathematical texts referring to a theory development or technical reports requiring a particular structure. - A major application of \dof is the integrated development of - formal certification documents (\eg, for Common Criteria or CENELEC + A major application of \<^dof> is the integrated development of + formal certification documents (\<^eg>, for Common Criteria or CENELEC 50128) that require consistency across both formal and informal arguments. - \isadof is integrated into Isabelle's IDE, which + \<^isadof> is integrated into Isabelle's IDE, which allows for smooth ontology development as well as immediate ontological feedback during the editing of a document. Its checking facilities leverage the collaborative @@ -52,11 +67,11 @@ text*[abs::abstract, underlying ontological structure. In this user-manual, we give an in-depth presentation of the design - concepts of \dof's Ontology Definition Language (ODL) and describe + concepts of \<^dof>'s Ontology Definition Language (ODL) and describe comprehensively its major commands. Many examples show typical best-practice applications of the system. - It is an unique feature of \isadof that ontologies may be used to control + It is an unique feature of \<^isadof> that ontologies may be used to control the link between formal and informal content in documents in a machine checked way. These links can connect both text elements as well as formal modelling elements such as terms, definitions, code and logical formulas, diff --git a/src/DOF/Isa_COL.thy b/src/DOF/Isa_COL.thy index 22681f0a..baa303b3 100755 --- a/src/DOF/Isa_COL.thy +++ b/src/DOF/Isa_COL.thy @@ -226,6 +226,20 @@ val _ = end \ +section\Shortcuts, Macros, Environments\ +text\This is actually \<^emph>\not\ a real DOF feature, rather a slightly more abstract layer over + slightly buried standard features of the Isabelle document generator ... \ + +ML\ +structure DOF_lib = +struct +fun define_shortcut (name, pos) latexshcut = + Thy_Output.antiquotation_raw (Binding.make(name,pos)) (Scan.succeed ()) + (fn _ => fn () => Latex.string latexshcut) +end +\ + + section\Tables\ (* TODO ! ! ! *) diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy index f79a8f81..b104ea71 100644 --- a/src/tests/OutOfOrderPresntn.thy +++ b/src/tests/OutOfOrderPresntn.thy @@ -163,32 +163,26 @@ print_doc_classes section\Experiments on Inline-Textelements\ text\Std Abbreviations. Inspired by the block *\control spacing\ - in @{file \$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\}. - We could mechanize the table-construction and even attach the LaTeX - quirks to be dumped into the prelude. - \ + in @{file \$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\}. + We could mechanize the table-construction and even attach the LaTeX + quirks to be dumped into the prelude. \ + ML\ val _ = Theory.setup - ( Thy_Output.antiquotation_raw \<^binding>\dof\ (Scan.succeed ()) - (fn _ => fn () => Latex.string "\\dof") - #> Thy_Output.antiquotation_raw \<^binding>\isadof\ (Scan.succeed ()) - (fn _ => fn () => Latex.string "\\isadof") - #> Thy_Output.antiquotation_raw \<^binding>\eg\ (Scan.succeed ()) - (fn _ => fn () => Latex.string "\\eg") - #> Thy_Output.antiquotation_raw \<^binding>\TeXLive\ (Scan.succeed ()) - (fn _ => fn () => Latex.string "\\TeXLife") - #> Thy_Output.antiquotation_raw \<^binding>\LaTeX\ (Scan.succeed ()) - (fn _ => fn () => Latex.string "\\LaTeX{}") - -) + ( Thy_Output.antiquotation_raw \<^binding>\doof\ (Scan.succeed ()) + (fn _ => fn () => Latex.string "\\emph{doof}") + #> Thy_Output.antiquotation_raw \<^binding>\LATEX\ (Scan.succeed ()) + (fn _ => fn () => Latex.string "\\textbf{LaTeX}") + ) \ -textN\ \<^eg> \<^TeXLive> \<^dof> \<^isadof> \<^LaTeX> \ +textN\ \<^doof> \<^LATEX> \ + +(* the same effect is achieved with : *) +setup \DOF_lib.define_shortcut ("bla",\<^here>) "\\bla"\ -text\ \<^theory_text>\definition\ -\ end (*>*)