From b56c02cd6ae7a122f5c2fe977d0c2485120d1240 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Fri, 17 Aug 2018 13:19:12 +0200
Subject: [PATCH] Repaired bug in the meta-args parser.

LaTeX generation for Text* environments with
antiquotation expansion works for the first time.
---
 Isa_DOF.thy                               | 12 +++++++-----
 examples/scholarly/IsaDofApplications.thy |  4 ++--
 2 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/Isa_DOF.thy b/Isa_DOF.thy
index 5762949f..6d717056 100644
--- a/Isa_DOF.thy
+++ b/Isa_DOF.thy
@@ -395,12 +395,13 @@ fun meta_args_2_string thy (((lab, _), cid_opt), attr_list) =
     (* for the moment naive, i.e. without textual normalization of attribute names and 
        adapted term printing *)
     let val l   = "label = "^lab
-        val cid = "cid =" ^ (case cid_opt of
+        val cid = "type = " ^ (case cid_opt of
                                 NONE => DOF_core.default_cid
                               | SOME(cid,_) => DOF_core.name2doc_class_name thy cid) 
-        fun str ((lhs,_),rhs) = lhs^"="^rhs  (* no normalization on lhs (could be long-name)
-                                                no paraphrasing on rhs (could be fully paranthesized
-                                                pretty-printed formula in LaTeX notation ... *)
+        fun str ((lhs,_),rhs) = lhs^" = "^(enclose "{" "}" rhs)  
+                                (* no normalization on lhs (could be long-name)
+                                   no paraphrasing on rhs (could be fully paranthesized
+                                   pretty-printed formula in LaTeX notation ... *)
     in  enclose "[" "]" (commas ([l,cid] @ (map str attr_list))) end
 
 val semi = Scan.option (Parse.$$$ ";");
@@ -628,7 +629,8 @@ val _ =
 (* this sets parser and converter for LaTeX generation of meta-attributes. 
    Currently of *all* commands, no distinction between text* and text command. 
 *)
-val _ = Thy_Output.set_meta_args_parser (fn thy => attributes >> meta_args_2_string thy)
+val _ = Thy_Output.set_meta_args_parser 
+             (fn thy => (Scan.optional (attributes >> meta_args_2_string thy) "")) 
 
 end (* struct *)
 
diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy
index 7a39c49b..e61d22cf 100644
--- a/examples/scholarly/IsaDofApplications.thy
+++ b/examples/scholarly/IsaDofApplications.thy
@@ -293,9 +293,9 @@ figure*[fig1::figure, spawn_columns=False,relative_width="''95''",
        \<open> Ouroboros I: This paper from inside \ldots \<close>  
 
 text*[ctest2]\<open>This is a crucial test : @{docitem_ref \<open>fig1\<close>} @{thm "refl"}\<close>
-(*
+
 Text*[ctest]\<open>This is a crucial test : @{docitem_ref \<open>fig1\<close>} @{thm "refl"}\<close>
-*)
+
 
 text\<open> @{docitem_ref \<open>fig1\<close>} shows the corresponding view in the Isabelle/PIDE of the present paper.
 Note that the text uses \isadof's own text-commands containing the meta-information provided by