comment inside meta_args problem solved.

Isa_DOF.thy

@@ -686,21 +686,25 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : meta_args_t) =
 
 val semi = Scan.option (Parse.$$$ ";");
 val is_improper = not o (Token.is_proper orf Token.is_begin_ignore orf Token.is_end_ignore);
-val improper = Scan.many is_improper;
+val improper = Scan.many is_improper; (* parses white-space and comments *)
 
 val attribute =
     Parse.position Parse.const
     --| improper 
-    -- Scan.optional (Parse.$$$ "=" --| improper |-- Parse.!!! Parse.term) "True"
+    -- Scan.optional (Parse.$$$ "=" --| improper |-- Parse.!!! Parse.term --| improper) "True"
    : ((string * Position.T) * string) parser;
 
 val attribute_upd  : (((string * Position.T) * string) * string) parser =
     Parse.position Parse.const 
-    -- (@{keyword "+="} || @{keyword ":="})
+    --| improper
-    -- Parse.!!! Parse.term;
+    -- ((@{keyword "+="} --| improper) || (@{keyword ":="} --| improper))
+    -- Parse.!!! Parse.term
+    --| improper
+    : (((string * Position.T) * string) * string) parser;
 
 val reference =
     Parse.position Parse.name 
+    --| improper
     -- Scan.option (Parse.$$$ "::" -- improper |-- Parse.!!! (Parse.position Parse.name));
 
 
@@ -717,7 +721,7 @@ val attributes_upd =
      -- improper 
      |-- (reference -- 
          (Scan.optional(Parse.$$$ "," -- improper |-- (Parse.enum "," (improper |-- attribute_upd)))) []))
-     --| Parse.$$$ "]"
+     --| Parse.$$$ "]" 
 
 
 

examples/scholarly/IsaDofApplications.thy

@@ -4,24 +4,29 @@ theory IsaDofApplications
 begin
 (*>*)  
  
-title*[
+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,
+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''",
+      email       = "''idir.aitsadoune@centralesupelec.fr''",
-      affiliation="''CentraleSupelec, Paris, France''"]\<open>Idir Ait-Sadoune\<close>
+      affiliation = "''CentraleSupelec, Paris, France''"]\<open>Idir Ait-Sadoune\<close>
 text*[paolo::author,
-      email="''paolo.crisafulli@irt-systemx.fr''",
+      email      = "''paolo.crisafulli@irt-systemx.fr''",
-      affiliation="''IRT-SystemX, Paris, France''"]\<open>Paolo Crisafulli\<close>
+      affiliation= "''IRT-SystemX, Paris, France''"]\<open>Paolo Crisafulli\<close>
 text*[bu::author,
-      email = "''wolff@lri.fr''",
+      email       = "''wolff@lri.fr''",
-      affiliation="''Universit\\'e Paris-Sud, Paris, France''"]\<open>Burkhart Wolff\<close>
+      affiliation = "''Universit\\'e Paris-Sud, Paris, France''"]\<open>Burkhart Wolff\<close>
     
 
 text*[abs::abstract,

patches/thy_output.ML

@@ -408,23 +408,6 @@ val locale =
   Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
     Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
 
-(*
-val reference =
-    Parse.position Parse.name 
-    -- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name));
-
-val attribute =
-    Parse.position Parse.const 
-    -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.term) "";
-
-val attributes =  
-    (Parse.$$$ "[" 
-     |-- (reference -- 
-         (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) []))
-     --| Parse.$$$ "]"
-
-fun convert_meta_args (NONE : ((((string * Position.T) * (string * Position.T) option) * ((string * Position.T) * string) list) option)) = ""
-*)
 val meta_args_parser_hook =  Unsynchronized.ref((fn thy => fn s => ("",s)): theory -> string parser)
 
 
@@ -441,15 +424,15 @@ fun present_thy thy command_results toks =
 
     fun markup pred mk flag = Scan.peek (fn d =>
       improper |--
-        Parse.position (Scan.one (fn tok =>
+        Parse.position (Scan.one (fn tok =>  Token.is_command tok andalso 
-          Token.is_command tok andalso pred keywords (Token.content_of tok))) --
+                                             pred keywords (Token.content_of tok))) --
       Scan.repeat tag --
-      Parse.!!!! 
+      (improper |--
-      (    (!meta_args_parser_hook thy)
+      (Parse.!!!! 
-         --
+      (  (!meta_args_parser_hook thy)
-           (  (improper -- locale -- improper) 
+         -- (  (improper -- locale -- improper) 
          |-- (Parse.document_source)) 
-         --| improper_end)
+         --| improper_end)))
       >> (fn (((tok, pos'), tags), (meta_args,source)) =>
         let val name = Token.content_of tok
         in (SOME (name, pos', tags), (mk (name, meta_args, source), (flag, d))) end));