Merge branch 'ICFEM-2022' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF into ICFEM-2022

etc/options

@@ -2,7 +2,25 @@
 
 section "Isabelle/DOF"
 
-public option dof_url : string = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
+public option dof_document_class : string = "scrreprt-modern"
+  -- "Default document class for Isabelle/DOF documents"
+
+public option dof_presentation_ontologies : string = "technical_report scholarly_paper"
+  -- "ontologies (separated by blanks)"
+
+
+option dof_version : string = "Unreleased" 
+  -- "Isabelle/DOF version" 
+     (* "Unreleased" for development, semantic version for releases *)
+
+option dof_isabelle : string = "2021-1" 
+
+option dof_latest_version : string = "1.2.0"    
+option dof_latest_isabelle : string = "Isabelle2021"
+option dof_latest_doi : string = "10.5281/zenodo.6385695"
+option dof_generic_doi : string = "10.5281/zenodo.3370482"
+
+option dof_url : string = "https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF"
   -- "Isabelle/DOF source repository"
 
 option dof_artifact_dir : string = "releases/Isabelle_DOF/Isabelle_DOF"

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/ROOT

@@ -6,8 +6,10 @@ session "2018-cicm-isabelle_dof-applications" = "Isabelle_DOF" +
   document_files
     "isadof.cfg"
     "root.bib"
+    "authorarchive.sty"
     "preamble.tex"
     "lstisadof.sty"
+    "vector_iD_icon.pdf"
     "figures/isabelle-architecture.pdf"
     "figures/Dogfood-Intro.png"
     "figures/InteractiveMathSheet.png"

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/authorarchive.sty

