reset

Isabelle_DOF-Example-Extra/ROOTS

@@ -1,4 +1,3 @@
-scholarly_paper
 technical_report
 CENELEC_50128
 cytology

Isabelle_DOF-Example-Extra/scholarly_paper/ROOTS

@@ -1 +0,0 @@
-2020-iFM-CSP

Isabelle_DOF-Example-II/paper.thy

@@ -16,6 +16,8 @@ declare[[ Theorem_default_class    = "theorem"]]
 define_shortcut* csp      \<rightleftharpoons> \<open>CSP\<close>
                  holcsp   \<rightleftharpoons> \<open>HOL-CSP\<close>
                  isabelle \<rightleftharpoons> \<open>Isabelle/HOL\<close>
+                 hfill    \<rightleftharpoons> \<open>\hfill\<close>
+                 br    \<rightleftharpoons> \<open>\break\<close>
 
 (*>*)
 
@@ -27,7 +29,7 @@ author*[lina,email="\<open>lina.ye@lri.fr\<close>",affiliation="\<open>LRI, Inri
                
 abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Algebra\<close>,
                              \<open>Concurrency\<close>,\<open>Computational Models\<close>]"]
-\<open>  The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today 
+\<open>  The theory of Communicating Sequential Processes going back to Hoare and Roscoe is still today  
    one of the reference theories for concurrent specification and computing. In 1997, a first 
    formalization in \<^isabelle> of the denotational semantics of the  Failure/Divergence Model of
    \<^csp> was undertaken; in particular, this model can cope with infinite alphabets, in contrast 
@@ -127,8 +129,6 @@ attempt to formalize denotational \<^csp> semantics covering a part of Bill Rosc
 section*["pre"::tc,main_author="Some(@{docitem \<open>bu\<close>}::author)"]
 \<open>Preliminaries\<close>
 
-text\<open>\<close>
-
 subsection*[cspsemantics::tc, main_author="Some(@{docitem ''bu''})"]\<open>Denotational \<^csp> Semantics\<close>
 
 text\<open> The denotational semantics (following @{cite "roscoe:csp:1998"}) comes in three layers: 
@@ -573,7 +573,7 @@ be deadlocked after any non-terminating trace.
 \<close>
 
 Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>", level="Some 2"]
-\<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>   
+\<open> \<^hfill> \<^br> \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>   
 Definition*[X11, level="Some 2"]\<open>  \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close>   \<close>
 
 text\<open> Recall that all five reference processes are livelock-free. 
@@ -984,10 +984,6 @@ over finite sub-systems with globally infinite systems in a logically safe way.
 subsection*[bib::bibliography]\<open>References\<close>
 
 close_monitor*[this]
-(*
-term\<open>\<longrightarrow>\<close>
-term\<open> demon \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l := \<Sqinter> \<Delta>t \<in> \<real>\<^sub>>\<^sub>0.     ||| i\<in>A. ACTOR i \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l 
-                                   \<lbrakk>S\<rbrakk> sync!\<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>' \<longrightarrow> demon \<sigma>\<^sub>g\<^sub>l\<^sub>o\<^sub>b\<^sub>a\<^sub>l\<^sub>'   \<close>
-*)
+
 end
 (*>*) 

Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy

@@ -43,7 +43,7 @@ text\<open>For now, as the term annotation is not bound to a meta logic which wi
 \<^term>\<open>[@{term ''True''}]\<close> to \<^term>\<open>[True]\<close>, we can not use the HOL \<^const>\<open>True\<close> constant
 in the assertion.\<close>
 
-ML\<open> @{term "[@{term \<open>True \<longrightarrow> True \<close>}]"}; (* with isa-check *)  \<close>
+ML\<open> @{term_ "[@{term \<open>True \<longrightarrow> True \<close>}]"}; (* with isa-check *)  \<close>
 
 ML\<open> 
     (* Checking the default classes which should be in a neutral(unset) state. *)
@@ -81,11 +81,11 @@ text\<open>... which makes it possible to refer in a freeform definition to its
 which will appear textually later. With this pragmatics, an "out-of-order-presentation" 
 can be achieved within \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close> for the most common cases.\<close>
 
-(*<*)  (*LATEX FAILS *)
+
+
 Definition*[e1bis::"definition", short_name="\<open>Nice lemma.\<close>"]
    \<open>Lorem ipsum dolor sit amet, ... 
     This is formally defined as follows in @{definition (unchecked) "e1bisbis"}\<close>
-(*>*)
 definition*[e1bisbis, status=formal] e :: int where "e = 2"
 
 section\<open>Tests for Theorems, Assertions, Assumptions, Hypothesis, etc.\<close>
@@ -105,9 +105,10 @@ Theorem*[e2]\<open>... suspendisse non arcu malesuada mollis, nibh morbi, ... \<
 
 theorem*[e2bis::"theorem", status=formal] f : "e = 1+1" unfolding e_def by simp
 
