From 396ef1d477fbaf4704c00812f21ebbde7a200ccf Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolff@lri.fr>
Date: Fri, 1 Jan 2021 21:23:21 +0100
Subject: [PATCH] More content in 4, better tree printing.

---
 .../Isabelle_DOF-Manual/04_RefMan.thy         | 58 ++++++++++++++++++-
 src/DOF/Isa_DOF.thy                           |  4 +-
 2 files changed, 58 insertions(+), 4 deletions(-)

diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
index 7d646f9..eea9246 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
@@ -412,7 +412,7 @@ text\<open>
       setup\<open> DOF_lib.define_macro \<^binding>\<open>vs\<close>  "\\vspace{" "}" (check_latex_measure) \<close> 
     \<close>}
   where \<^ML>\<open>check_latex_measure\<close> is a hand-programmed function that checks 
-  of the input syntax.
+  the input for syntactical and static semantic constraints.
 \<close>
 
 
@@ -502,14 +502,68 @@ which are not "ontology-aware" but function similar otherwise.\<close>
 
 subsection*["text-elements"::technical]\<open>The Ontology \<^theory>\<open>Isabelle_DOF.scholarly_paper\<close>\<close>
 (*<*)
-ML\<open>writeln (DOF_core.print_doc_class_tree @{context} (fn (n,l) => String.isPrefix "scholarly_paper" l) I)\<close>
+ML\<open>val toLaTeX = String.translate (fn c => if c = #"_" then "\\_" else String.implode[c])\<close>     
+ML\<open>writeln (DOF_core.print_doc_class_tree 
+                 @{context} (fn (n,l) =>        String.isPrefix "scholarly_paper" l 
+                                         orelse String.isPrefix "Isa_COL" l) 
+                 toLaTeX)\<close>
 (*>*)
+text\<open>The \<^verbatim>\<open>scholarly_paper\<close> ontology extends \<^verbatim>\<open>COL\<close> by the following concepts:
+\begin{center}
+\begin{minipage}{.9\textwidth}
+\dirtree{%
+.0 .
+.1 scholarly\_paper.title.
+.1 scholarly\_paper.subtitle.
+.1 scholarly\_paper.author{An Author Entity Declaration}.
+.1 scholarly\_paper.abstract.
+.1 Isa\_COL.text\_element.
+.2 scholarly\_paper.text\_section{A Subclass for Major Paper Text-Elements}.    
+.3 scholarly\_paper.introduction{...}.
+.3 scholarly\_paper.conclusion{...}.
+.4 scholarly\_paper.related\_work{...}.
+.3 scholarly\_paper.bibliography{...}.
+.3 scholarly\_paper.annex{...}.
+.3 scholarly\_paper.example{...}.
+.3 scholarly\_paper.technical{Freeform Class for Technical Content}.
+.4 ... 
+.4 scholarly\_paper.math\_content{...}.
+.5 scholarly\_paper.definition{Freeform Definition}.
+.5 scholarly\_paper.lemma{Freeform Lemma}.
+.5 scholarly\_paper.theorem{...}.
+.5 scholarly\_paper.corollary{...}.
+.5 scholarly\_paper.math\_example{...}.
+.5 scholarly\_paper.math\_semiformal{...}.
+.4 scholarly\_paper.tech\_example{...}.
+.4 scholarly\_paper.math\_motivation{...}.
+.4 scholarly\_paper.math\_explanation{...}.
+.4 scholarly\_paper.engineering\_content{...}.
+.5 scholarly\_paper.data{...}.
+.5 scholarly\_paper.evaluation{...}.
+.5 scholarly\_paper.experiment{...}.
+.1 ... 
+.1 scholarly\_paper.article{The Paper Monitor}.
+.1 \ldots.
+}
+\end{minipage}
+\end{center}
+\<close>
+
+text\<open>They were alltogether also supported 
+
+\<close>
+
+
+
+subsubsection*["text-elements-expls"::technical]\<open>Examples\<close>
+
 text\<open>
   While the default user interface for class definitions via the  
   \<^boxed_theory_text>\<open>text*\<open> ... \<close>\<close>-command allow to access all features of the document 
   class, \<^isadof> provides short-hands for certain, widely-used, concepts such as 
   \<^boxed_theory_text>\<open>title*\<open> ... \<close>\<close> or \<^boxed_theory_text>\<open>section*\<open> ... \<close>\<close>, \<^eg>:
 
+
 @{boxed_theory_text [display]\<open>
  title*[title::title]\<open>Isabelle/DOF\<close>
  subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index ffbee3e..48604d5 100755
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -679,12 +679,12 @@ fun print_doc_class_tree ctxt P T =
         fun is_class_son X (n, dc:docclass_struct) = (X = #inherits_from dc)
         fun tree lev ([]:(string * docclass_struct)list) = ""
            |tree lev ((n,R)::S) = (if P(lev,n) 
-                                  then "."^Int.toString lev^" "^(T n)^"\n"
+                                  then "."^Int.toString lev^" "^(T n)^"{...}.\n"
                                        ^ (tree(lev + 1)(filter(is_class_son(SOME([],n)))class_tab))
                                   else "."^Int.toString lev^" ... \n") 
                                   ^ (tree lev S)
         val roots = filter(is_class_son NONE) class_tab
-    in  tree 0 roots end
+    in  ".0 .\n" ^ tree 1 roots end