inbtroduced shortcut interface.

examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy

@@ -16,6 +16,21 @@ theory "00_Frontmatter"
   imports "Isabelle_DOF.technical_report"
 begin
 
+section\<open>Document Local Setup.\<close>
+text\<open>Some internal setup, introducing document specific abbreviations and macros.\<close>
+
+setup \<open>DOF_lib.define_shortcut ("dof",\<^here>) "\\dof"\<close>
+setup \<open>DOF_lib.define_shortcut ("isadof",\<^here>) "\\isadof"\<close>
+setup \<open>   DOF_lib.define_shortcut ("eg",\<^here>) "\\eg"
+       #> DOF_lib.define_shortcut ("ie",\<^here>) "\\ie"\<close> 
+      (* this is an alternative style for macro definitions eauivalent to setup ... setup  ...*)
+setup \<open>   DOF_lib.define_shortcut ("TeXLive",\<^here>) "\\TeXLife"
+       #> DOF_lib.define_shortcut ("LaTeX",\<^here>) "\\LaTeX{}"\<close>
+
+text\<open>Note that these setups assume that the \<^LaTeX> macros are defined in the 
+     document prelude. \<close>
+
+
 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'']"]
-\<open> \isadof provides an implementation of \dof on top of Isabelle/HOL. 
-  \dof itself is a novel framework for \<^emph>\<open>defining\<close> ontologies
+\<open> \<^isadof> provides an implementation of \<^dof> on top of Isabelle/HOL. 
+  \<^dof> itself is a novel framework for \<^emph>\<open>defining\<close> ontologies
   and \<^emph>\<open>enforcing\<close> 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,

src/DOF/Isa_COL.thy

@@ -226,6 +226,20 @@ val _ =
 end 
 \<close>
 
+section\<open>Shortcuts, Macros, Environments\<close>
+text\<open>This is actually \<^emph>\<open>not\<close> a real DOF feature, rather a slightly more abstract layer over
+     slightly buried standard features of the Isabelle document generator ... \<close>
+
+ML\<open>
+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
+\<close>
+
+
 section\<open>Tables\<close>
 (* TODO ! ! ! *)
 

src/tests/OutOfOrderPresntn.thy

@@ -163,32 +163,26 @@ print_doc_classes
 
 section\<open>Experiments on Inline-Textelements\<close>
 text\<open>Std Abbreviations. Inspired by the block *\<open>control spacing\<close> 
- in @{file \<open>$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\<close>}.
- We could mechanize the table-construction and even attach the LaTeX 
- quirks to be dumped into the prelude.    
- \<close>
+     in @{file \<open>$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\<close>}.
+     We could mechanize the table-construction and even attach the LaTeX 
+     quirks to be dumped into the prelude.  \<close>
+
 ML\<open>
 val _ =
   Theory.setup
-   (   Thy_Output.antiquotation_raw \<^binding>\<open>dof\<close> (Scan.succeed ())
-          (fn _ => fn () => Latex.string "\\dof")
-    #> Thy_Output.antiquotation_raw \<^binding>\<open>isadof\<close> (Scan.succeed ())
-          (fn _ => fn () => Latex.string "\\isadof")
-    #> Thy_Output.antiquotation_raw \<^binding>\<open>eg\<close> (Scan.succeed ())
-          (fn _ => fn () => Latex.string "\\eg") 
-    #> Thy_Output.antiquotation_raw \<^binding>\<open>TeXLive\<close> (Scan.succeed ())
-          (fn _ => fn () => Latex.string "\\TeXLife") 
-    #> Thy_Output.antiquotation_raw \<^binding>\<open>LaTeX\<close> (Scan.succeed ())
-          (fn _ => fn () => Latex.string "\\LaTeX{}") 
-
-)
+   (   Thy_Output.antiquotation_raw \<^binding>\<open>doof\<close> (Scan.succeed ())
+          (fn _ => fn () => Latex.string "\\emph{doof}")
+    #> Thy_Output.antiquotation_raw \<^binding>\<open>LATEX\<close> (Scan.succeed ())
+          (fn _ => fn () => Latex.string "\\textbf{LaTeX}") 
+   )
 \<close>
 
-textN\<open> \<^eg> \<^TeXLive> \<^dof> \<^isadof> \<^LaTeX> \<close>
+textN\<open>  \<^doof> \<^LATEX> \<close>
+
+(* the same effect is achieved with : *)
+setup \<open>DOF_lib.define_shortcut ("bla",\<^here>) "\\bla"\<close>
 
-text\<open> \<^theory_text>\<open>definition\<close>
 
-\<close>
 
 end
 (*>*)