+(*<*) (* @{theorem "e2bis"} breaks LaTeX generation ... *)
 Lemma*[e3,level="Some 2"]
 \<open>... phasellus amet id massa nunc, pede suscipit repellendus, ... @{theorem "e2bis"} \<close>
-(*<*)(*LATEX FAILS *)
+(*>*) 
 Proof*[d10, short_name="\<open>Induction over Tinea pedis.\<close>"]\<open>Freeform Proof\<close>
 
 lemma*[dfgd::"lemma"] q: "All (\<lambda>x. X \<and> Y \<longrightarrow> True)" oops
@@ -165,6 +166,7 @@ text*[tt13::scholarly_paper.conclusion ]\<open>Lectus accumsan velit ultrices, .
 subsection\<open>Technical Content Specific Elements\<close>
 
 text*[tu1::scholarly_paper.axiom    ]\<open>Lectus accumsan velit ultrices, ...\<close>
+text*[tu1bis::scholarly_paper.math_content, mcc="axm"   ]\<open>Lectus accumsan velit ultrices, ...\<close>
 text*[tu2::scholarly_paper.lemma    ]\<open>Lectus accumsan velit ultrices, ...\<close>
 text*[tu3::scholarly_paper.example  ]\<open>Lectus accumsan velit ultrices, ...\<close>
 text*[tu4::scholarly_paper.premise  ]\<open>Lectus accumsan velit ultrices, ...\<close>
@@ -191,7 +193,5 @@ text*[tt10::scholarly_paper.tech_example]\<open>Lectus accumsan velit ultrices,
 text*[tu8::scholarly_paper.tech_code]        \<open>Lectus accumsan velit ultrices, ...\<close>
 text*[tu27::scholarly_paper.engineering_content]\<open>Lectus accumsan velit ultrices, ...\<close>
 text*[tu14::scholarly_paper.evaluation ]\<open>Lectus accumsan velit ultrices, ...\<close>
-(*>*)
 
 end
-(*>*)

Isabelle_DOF-Unit-Tests/ROOT

@@ -1,5 +1,5 @@
 session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" + 
-  options [document = pdf, document_output = "output", document_build = dof]
+  options [document = pdf, document_output = "output", document_build = dof, document_variants = "document:overview=-proof,-ML,-unimportant"]
   theories
     "TestKit"
     "Latex_Tests"

Isabelle_DOF/latex/styles/DOF-core.sty

