From eaca1959ce1d29fccc9d80230d3609adc8a9145f Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Thu, 4 Oct 2018 16:58:09 +0200
Subject: [PATCH] Intermediate status : some spacing works.

---
 Isa_DOF.thy                               | 17 ++++++++++-------
 examples/scholarly/IsaDofApplications.thy | 22 +++++++++++++++-------
 ontologies/scholarly_paper.thy            |  4 +++-
 3 files changed, 28 insertions(+), 15 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index cce53d32..fb92e40e 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -511,7 +511,7 @@ fun write_ontology_latex_sty_template thy =
                    (* or parameterising with "env" ? ? ?*)
             else ""
         val content = String.concat(map write_class (Symtab.dest y))
-        val _ = writeln content
+        (* val _ = writeln content  -- for interactive testing only, breaks LaTeX compilation *) 
     in  writeFile ("Isa-DOF."^curr_thy_name^".template.sty") content
     end;
 
@@ -689,8 +689,10 @@ val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_
 val improper = Scan.many is_improper;
 
 val attribute =
-    Parse.position Parse.const 
-    -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.term) "True";
+    Parse.position Parse.const
+    --| improper 
+    -- Scan.optional (Parse.$$$ "=" --| improper |-- Parse.!!! Parse.term) "True"
+   : ((string * Position.T) * string) parser;
 
 val attribute_upd  : (((string * Position.T) * string) * string) parser =
     Parse.position Parse.const 
@@ -703,17 +705,18 @@ val reference =
 
 
 val attributes =  
-    (Parse.$$$ "["
+    ((Parse.$$$ "["
       -- improper 
      |-- (reference -- 
-         (Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," ( attribute)))) []))
-     --| Parse.$$$ "]" : meta_args_t parser 
+         (Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," (improper |-- attribute)))) []))
+     --| Parse.$$$ "]"
+     --| improper)  : meta_args_t parser 
 
 val attributes_upd =  
     (Parse.$$$ "[" 
      -- improper 
      |-- (reference -- 
-         (Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," attribute_upd))) []))
+         (Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," (improper |-- attribute_upd)))) []))
      --| Parse.$$$ "]"
 
 
diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy
index ca8f5b3e..5cad9b8e 100644
--- a/examples/scholarly/IsaDofApplications.thy
+++ b/examples/scholarly/IsaDofApplications.thy
@@ -5,19 +5,27 @@ begin
 (*>*)  
  
 title*[
-tit::
-       title]\<open>Using the Isabelle Ontology Framework\<close> 
+tit::title]\<open>Using the Isabelle Ontology Framework\<close> 
 subtitle*[stit::subtitle]
 \<open>Linking the Formal with the Informal\<close>
 
 text*[adb::author,
-      email="''a.brucker@sheffield.ac.uk''",orcid="''0000-0002-6355-1200''",affiliation="''The University of Sheffield, Sheffield, UK''"]\<open>Achim D. Brucker\<close>
-text*[idir::author,email="''idir.aitsadoune@centralesupelec.fr''",affiliation="''CentraleSupelec, Paris, France''"]\<open>Idir Ait-Sadoune\<close>
-text*[paolo::author,email="''paolo.crisafulli@irt-systemx.fr''",affiliation="''IRT-SystemX, Paris, France''"]\<open>Paolo Crisafulli\<close>
-text*[bu::author,email="''wolff@lri.fr''",affiliation="''Universit\\'e Paris-Sud, Paris, France''"]\<open>Burkhart Wolff\<close>
+      email="''a.brucker@sheffield.ac.uk''",
+      orcid="''0000-0002-6355-1200''",
+      affiliation="''The University of Sheffield, Sheffield, UK''"]\<open>Achim D. Brucker\<close>
+text*[idir::author,
+      email="''idir.aitsadoune@centralesupelec.fr''",
+      affiliation="''CentraleSupelec, Paris, France''"]\<open>Idir Ait-Sadoune\<close>
+text*[paolo::author,
+      email="''paolo.crisafulli@irt-systemx.fr''",
+      affiliation="''IRT-SystemX, Paris, France''"]\<open>Paolo Crisafulli\<close>
+text*[bu::author,
+      email = "''wolff@lri.fr''",
+      affiliation="''Universit\\'e Paris-Sud, Paris, France''"]\<open>Burkhart Wolff\<close>
     
 
-text*[abs::abstract,keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\<open>
+text*[abs::abstract,
+      keywordlist="[''Ontology'',''Ontological Modeling'',''Isabelle/DOF'']"]\<open>
 While Isabelle is mostly known as part of Isabelle/HOL (an interactive 
 theorem prover), it actually provides a framework for developing a wide
 spectrum of applications. A particular strength
diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy
index 44a86a3d..6bf627a2 100644
--- a/ontologies/scholarly_paper.thy
+++ b/ontologies/scholarly_paper.thy
@@ -88,8 +88,10 @@ doc_class article =
            \<lbrace>technical || example\<rbrace>\<^sup>+ ~~ 
            conclusion   ~~  
            bibliography)"
-(*
+
+(* breaks currently LaTeX compilation:
 gen_sty_template
 *)
+
 end