@@ -0,0 +1,339 @@
+%% Copyright (C) 2008-2019 Achim D. Brucker, https://www.brucker.ch
+%%
+%% 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{authorarchive}
+  [0000/00/00 Unreleased v1.1.1+%
+  Self-archiving information for scientific publications.]
+%
+\PassOptionsToPackage{hyphens}{url}
+%
+\RequirePackage{ifthen}
+\RequirePackage[inline]{enumitem}
+\RequirePackage{graphicx}
+\RequirePackage{eso-pic}
+\RequirePackage{intopdf}
+\RequirePackage{kvoptions}
+\RequirePackage{hyperref}
+\RequirePackage{calc}
+\RequirePackage{qrcode}
+\RequirePackage{hvlogos}
+%
+%Better url breaking
+\g@addto@macro{\UrlBreaks}{\UrlOrds}
+%
+% Option declarations
+% -------------------
+\SetupKeyvalOptions{
+  family=AA,
+  prefix=AA@
+}
+%
+\DeclareStringOption[.]{bibtexdir}
+\DeclareStringOption[https://duckduckgo.com/?q=]{baseurl}
+\DeclareStringOption[.pdf]{suffix}
+\DeclareStringOption[UNKNOWN PUBLISHER]{publisher}[]
+\DeclareStringOption[UNKNOWN YEAR]{year}[]
+\DeclareStringOption[]{key}[]
+\DeclareStringOption[]{doi}[]
+\DeclareStringOption[]{doiText}[]
+\DeclareStringOption[]{publisherurl}[]
+\DeclareStringOption[UNKNOWN START PAGE]{startpage}[]
+\DeclareStringOption[UNKNOWN PUBLICATION]{publication}[]
+
+\DeclareBoolOption{ACM}
+\DeclareBoolOption{acmart}
+\DeclareBoolOption{ENTCS}
+\DeclareBoolOption{IEEE}
+\DeclareBoolOption{LNCS}
+\DeclareBoolOption{LNI}
+\DeclareBoolOption{nocopyright}
+\DeclareBoolOption{nourl}
+\DeclareBoolOption{nobib}
+\DeclareBoolOption{orcidicon}
+%\ProcessOptions\relax
+
+
+% Default option rule
+\DeclareDefaultOption{%
+  \ifx\CurrentOptionValue\relax
+    \PackageWarningNoLine{\@currname}{%
+      Unknown option `\CurrentOption'\MessageBreak
+      is passed to package `authorarchive'%
+    }%
+    % Pass the option to package color.
+    % Again it is better to expand \CurrentOption.
+    \expandafter\PassOptionsToPackage\expandafter{\CurrentOption}{color}%
+  \else
+    % Package color does not take options with values.
+    % We provide the standard LaTeX error.
+    \@unknownoptionerror
+  \fi
+}
+\ProcessKeyvalOptions*
+
+% Provide command for dynamic configuration seutp
+\def\authorsetup{\kvsetkeys{AA}}
+
+% Load local configuration
+\InputIfFileExists{authorarchive.config}{}{}
+
+
+\newlength\AA@x
+\newlength\AA@y
+\newlength\AA@width
+
+\def\AA@bibBibTeX{\AA@bibtexdir/\AA@key.bib}
+\def\AA@bibBibTeXLong{\AA@bibtexdir/\AA@key.bibtex}
+\def\AA@bibWord{\AA@bibtexdir/\AA@key.word.xml}
+\def\AA@bibEndnote{\AA@bibtexdir/\AA@key.enw}
+\def\AA@bibRIS{\AA@bibtexdir/\AA@key.ris}
+
+\newboolean{AA@bibExists}
+\setboolean{AA@bibExists}{false}
+\IfFileExists{\AA@bibBibTeX}{\setboolean{AA@bibExists}{true}}{}
+\IfFileExists{\AA@bibBibTeXLong}{\setboolean{AA@bibExists}{true}}{}
+\IfFileExists{\AA@bibWord}{\setboolean{AA@bibExists}{true}}{}
+\IfFileExists{\AA@bibEndnote}{\setboolean{AA@bibExists}{true}}{}
+\IfFileExists{\AA@bibRIS}{\setboolean{AA@bibExists}{true}}{}
+
+\setlength\AA@x{1in+\hoffset+\oddsidemargin}
+
+\newcommand{\authorcrfont}{\footnotesize}
+\newcommand{\authorat}[1]{\AtPageUpperLeft{\put(\LenToUnit{\AA@x},\LenToUnit{.2cm-\paperheight}){#1}}}
+\newcommand{\authorwidth}[1]{\setlength{\AA@width}{#1}}
+\setlength{\AA@width}{\textwidth}
+
+\def\AA@pageinfo{}
+\ifthenelse{\equal{\AA@startpage}{UNKNOWN START PAGE}}{%
+}{%
+  \setcounter{page}{\AA@startpage}%
+  \def\AA@pageinfo{pp. \thepage--\pageref{\aa@lastpage}, }
+}
+
+
+
+%%%% sig-alternate.cls
+\ifAA@ACM%
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=ACM}
+  }{}
+  \global\boilerplate={}
+  \global\copyrightetc={}
+  \renewcommand{\conferenceinfo}[2]{}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \setlength\AA@x{1in+\hoffset+\oddsidemargin}
+  \setlength\AA@y{-\textheight+\topmargin+\headheight-\footskip} % -\voffset-\topmargin-\headheight-\footskip}
+  \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},\LenToUnit{\AA@y}){#1}}
+  \setlength{\AA@width}{\columnwidth}
+\fi
+%
+%%%% acmart.cls
+\ifAA@acmart%
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=ACM}
+  }{}
+  \renewcommand{\authorat}[1]{\AtPageUpperLeft{\put(\LenToUnit{\AA@x},\LenToUnit{0.2cm-\paperheight}){#1}}}
+  \setlength{\AA@width}{\textwidth}
+\fi
+%
+%%%% LNCS
+\ifAA@LNCS%
+  \ifAA@orcidicon%
+    \renewcommand{\orcidID}[1]{\href{https://orcid.org/#1}{%
+      \textsuperscript{\,\includegraphics[height=2\fontcharht\font`A]{vector_iD_icon}}}}
+  \else\relax\fi%
+%  
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=Springer-Verlag}
+  }{}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \@ifclasswith{llncs}{a4paper}{%
+    \ExplSyntaxOn
+    \@ifundefined{pdfmanagement_add:nnn}{%
+      \pdfpagesattr{/CropBox [92 114 523 780]}%
+    }{%
+      \pdfmanagement_add:nnn {Pages}{CropBox}{[92~114~523~780]}
+    }%
+    \ExplSyntaxOff
+    \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},40){#1}}%
+  }{%
+    \ExplSyntaxOn
+    \@ifundefined{pdfmanagement_add:nnn}{%
+      \pdfpagesattr{/CropBox [92 65 523 731]}% LNCS page: 152x235 mm
+    }{%
+      \pdfmanagement_add:nnn {Pages}{CropBox}{[92~62~523~731]}
+    }%
+    \ExplSyntaxOff
+    \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},23){#1}}
+  }
+  \setlength{\AA@width}{\textwidth}
+  \setcounter{tocdepth}{2}
+\fi
+%
+%%%% LNI
+\ifAA@LNI%
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=GI}
+  }{}
+  \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},35){#1}}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \pdfpagesattr{/CropBox [70 65 526.378 748.15]} % TODO
+  \setlength{\AA@width}{\textwidth}
+  \setcounter{tocdepth}{2}
+\fi
+%
+%%%% ENTCS
+\ifAA@ENTCS%
+  \addtolength{\voffset}{1cm}
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=Elsevier Science B.~V.}
+  }{}
+  \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},\LenToUnit{-.5cm-\the\ht\AA@authoratBox}){#1}}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \setlength{\AA@width}{\textwidth}
+\fi
+%
+%%%% IEEE
+\ifAA@IEEE%
+  \ifthenelse{\equal{\AA@publisher}{UNKNOWN PUBLISHER}}{%
+    \setkeys{AA}{publisher=IEEE}
+  }{}
+  \renewcommand{\authorat}[1]{\put(\LenToUnit{\AA@x},6){#1}}
+  \renewcommand{\authorcrfont}{\scriptsize}
+  \setlength{\AA@width}{\textwidth}
+  \setcounter{tocdepth}{2}
+\fi
+%
+
+\hypersetup{%
+  draft         = false,
+  bookmarksopen = true,
+  bookmarksnumbered= true,
+  pdfauthor     = {\@author},
+  pdftitle      = {\@title},
+}
+
+\@ifpackageloaded{totpages}{%
+  \def\aa@lastpage{TotPages}
+}{%
+  \RequirePackage{lastpage}
+  \def\aa@lastpage{LastPage}
+}
+\newsavebox{\AA@authoratBox}
+
+\AddToShipoutPicture*{%
+  \setlength{\unitlength}{1mm}%
+  \savebox{\AA@authoratBox}{%
+    \parbox{1.4cm}{%
+      \bgroup%
+        \normallineskiplimit=0pt%
+        \ifAA@nourl%
+           \ifx\AA@doi\@empty\relax%
+           \else%
+              \qrcode[hyperlink,height=1.17cm,padding]{https://doi.org/\AA@doi}%
+            \fi%
+        \else%
+          \qrcode[hyperlink,height=1.17cm,padding]{\AA@baseurl/\AA@key\AA@suffix}%
+        \fi%
+      \egroup%
+    }%
+    \ifAA@nourl\ifx\AA@doi\@empty\addtolength{\AA@width}{1.4cm}\fi\fi
+    \parbox{\AA@width-1.4cm}{\authorcrfont%
+      \ifAA@LNCS%
+        \AA@publication, \AA@pageinfo  \AA@year. %
+        \ifAA@nocopyright\else
+          \textcopyright~\AA@year~\AA@publisher.
+        \fi
+        This is the author's
+        version of the work. It is posted
+        \ifAA@nourl\relax\else%
+          at \url{\AA@baseurl/\AA@key\AA@suffix} %
+        \fi
+        \ifAA@nocopyright\relax\else
+          by permission of \AA@publisher{}
+        \fi
+        for your personal use.
+        \ifx\AA@doi\@empty%
+          \relax
+        \else
+          The final publication is available at Springer via
+          \ifx\AA@doiText\@empty%
+            \url{https://doi.org/\AA@doi}.
+          \else
+            \href{https://doi.org/\AA@doi}{\AA@doiText}.
+          \fi
+        \fi
+      \else
+        \ifAA@nocopyright\relax\else
+          \textcopyright~\AA@year~\AA@publisher. %
+        \fi%
+        This is the author's
+        version of the work. It is posted
+        \ifAA@nourl\relax\else%
+          at \url{\AA@baseurl/\AA@key\AA@suffix} %
+        \fi
+        \ifAA@nocopyright\relax\else
+          by permission of \AA@publisher{} %
+        \fi
+        for your personal use. Not for redistribution. The definitive
+        version was published in \emph{\AA@publication}, \AA@pageinfo \AA@year%
+        \ifx\AA@doi\@empty%
+          \ifx\AA@publisherurl\@empty%
+            .%
+          \else
+            \url{\AA@publisherurl}.%
+          \fi
+        \else
+          \ifx\AA@doiText\@empty%
+            , doi: \href{https://doi.org/\AA@doi}{\AA@doi}.%
+          \else
+            , doi: \href{https://doi.org/\AA@doi}{\AA@doiText}.%
+          \fi
+        \fi
+      \fi
+      \ifAA@nobib\relax\else%
+        \ifthenelse{\boolean{AA@bibExists}}{%
+          \hfill
+          \begin{itemize*}[label={}, itemjoin={,}]
+            \IfFileExists{\AA@bibBibTeX}{%
+              \item \attachandlink{\AA@bibBibTeX}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
+            }{%
+              \IfFileExists{\AA@bibBibTeXLong}{%
+                \item \attachandlink[\AA@key.bib]{\AA@bibBibTeXLong}[application/x-bibtex]{BibTeX entry of this paper}{\BibTeX}%
+              }{%
+                \typeout{No file \AA@bibBibTeX{} (and no \AA@bibBibTeXLong) found. Not embedded reference in BibTeX format.}%
+              }%
+            }%
+            \IfFileExists{\AA@bibWord}{%
+              \item \attachandlink{\AA@bibWord}[application/xml]{XML entry of this paper (e.g., for Word 2007 and later)}{Word}%
+            }{%
+              \typeout{No file \AA@bibWord{} found. Not embedded reference for Word 2007 and later.}%
+            }%
+            \IfFileExists{\AA@bibEndnote}{%
+              \item \attachandlink{\AA@bibEndnote}[application/x-endnote-refer]{Endnote entry of this paper}{EndNote}%
+            }{%
+              \typeout{No file \AA@bibEndnote{} found. Not embedded reference in Endnote format.}%
+            }%
+            \IfFileExists{\AA@bibRIS}{%
+              \item \attachandlink{\AA@bibRIS}[application/x-research-info-systems]{RIS entry of this paper}{RIS}%
+            }{%
+              \typeout{No file \AA@bibRIS{} found. Not embedded reference in RIS format.}%
+            }%
+          \end{itemize*}\\
+        }{%
+          \PackageError{authorarchive}{No bibliographic files found. Specify option 'nobib' if this is intended.}
+        }
+      \fi
+    }
+  }
+  \authorat{\raisebox{\the\ht\AA@authoratBox}{\usebox{\AA@authoratBox}}}
+}

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/isadof.cfg

@@ -1,2 +1,2 @@
-Template: scrartcl
+Template: lncs
 Ontology: scholarly_paper

examples/scholarly_paper/2018-cicm-isabelle_dof-applications/document/preamble.tex

@@ -53,23 +53,18 @@
 \usepackage[size=footnotesize]{caption}
 
 
-\subject{Example of an Academic Paper\footnote{%
-  This document is an example setup for writing an academic paper. While
-  it is optimized for the Springer's LNCS class, it uses a Koma Script
-  LaTeX class to avoid the re-distribution of \texttt{llncs.cls},
-  which would violate Springer's copyright. This example has been
-  published at CICM 2018:
-    \protect\begin{quote}
-      Achim D. Brucker, Idir Ait-Sadoune, Paolo Crisafulli, and
-      Burkhart Wolff. Using The Isabelle Ontology Framework: Linking
-      the Formal with the Informal. In Conference on Intelligent
-      Computer Mathematics (CICM). Lecture Notes in Computer Science
-      (11006), Springer-Verlag, 2018. 
-    \protect\end{quote}
-    Note that the content of this example is not updated and, hence,
-    might not be correct with respect to the latest version of
-    \isadof{}. 
-    }}
+\usepackage[LNCS,
+   orcidicon,
+   key=brucker.ea-isabelle-ontologies-2018,
+   year=2018,
+   publication={F. Rabe et al. (Eds.): CICM 2018, LNAI 11006},
+   nobib,
+   startpage={1},
+   doi={10.1007/978-3-319-96812-4_3},
+   doiText={10.1007/978-3-319-96812-4\_3},
+]{authorarchive}
+\authorrunning{A. D. Brucker et al.}
+\pagestyle{headings}
 
 
 \title{<TITLE>}

examples/scholarly_paper/2021-ITP-PMTI/ROOT

@@ -1,13 +1,11 @@
 session "2021-ITP-PMTI" = "Isabelle_DOF" +
-  options [document = pdf, document_output = "output", document_build = dof,
-    document_comment_latex = true]
+  options [document = pdf, document_output = "output", document_build = dof]
   theories
     "paper"
   document_files
     "isadof.cfg"
     "root.bib"
     "preamble.tex"
-    "spmpscinat.bst"
     "figures/Req-Appl-ex.png"
     "figures/formal-development.png"
     "figures/Req-Def-ex.png"

examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy

@@ -181,7 +181,6 @@ Usage: isabelle mkroot_DOF [OPTIONS] [DIR]
     -o ONTOLOGY  (default: scholarly_paper)
        Available ontologies:
        * CENELEC_50128
-       * math_exam
        * scholarly_paper
        * technical_report
     -t TEMPLATE   (default: scrartcl)
@@ -505,9 +504,6 @@ side_by_side_figure*["hyperlinks"::side_by_side_figure,anchor="''fig:Dogfood-IV-
                       caption2="''Exploring an attribute (hyperlinked to the class).''",
                       relative_width2="47",
                       src2="''figures/Dogfood-V-attribute''"]\<open>Navigation via generated hyperlinks.\<close>
-(* TODO: Update the images in fig:Dogfood-IV-jumpInDocCLass side_by_side_figure
-   to align them. This has to wait that the exploration of an attribute is again possible.
-   See: https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF/issues/10 *)
 
 text\<open> 
   From these class definitions, \<^isadof> also automatically generated editing 

examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy

@@ -331,7 +331,7 @@ is currently only available in the SML API's of the kernel.
   symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
   evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
 \<^item> \<open>upd_meta_args\<close> :
-   \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
+   \<^rail>\<open> (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\<close>
 \<^item> \<open>annotated_text_element\<close> :
 \<^rail>\<open> 
     (  @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
@@ -1009,9 +1009,6 @@ text\<open>
   these types. They are just types declared in HOL, 
   which are ``inhabited'' by special constant symbols carrying strings, for
   example of the format \<^boxed_theory_text>\<open>@{thm <string>}\<close>.
-  % TODO:
-  % Update meta-types implementation explanation to the new implementation
-  % in repository commit 08c101c5440eee2a087068581952026e88c39f6a
   When HOL
   expressions were used to denote values of \<^boxed_theory_text>\<open>doc_class\<close>
   instance attributes, this requires additional checks after

src/DOF/Isa_DOF.thy

@@ -1010,8 +1010,6 @@ fun elaborate_instances_list thy isa_name _ _ _ =
     val base_name' = DOF_core.get_class_name_without_prefix (base_name_without_suffix)
     val class_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
                                                 (base_name')
-    val class_list_typ = Proof_Context.read_typ (Proof_Context.init_global thy)
-                                                (base_name' ^ " List.list")
     val tab = #tab(#docobj_tab(DOF_core.get_data_global thy))
     val table_list = Symtab.dest tab
     fun get_instances_name_list _ [] = []
@@ -1028,13 +1026,7 @@ fun elaborate_instances_list thy isa_name _ _ _ =
           end
     val long_class_name = DOF_core.read_cid_global thy base_name'
     val values_list = get_instances_name_list long_class_name table_list
-    val hol_list_terms_list =
-      fold
-        (fn x =>
-         fn y =>
-         Const (@{const_name "Cons"}, [class_typ, class_list_typ] ---> class_list_typ) $ x $ y)
-        values_list (Const (@{const_name "Nil"}, class_list_typ))
-  in hol_list_terms_list end
+  in HOLogic.mk_list class_typ values_list end
 
 fun declare_class_instances_annotation thy doc_class_name =
   let
@@ -1244,13 +1236,34 @@ fun infer_type thy term = hd (Type_Infer_Context.infer_types (Proof_Context.init
 
 fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long
                      (S:(string * Position.T * string * term)list) term = 
-    let val cid_ty = cid_2_cidType cid_long thy 
+    let val cid_ty = cid_2_cidType cid_long thy
         val generalize_term =  Term.map_types (generalize_typ 0)
         fun toString t = Syntax.string_of_term (Proof_Context.init_global thy) t  
         fun instantiate_term S t =
           Term_Subst.map_types_same (Term_Subst.instantiateT (TVars.make S)) (t)
         fun read_assn (lhs, pos:Position.T, opr, rhs) term =
-            let val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy
+            let 
+                fun get_class_name parent_cid attribute_name pos =
+                  let
+                    val {attribute_decl, inherits_from, ...} =
+                                                   the (DOF_core.get_doc_class_global parent_cid thy)
+                  in
+                    if exists (fn (binding, _, _) => Binding.name_of binding = attribute_name)
+                              attribute_decl
+                    then parent_cid
+                    else
+                      case inherits_from of
+                          NONE =>
+                                ISA_core.err ("Attribute not defined for class: " ^ cid_long) pos
+                        | SOME (_, parent_name) =>
+                                              get_class_name parent_name attribute_name pos
+                  end
+                val attr_defined_cid = get_class_name cid_long lhs pos
+                val {id, name, ...} = the (DOF_core.get_doc_class_global attr_defined_cid thy)
+                val markup = docclass_markup false cid_long id (Binding.pos_of name);
+                val ctxt = Context.Theory thy
+                val _    = Context_Position.report_generic ctxt pos markup;
+                val info_opt = DOF_core.get_attribute_info cid_long (Long_Name.base_name lhs) thy
                 val (ln,lnt,lnu,lnut) = case info_opt of 
                                            NONE => error ("unknown attribute >" 
                                                           ^((Long_Name.base_name lhs))
@@ -1353,14 +1366,11 @@ fun check_invariants thy oid =
   let
     val value = the (DOF_core.get_value_global oid thy)
     val cid = #cid (the (DOF_core.get_object_global oid thy))
-    (*val _ = writeln ("cid: " ^ @{make_string} (Long_Name.base_name cid))*)
     fun get_all_invariants cid thy =
-      let val invs = #invs (the (DOF_core.get_doc_class_global cid thy))
-      in case DOF_core.get_doc_class_global cid thy of
-             NONE => error("undefined class id for invariants: " ^ cid)
-           | SOME ({inherits_from=NONE, ...}) => invs
-           | SOME ({inherits_from=SOME(_,father), ...}) => (invs) @ (get_all_invariants father thy)
-      end
+       case DOF_core.get_doc_class_global cid thy of
+          NONE => error("undefined class id for invariants: " ^ cid)
+        | SOME ({inherits_from=NONE, invs, ...}) => invs
+        | SOME ({inherits_from=SOME(_,father), invs, ...}) => (invs) @ (get_all_invariants father thy)
     val invariants = get_all_invariants cid thy
     val inv_and_apply_list = 
       let fun mk_inv_and_apply inv value thy =
@@ -2008,7 +2018,7 @@ fun print_doc_items b ctxt =
                   writeln ("    type:            "^cid);
                   case vcid of NONE => () | SOME (s) => 
                   writeln ("    virtual type:    "^ s);
-                  writeln ("    origine:         "^thy_name);
+                  writeln ("    origin:          "^thy_name);
                   writeln ("    inline:          "^dfg inline);
                   writeln ("    input_term:      "
                            ^ (Syntax.string_of_term

src/ROOT

@@ -7,8 +7,6 @@ session "Isabelle_DOF" = "Functional-Automata" +
     "ontologies"
     "ontologies/CENELEC_50128"
     "ontologies/Conceptual"
-    "ontologies/math_exam"
-    "ontologies/math_paper"
     "ontologies/scholarly_paper"
     "ontologies/small_math"
     "ontologies/technical_report"

src/Tools/mkroot_DOF

@@ -90,7 +90,7 @@ do
       NAME="$OPTARG"
       ;;
     o)
-      if [ ! -f "$ISABELLE_DOF_HOME/src/ontologies/*//DOF-$OPTARG.sty" ]; then
+      if [ ! -f "$ISABELLE_DOF_HOME/src/ontologies"/*/DOF-$OPTARG.sty ]; then
           echo "ERROR: Ontology $OPTARG not available!"
           exit 1
       fi

src/document-templates/root-lncs.tex

@@ -31,7 +31,6 @@
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{DOF-amssymb}
-\usepackage[numbers, sort&compress, sectionbib]{natbib}
 \IfFileExists{DOF-core.sty}{}{%
   \PackageError{DOF-core}{Isabelle/DOF not installed. 
     This is a Isabelle_DOF project. The document preparation requires
@@ -102,7 +101,7 @@
 {\small   \renewcommand{\doi}[1]{}
   \newcommand{\urlprefix}{}
 
-  \bibliographystyle{spmpscinat}
+  \bibliographystyle{splncs04}
   
   \bibliography{root}
 }}{}