@@ -65,7 +65,7 @@
   \ifcsname isaDof.\commandkey{type}\endcsname%
       \csname isaDof.\commandkey{type}\endcsname%
               [label=\commandkey{label},\commandkey{args}]{#1}%
-  \else\relax\fi%
+  \else%
   \ifcsname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
       \csname isaDof.\commandkey{env}.\commandkey{type}\endcsname%
               [label=\commandkey{label},\commandkey{args}]{#1}%
@@ -81,6 +81,7 @@
         definition for "\commandkey{env}" available either.}%
       \fi%
   \fi%
+\fi%
 }
 % end: generic dispatcher
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -170,4 +171,4 @@
 \newcommand{\isactrltermUNDERSCORE}{\isakeywordcontrol{term{\isacharunderscore}}}
 \newcommand{\isactrlvalueUNDERSCORE}{\isakeywordcontrol{value{\isacharunderscore}}}
 \newcommand{\isasymdoublequote}{\texttt{\upshape"}}
-\newcommand{\isasymquote}{\texttt{\upshape'}}
+\newcommand{\isasymquote}{\texttt{\upshape'}}

Isabelle_DOF/ontologies/scholarly_paper/DOF-scholarly_paper-thm.sty

@@ -1,38 +0,0 @@
-%% Copyright (C) 2020 The University of Paris-Saclay
-%%               2020 The University of Exeter
-%%
-%% License:
-%%   This program can be redistributed and/or modified under the terms
-%%   of the LaTeX Project Public License Distributed from CTAN
-%%   archives in directory macros/latex/base/lppl.txt; either
-%%   version 1.3c of the License, or (at your option) any later version.
-%%   OR
-%%   The 2-clause BSD-style license.
-%%
-%%   SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
-
-\NeedsTeXFormat{LaTeX2e}\relax
-\ProvidesPackage{DOF-scholarly_paper-thm}
-  [00/00/0000 Document-Type Support Framework for Isabelle (LNCS).]
-
-\RequirePackage{amsthm}
-
-\newtheorem{example}{Example}
-\newtheorem{assumption}{Assumption}
-\newtheorem{definition}{Definition}
-\newtheorem{theorem}{Theorem} 
-
-%\newtheorem{assertion}{Assumption} %% Hack
-
-%Assertion* 
-%Proposition*
-%Premise*
-%Corollary* 
-%Consequence*
-%Conclusion* 
-%Assumption* 
-%Hypothesis* 
-            
-%Proof*    -- A bit special ? Own local format ?
-
-

Isabelle_DOF/ontologies/scholarly_paper/DOF-scholarly_paper.sty

@@ -31,13 +31,13 @@
 \@ifclassloaded{llncs}%
   {}%
   {%
+    \RequirePackage{amsthm}
     \@ifclassloaded{scrartcl}%
     {%
       \newcommand{\institute}[1]{}%
       \newcommand{\inst}[1]{}%
       \newcommand{\orcidID}[1]{}%
       \newcommand{\email}[1]{}%
-      \RequirePackage{DOF-scholarly_paper-thm}%
     }%
     {%
       \@ifclassloaded{lipics-v2021}%
@@ -165,22 +165,47 @@
   \end{isamarkuptext}%
 }
 
-\newtheorem{axiom}{Axiom}
-\newtheorem{ruleX}{Rule} % apparent name-clash with s th from libraries...
-\newtheorem{assertion}{Assertion} 
-
-% \newcommand{\formalMathStmt[label, mcc, ]
-% end: scholarly_paper.abstract
-% "defn" | "axm" | "theom" | "lemm" | "corr" | "prpo" | "rulE" | "assn" | "hypt" | "assm" | "prms" | "cons" |      
-% "conc_stmt" |"prf_stmt"  | "expl_stmt" |"rmrk" | "notn" | "tmgy" |      
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
+%\RequirePackage{amsthm}
+%\newtheorem{example}{Example}
+%\newtheorem{assumption}{Assumption}
+%\newtheorem{definition}{Definition}
+%\newtheorem{theorem}{Theorem} 
+\newtheorem{defn}{Definition} 
+\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{axm}{Axiom}
+\newtheorem{theom}{Theorem}
+\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{lemm}{Lemma}
+\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{corr}{Corollary}
+\NewEnviron{isamarkupCorollary*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{prpo}{Proposition}
+\NewEnviron{isamarkupProposition*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{rulE}{Rule}
+\newtheorem{assn}{Assertion}    
+\NewEnviron{isamarkupAssertion*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{hypt}{Hypothesis}
+\NewEnviron{isamarkupHypothesis*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{assm}{Assumption}
+\NewEnviron{isamarkupAssumption*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{prms}{Premise}
+\NewEnviron{isamarkupPremise*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{cons}{Consequence}
+\NewEnviron{isamarkupConsequence*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{conc_stmt}{Conclusion}
+\NewEnviron{isamarkupConclusion*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{prf_stmt}{Proof}
+\NewEnviron{isamarkupProof*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{expl_stmt}{Example}
+\NewEnviron{isamarkupExample*}[1][]{\isaDof[env={text},#1]{\BODY}}
+\newtheorem{rmrk}{Remark}
+\newtheorem{notn}{Notation}
+\newtheorem{tmgy}{Terminology}
 
 \newisadof{text.scholarly_paper.math_content}%
 [label=,type=%
- , scholarly_paper.math_content.short_name ={} % {} or \relax
- , scholarly_paper.math_content.mcc     = % "defn" | "axm" | "thm" | "lem" | "prop" | "rule" | "assn" | "assm"
+ , scholarly_paper.math_content.short_name ={}%
+ , scholarly_paper.math_content.mcc     = % 
  , Isa_COL.text_element.level         =%
  , Isa_COL.text_element.referentiable =%
  , Isa_COL.text_element.variants      =%
@@ -193,317 +218,20 @@
  [1]
  {%
     \begin{isamarkuptext}%
-        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
-                         {\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                             \label{\commandkey{label}} #1 
-                          \end{definition}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{axm}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{axiom} \label{\commandkey{label}} #1 \end{axiom} }
-                         {\begin{axiom} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                        \label{\commandkey{label}} #1 
-                          \end{axiom}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{theom}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
-                         {\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                          \label{\commandkey{label}} #1 
-                          \end{theorem}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lemm}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
-                         {\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                        \label{\commandkey{label}} #1 
-                          \end{lemma}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl_stmt}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{example} \label{\commandkey{label}} #1 \end{example} }
-                         {\begin{example} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                          \label{\commandkey{label}} #1 
-                          \end{example}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{corr}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{corrollary} \label{\commandkey{label}} #1 \end{corrollary} }
-                         {\begin{corrollary} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                             \label{\commandkey{label}} #1 
-                          \end{corrollary}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{prpo}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{property} \label{\commandkey{label}} #1 \end{property} }
-                         {\begin{property} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                           \label{\commandkey{label}} #1 
-                          \end{property}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rulE}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{ruleX} \label{\commandkey{label}} #1 \end{ruleX} }
-                         {\begin{ruleX} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                        \label{\commandkey{label}} #1 
-                          \end{ruleX}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{rmrk}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{remark}  \label{\commandkey{label}} #1 \end{remark} }
-                         {\begin{remark} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                          \label{\commandkey{label}} #1 
-                          \end{remark}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assn}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{assertion} \label{\commandkey{label}} #1 \end{assertion} }
-                         {\begin{assertion} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                             \label{\commandkey{label}} #1 
-                          \end{assertion}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{assm}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{assumption} \label{\commandkey{label}} #1 \end{assumption} }
-                         {\begin{assumption} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                             \label{\commandkey{label}} #1 
-                          \end{assumption}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{notn}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{notation} \label{\commandkey{label}} #1 \end{notation} }
-                         {\begin{notation} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                           \label{\commandkey{label}} #1 
-                          \end{notation}}
-                    }%
-                   }%
-        {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{tmgy}}    
-                   {%
-                    {\ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{terminology} \label{\commandkey{label}} #1 \end{terminology} }
-                         {\begin{terminology} [\commandkey{scholarly_paper.math_content.short_name}] 
-                                              \label{\commandkey{label}} #1 
-                          \end{terminology}}
-                    }%
-                   }%
-        {%     
-           \typeout{Internal error: enumeration out of sync with ontology scholarly-paper.} 
-        }%
-        }%
-        }%
-        }%
-        }%
-        }%
-        }%
-        }%
-        }%
-        }%
-        }%
-        }%
-        }%      
+      \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
+        {%
+         \begin{\commandkey{scholarly_paper.math_content.mcc}}\label{\commandkey{label}}
+           #1
+         \end{\commandkey{scholarly_paper.math_content.mcc}}
+        }{%
+         \begin{\commandkey{scholarly_paper.math_content.mcc}}[\commandkey{scholarly_paper.math_content.short_name}]\label{\commandkey{label}} 
+           #1 
+         \end{\commandkey{scholarly_paper.math_content.mcc}}
+        }
     \end{isamarkuptext}%
  } 
 
-
-
-% end: scholarly_paper.math_content
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Besser: Einfach durchreichen wg Vererbung !
-\newisadof{text.scholarly_paper.math_example}%
-[label=,type=%
- , scholarly_paper.math_content.short_name =%
- , scholarly_paper.math_content.mcc =%
- , Isa_COL.text_element.level         =%
- , Isa_COL.text_element.referentiable =%
- , Isa_COL.text_element.variants      =%
- , scholarly_paper.text_section.main_author  =%
- , scholarly_paper.text_section.fixme_list   =%
- , scholarly_paper.technical.definition_list =%
- , scholarly_paper.technical.status          =%
- ]
- [1]
- {%
-    \begin{isamarkuptext}%
-        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{expl}}{
-              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{example} \label{\commandkey{label}} #1 \end{example} }
-                         {\begin{example} [\commandkey{scholarly_paper.math_content.short_name}]
-                                          \label{\commandkey{label}} #1  
-                          \end{example}}
-          }{%     
-          #1%
-        }%
-    \end{isamarkuptext}%
- }
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\NewEnviron{isamarkupDefinition*}[1][]{\isaDof[env={text},#1]{\BODY}}
-\newisadof{text.scholarly_paper.definition}%
-[label=,type=%
- , scholarly_paper.math_content.short_name =%
- , scholarly_paper.math_content.mcc =%
- , Isa_COL.text_element.level         =%
- , Isa_COL.text_element.referentiable =%
- , Isa_COL.text_element.variants      =%
- , scholarly_paper.text_section.main_author  =%
- , scholarly_paper.text_section.fixme_list   =%
- , Isa_COL.text_element.level                =%
- , scholarly_paper.technical.definition_list =%
- , scholarly_paper.technical.status          =%
- ]
- [1]
- {%
-    \begin{isamarkuptext}%
-        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{defn}}{
-              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
-                         {\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{definition}}
-          }{%     
-          #1%
-        }%
-    \end{isamarkuptext}%
- }
-
-% An experiment in inheritance of the default behaviour.
-% \newisadof{text.scholarly_paper.definition}%
-% [label=,type=%
-%  , scholarly_paper.math_content.short_name =%
-%  , scholarly_paper.math_content.mcc =%
-%  , Isa_COL.text_element.level         =%
-%  , Isa_COL.text_element.referentiable =%
-%  , Isa_COL.text_element.variants      =%
-%  , scholarly_paper.text_section.main_author  =%
-%  , scholarly_paper.text_section.fixme_list   =%
-%  , scholarly_paper.technical.definition_list =%
-%  , scholarly_paper.technical.status          =%
-%  ]
-%  [1]
-%  {%
-%     \cscommand{text.scholarly_paper.math_content}%
-%     [label=\commandkey{label},type=\commandkey{type}%
-%     , scholarly_paper.math_content.short_name   =\commandkey{scholarly_paper.math_content.short_name}%
-%     , scholarly_paper.math_content.mcc          =\commandkey{scholarly_paper.math_content.mcc}%
-%     , Isa_COL.text_element.level                =\commandkey{Isa_COL.text_element.level}%
-%     , Isa_COL.text_element.referentiable        =\commandkey{Isa_COL.text_element.referentiable}%
-%     , Isa_COL.text_element.variants             =\commandkey{Isa_COL.text_element.variants}%
-%     , scholarly_paper.text_section.main_author  =\commandkey{scholarly_paper.text_section.main_author}%
-%     , scholarly_paper.text_section.fixme_list   =\commandkey{scholarly_paper.text_section.fixme_list}%
-%     , scholarly_paper.technical.definition_list =\commandkey{scholarly_paper.technical.definition_list}%
-%     , scholarly_paper.technical.status          =\commandkey{scholarly_paper.technical.status}%
-%     ]
-%     {#1}%
-%  }
- 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% Besser: Einfach durchreichen wg Vererbung !
-\NewEnviron{isamarkupLemma*}[1][]{\isaDof[env={text.scholarly_paper.lemma},#1]{\BODY}}
-\newisadof{text.scholarly_paper.lemma}%
-[label=,type=%
- , scholarly_paper.math_content.short_name =%
- , scholarly_paper.math_content.mcc =%
- , Isa_COL.text_element.level         =%
- , Isa_COL.text_element.referentiable =%
- , Isa_COL.text_element.variants      =%
- , scholarly_paper.text_section.main_author  =%
- , scholarly_paper.text_section.fixme_list   =%
- , Isa_COL.text_element.level                =%
- , scholarly_paper.technical.definition_list =%
- , scholarly_paper.technical.status          =%
- ]
- [1]
- {%
-    \begin{isamarkuptext}%
-        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{lem}}{
-              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{lemma} \label{\commandkey{label}} #1 \end{lemma} }
-                         {\begin{lemma} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{lemma}}
-          }{%     
-          #1%
-        }%
-    \end{isamarkuptext}%
- } 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Besser: Einfach durchreichen wg Vererbung !
-\NewEnviron{isamarkupTheorem*}[1][]{\isaDof[env={text.scholarly_paper.theorem},#1]{\BODY}}
-\newisadof{text.scholarly_paper.theorem}%
-[label=,type=%
- , scholarly_paper.math_content.short_name =%
- , scholarly_paper.math_content.mcc =%
- , Isa_COL.text_element.level         =%
- , Isa_COL.text_element.referentiable =%
- , Isa_COL.text_element.variants      =%
- , scholarly_paper.text_section.main_author  =%
- , scholarly_paper.text_section.fixme_list   =%
- , Isa_COL.text_element.level                =%
- , scholarly_paper.technical.definition_list =%
- , scholarly_paper.technical.status          =%
- ]
- [1]
- {%
-    \begin{isamarkuptext}%
-        \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{thm}}{
-              \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }  
-                         {\begin{theorem} \label{\commandkey{label}} #1 \end{theorem} }
-                         {\begin{theorem} [\commandkey{scholarly_paper.math_content.short_name}] \label{\commandkey{label}} #1 \end{theorem}}
-          }{%     
-          #1%
-        }%
-    \end{isamarkuptext}%
- } 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Generic Example. Different inheritance hierachy.
-\newisadof{text.scholarly_paper.example}%
-[label=,type=%
- , Isa_COL.text_element.level         =%
- , Isa_COL.text_element.referentiable =%
- , Isa_COL.text_element.variants      =%
- , scholarly_paper.text_section.main_author  =%
- , scholarly_paper.text_section.fixme_list   =%
- , scholarly_paper.technical.definition_list =%
- , scholarly_paper.example.status     =%
- , scholarly_paper.example.short_name =%
- ]
- [1]
- {%
-    \begin{isamarkuptext}%
-        \ifthenelse{\equal{\commandkey{scholarly_paper.example.status}}{semiformal}}{
-              \ifthenelse{\equal{\commandkey{scholarly_paper.example.short_name}} {} }  
-                         {\begin{example} \label{\commandkey{label}} #1 \end{example} }
-                         {\begin{example} [\commandkey{scholarly_paper.example.short_name}] %
-                                          \label{\commandkey{label}} #1 %
-                          \end{example}} %
-                         }%
-        {%     
-          #1%
-        }%
-    \end{isamarkuptext}%
- }
-
 
 %% Miscellaneous
 \usepackage{xspace}
@@ -511,3 +239,4 @@
 \newcommand{\eg}{e.\,g.\xspace}
 \newcommand{\etc}{etc}
 
+

Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy

@@ -53,12 +53,12 @@ ML\<open>
 val _ =
   Monitor_Command_Parser.document_command \<^command_keyword>\<open>abstract*\<close> "Textual Definition"
     {markdown = true, body = true}
-    (Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []);
+    (Onto_Macros.enriched_document_cmd_exp (SOME "abstract") []) (K(K I));
 
 val _ =
   Monitor_Command_Parser.document_command \<^command_keyword>\<open>author*\<close> "Textual Definition"
     {markdown = true, body = true}
-    (Onto_Macros.enriched_document_cmd_exp (SOME "author") []);
+    (Onto_Macros.enriched_document_cmd_exp (SOME "author") []) (K(K I));
 \<close>
 
 text\<open>Scholarly Paper is oriented towards the classical domains in science:
@@ -444,48 +444,49 @@ fun doc_cmd kwd txt flag key =
       in
         Onto_Macros.enriched_formal_statement_command  default [("mcc",key)] meta_args thy
       end)
+      (Onto_Macros.transform_attr [("mcc",key)])
 
 in
 
 val _ = doc_cmd \<^command_keyword>\<open>Definition*\<close> "Freeform Definition" 
-                 Definition_default_class \<^const_name>\<open>defn\<close>;
+                Definition_default_class "defn";
 
 val _ = doc_cmd \<^command_keyword>\<open>Lemma*\<close>      "Freeform Lemma Description" 
-                 Lemma_default_class \<^const_name>\<open>lemm\<close>;
+                 Lemma_default_class "lemm";
 
 val _ = doc_cmd \<^command_keyword>\<open>Theorem*\<close>    "Freeform Theorem" 
-                 Theorem_default_class \<^const_name>\<open>theom\<close>;
+                 Theorem_default_class "theom";
 
 (* cut and paste to make it runnable, but nonsensical so far: *)
 val _ = doc_cmd \<^command_keyword>\<open>Proposition*\<close> "Freeform Proposition"
-                  Proposition_default_class \<^const_name>\<open>prpo\<close>;
+                  Proposition_default_class "prpo";
 
 val _ = doc_cmd \<^command_keyword>\<open>Premise*\<close> "Freeform Premise"
-                  Premise_default_class \<^const_name>\<open>prms\<close>;
+                  Premise_default_class "prms";
 
 val _ = doc_cmd \<^command_keyword>\<open>Corollary*\<close> "Freeform Corollary"
-                  Corollary_default_class \<^const_name>\<open>corr\<close>;
+                  Corollary_default_class "corr";
 
 val _ = doc_cmd \<^command_keyword>\<open>Consequence*\<close> "Freeform Consequence"
-                  Consequence_default_class \<^const_name>\<open>cons\<close>;
+                  Consequence_default_class "cons";
                       
 val _ = doc_cmd \<^command_keyword>\<open>Conclusion*\<close> "Freeform Conclusion"
-                  Conclusion_default_class \<^const_name>\<open>conc_stmt\<close>;
+                  Conclusion_default_class "conc_stmt";
                            
 val _ = doc_cmd \<^command_keyword>\<open>Assumption*\<close> "Freeform Assumption"
-                  Assumption_default_class \<^const_name>\<open>assm\<close>;
+                  Assumption_default_class "assm";
 
 val _ = doc_cmd \<^command_keyword>\<open>Hypothesis*\<close> "Freeform Hypothesis"
-                  Hypothesis_default_class \<^const_name>\<open>prpo\<close>;
+                  Hypothesis_default_class "prpo";
 
 val _ = doc_cmd \<^command_keyword>\<open>Assertion*\<close> "Freeform Assertion"
-                  Assertion_default_class \<^const_name>\<open>assn\<close>;
+                  Assertion_default_class "assn";
 
 val _ = doc_cmd \<^command_keyword>\<open>Proof*\<close> "Freeform Proof"
-                  Proof_default_class \<^const_name>\<open>prf_stmt\<close>;
+                  Proof_default_class "prf_stmt";
 
 val _ = doc_cmd \<^command_keyword>\<open>Example*\<close> "Freeform Example"
-                  Example_default_class \<^const_name>\<open>expl_stmt\<close>;
+                  Example_default_class "expl_stmt";
 end
 end 
 \<close>

Isabelle_DOF/scala/dof_document_build.scala

@@ -97,6 +97,17 @@ object DOF_Document_Build
 \newcommand{\isadofgenericdoi}{""" + DOF.generic_doi + """}
 \newcommand{\isabellelatestversion}{""" + DOF.latest_isabelle + """}
 """)
+
+
+      val texinputs: Path = Path.explode("~~/lib/texinputs")
+      val comment_latex = options.bool("document_comment_latex")
+      if (!comment_latex) { 
+        Isabelle_System.copy_file(texinputs + Path.basic("comment.sty"), directory.doc_dir)
+      }
+
+      doc.tags.sty(comment_latex).write(directory.doc_dir)
+
+
       directory
     }
   }

Isabelle_DOF/thys/Isa_COL.thy

@@ -103,13 +103,44 @@ fun transform_cid thy NONE X = X
                              end  
 in
 
-fun enriched_formal_statement_command ncid (S: (string * string) list) =
-   let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ 
-                                      (("formal_results",@{here}),"([]::thm list)")::doc_attrs
-   in  fn margs => fn thy =>
+fun transform_attr S cid_long thy doc_attrs =
+  let
+    fun transform_attr' [] doc_attrs = doc_attrs
+      | transform_attr' (s::S) (doc_attrs) =
+          let fun markup2string s = s |> YXML.content_of
+                                      |> Symbol.explode 
+                                      |> List.filter (fn c => c <> Symbol.DEL)
+                                      |> String.concat
+              fun toLong n = DOF_core.get_attribute_info cid_long (markup2string n) thy
+                             |> the |> #long_name
+              val (name', value) = s |> (fn (n, v) => (toLong n, v))
+              val doc_attrs' = doc_attrs
+                               |> map (fn (name, term) => if name = name'
+                                                          then (name, value)
+                                                          else (name, term))
+          in if doc_attrs' = doc_attrs
+             then transform_attr' S doc_attrs' |> cons (name', value) 
+             else transform_attr' S doc_attrs' 
+          end
+  in transform_attr' S doc_attrs end
+
+(*fun update_meta_args_attrs S
+      ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) =
+  (((oid, pos),cid_pos), transform_attr S doc_attrs)
+*)
+(*fun enriched_formal_statement_command ncid (S: (string * string) list) =
+   fn margs => fn thy =>
           Monitor_Command_Parser.gen_enriched_document_cmd {inline=true} 
-                                    (transform_cid thy ncid) transform_attr margs thy 
-   end;
+                                    (transform_cid thy ncid) (transform_attr S) margs thy
+*)
+
+fun enriched_formal_statement_command ncid (S: (string * string) list) =
+  let fun transform_attr doc_attrs = (map (fn(cat,tag) => ((cat,@{here}),tag)) S) @ 
+                                      (("formal_results",@{here}),"([]::thm list)")::doc_attrs
+  in  fn margs => fn thy =>
+          Monitor_Command_Parser.gen_enriched_document_cmd {inline=true} 
+                                    (transform_cid thy ncid) transform_attr margs thy
+  end;
 
 fun enriched_document_cmd_exp ncid (S: (string * string) list) =
    (* expands ncid into supertype-check. *)
@@ -123,7 +154,7 @@ end (* local *)
 
 fun heading_command (name, pos) descr level =
   Monitor_Command_Parser.document_command (name, pos) descr
-    {markdown = false, body = true} (enriched_text_element_cmd level);
+    {markdown = false, body = true} (enriched_text_element_cmd level) (K(K I));
 
 val _ = heading_command \<^command_keyword>\<open>title*\<close> "section heading" NONE;
 val _ = heading_command \<^command_keyword>\<open>subtitle*\<close> "section heading" NONE;

Isabelle_DOF/thys/Isa_DOF.thy

@@ -2137,16 +2137,15 @@ fun close_monitor_command (args as (((oid, pos), cid_pos),
     end 
 
 
-fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) =
+fun meta_args_2_latex thy transform_attr
+      ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) =
     (* for the moment naive, i.e. without textual normalization of 
        attribute names and adapted term printing *)
-    let val l   = "label = "^ (enclose "{" "}" lab)
+    let val l   = DOF_core.get_instance_name_global lab thy |> enclose "{" "}"
+                                                            |> prefix "label = "
       (*  val _   = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *)
         val cid_long = case cid_opt of
-                                NONE => let val DOF_core.Instance cid =
-                                               DOF_core.get_instance_global lab thy
-                                        in cid |> #cid end
-                                  
+                                NONE => DOF_core.cid_of lab thy
                               | SOME(cid,_) => DOF_core.get_onto_class_name_global' cid thy        
         (* val _   = writeln("meta_args_2_string cid_long:"^ cid_long ) *)
         val cid_txt  = "type = " ^ (enclose "{" "}" cid_long);
@@ -2194,8 +2193,11 @@ fun meta_args_2_latex thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Pa
 
         val default_args_filtered = filter (fn (a,_) => not (exists (fn b => b = a) 
                                     (map (fn (c,_) => c) actual_args))) default_args
-        val str_args = map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs)) 
-                      (actual_args@default_args_filtered)
+        val transformed_args = (actual_args@default_args_filtered)
+                               |> transform_attr cid_long thy
+        val str_args = transformed_args
+                       |> map (fn (lhs,rhs) => lhs^" = "^(enclose "{" "}" rhs)) 
+                      
         val label_and_type = String.concat [ l, ",", cid_txt]
         val str_args = label_and_type::str_args
     in
@@ -2219,15 +2221,15 @@ fun gen_enriched_document_cmd' {inline} cid_transform attr_transform
 (* {markdown = true} sets the parsing process such that in the text-core
    markdown elements are accepted. *)
 
-fun document_output {markdown: bool, markup: Latex.text -> Latex.text} meta_args text ctxt =
+fun document_output {markdown: bool, markup: Latex.text -> Latex.text} transform_attr meta_args text ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     val _ = Context_Position.reports ctxt (Document_Output.document_reports text);
-    val output_meta = meta_args_2_latex thy meta_args;
+    val output_meta = meta_args_2_latex thy transform_attr meta_args;
     val output_text = Document_Output.output_document ctxt {markdown = markdown} text;
   in markup (output_meta @ output_text) end;
 
-fun document_output_reports name {markdown, body} meta_args text ctxt =
+fun document_output_reports name {markdown, body} transform_attr meta_args text ctxt =
   let
     (*val pos = Input.pos_of text;
     val _ =
@@ -2237,16 +2239,16 @@ fun document_output_reports name {markdown, body} meta_args text ctxt =
     fun markup xml =
       let val m = if body then Markup.latex_body else Markup.latex_heading
       in [XML.Elem (m (Latex.output_name name), xml)] end;
-  in document_output {markdown = markdown, markup = markup} meta_args text ctxt end;
+  in document_output {markdown = markdown, markup = markup} transform_attr meta_args text ctxt end;
 
 
 (* document output commands *)
 
-fun document_command (name, pos) descr mark cmd =
+fun document_command (name, pos) descr mark cmd transform_attr =
   Outer_Syntax.command (name, pos) descr
     (ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) =>
       Toplevel.theory' (fn _ => cmd meta_args)
-      (Toplevel.presentation_context #> document_output_reports name mark meta_args text #> SOME)));
+      (Toplevel.presentation_context #> document_output_reports name mark transform_attr meta_args text #> SOME)));
 
 
 (* Core Command Definitions *)
@@ -2272,14 +2274,14 @@ val _ =
 
 val _ =
   document_command \<^command_keyword>\<open>text*\<close> "formal comment (primary style)"
-    {markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I);
+    {markdown = true, body = true} (gen_enriched_document_cmd {inline=true} I I) (K(K I));
 
 
 (* This is just a stub at present *)
 val _ =
   document_command \<^command_keyword>\<open>text-macro*\<close> "formal comment macro"
     {markdown = true, body = true}
-    (gen_enriched_document_cmd {inline=false} (* declare as macro *) I I);
+    (gen_enriched_document_cmd {inline=false} (* declare as macro *) I I) (K(K I));
 
  
 val (declare_reference_default_class, declare_reference_default_class_setup) 
@@ -2690,7 +2692,8 @@ struct
 fun meta_args_2_string thy ((((lab, pos), cid_opt), attr_list) : ODL_Meta_Args_Parser.meta_args_t) = 
     (* for the moment naive, i.e. without textual normalization of 
        attribute names and adapted term printing *)
-    let val l   = "label = "^ (enclose "{" "}" lab)
+    let val l   = DOF_core.get_instance_name_global lab thy |> enclose "{" "}"
+                                                            |> prefix "label = "
       (*  val _   = writeln("meta_args_2_string lab:"^ lab ^":"^ (@{make_string } cid_opt) ) *)
         val cid_long = case cid_opt of
                                 NONE => let val DOF_core.Instance cid =
@@ -2814,6 +2817,8 @@ val docitem_antiquotation_parser = (Scan.lift (docitem_modes -- Parse.embedded_i
 
 fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src ) = 
     let val (str,pos) = Input.source_content src
+                        |> apfst (fn str => (Proof_Context.theory_of ctxt)
+                                            |> DOF_core.get_instance_name_global str)
         val inline = Config.get ctxt Document_Antiquotation.thy_output_display
         val _ = check_and_mark ctxt cid_decl {strict_checking = not unchecked} 
                                              {inline = inline} pos str
@@ -2824,7 +2829,7 @@ fun pretty_docitem_antiquotation_generic cid_decl ctxt ({unchecked, define}, src
            |(true,true)  => XML.enclose("\\csname isaDof.macroDef\\endcsname[type={"^cid_decl^"}]{")"}" 
            |(false,true) => XML.enclose("\\csname isaDof.macroExp\\endcsname[type={"^cid_decl^"}]{")"}"
         )
-        (Latex.text (Input.source_content src))
+        (Latex.text (str, pos))
     end      
 
 

Isabelle_DOF/thys/manual/M_03_GuidedTour.thy

@@ -533,7 +533,6 @@ We still mention a few of these document antiquotations here:
   verifies its existance in the (Isabelle-virtual) file-system.
 \<close>
 
-lemma \<open>x = x\<close> by auto
 text\<open>There are options to display sub-parts of formulas etc., but it is a consequence
 of tight-checking that the information must be given complete and exactly in the syntax of
 Isabelle. This may be over-precise and a burden to readers not familiar with Isabelle, which may

ROOTS

@@ -2,5 +2,6 @@ Isabelle_DOF
 Isabelle_DOF-Proofs
 Isabelle_DOF-Ontologies
 Isabelle_DOF-Unit-Tests
+Isabelle_DOF-Example-I
+Isabelle_DOF-Example-II
 Isabelle_DOF-Example-Extra
-Isabelle_DOF-Example-Scholarly_Paper