From a792cc79d24341ff7e706190fd26102aa8110db6 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 25 Aug 2020 11:11:38 +0200
Subject: [PATCH] was lucky to solve a deep bug in standard antiquotation
 evaluation inside text* soon.

---
 .../Isabelle_DOF-Manual/01_Introduction.thy   |  2 +-
 src/DOF/Isa_DOF.thy                           | 52 ++++++++++++++++++-
 src/tests/OutOfOrderPresntn.thy               |  2 +-
 3 files changed, 52 insertions(+), 4 deletions(-)

diff --git a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
index 2c8f29c3..9660248d 100755
--- a/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/01_Introduction.thy
@@ -33,7 +33,7 @@ have to follow a structure.  In practice, large groups of developers have to pro
 set of documents where the consistency is notoriously difficult to maintain. In particular, 
 certifications are centered around the \<^emph>\<open>traceability\<close> of requirements throughout the entire 
 set of documents. While technical solutions for the traceability problem exists (most notably:
-DOORS~\cite{ibm:doors:2019}), they are weak in the treatment of formal entities (such as formulas 
+DOORS~@{cite "ibm:doors:2019"}), they are weak in the treatment of formal entities (such as formulas 
 and their logical contexts).
 
 Further applications are the domain-specific discourse in juridical texts or medical reports.  
diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index 94953af8..f0a24b6b 100755
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -714,8 +714,15 @@ end (* struct *)
 
 setup\<open>DOF_core.strict_monitor_checking_setup\<close>
 
+section\<open> Syntax for Term Annotation Antiquotations (TA)\<close>
 
-section\<open> Syntax for Inner Syntax Antiquotations (ISA) \<close>
+text\<open>Isabelle/DOF allows for annotations at the term level, for which an
+antiquotation syntax and semantics is defined at the inner syntax level.
+(For this reasons, the mechanism has been called somewhat misleading
+\<^emph>\<open>inner syntax antiquotations\<close> in earlier versions of Isabelle/DOF.)
+
+For the moment, only a fixed number of builtin TA's is supported, future
+versions might extend this feature substantially.\<close>
 
 subsection\<open> Syntax \<close> 
 
@@ -1248,6 +1255,47 @@ fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transfor
   end;
 
 
+fun gen_enriched_document_command2 {inline=is_inline} cid_transform attr_transform 
+                                  markdown  
+                                  (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
+                                     xstring_opt:(xstring * Position.T) option),
+                                    toks:Input.source) 
+                                  : theory -> theory =
+  let  val toplvl = Toplevel.theory_toplevel
+
+       (* as side-effect, generates markup *)
+       fun check_n_tex_text thy = let val ctxt = Toplevel.presentation_context (toplvl thy);
+                                      val pos = Input.pos_of toks;
+                                      val _ =   Context_Position.reports ctxt
+                                                [(pos, Markup.language_document (Input.is_delimited toks)),
+                                                 (pos, Markup.plain_text)];
+
+                                      val text = Thy_Output.output_document 
+                                                                 (Proof_Context.init_global thy) 
+                                                                 markdown toks
+
+                                      val file = {path = Path.make [oid ^ "_snippet.tex"],
+                                                  pos = @{here}, 
+                                                  content = Latex.output_text text}
+ 
+                                  (*    val _ = Generated_Files.write_file (Path.make ["latex_test"]) 
+                                                                         file
+                                      val _ = writeln (Latex.output_text text) *)
+                                  in  thy end
+       
+       (* ... generating the level-attribute syntax *)
+  in   
+       (* ... level-attribute information management *)
+       (   create_and_check_docitem 
+                              {is_monitor = false} {is_inline = is_inline} 
+                              oid pos (cid_transform cid_pos) (attr_transform doc_attrs)
+       (* checking and markup generation *)
+        #>  check_n_tex_text ) 
+       (* Thanks Frederic Tuong for the hints concerning toplevel ! ! ! *)
+  end;
+
+
+
 (* General criticism : attributes like "level" were treated here in the kernel instead of dragging
    them out into the COL -- bu *)
 
@@ -1320,7 +1368,7 @@ val _ =
 val _ =
   Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
     (attributes -- Parse.opt_target -- Parse.document_source 
-      >> (Toplevel.theory o (gen_enriched_document_command {inline=true} 
+      >> (Toplevel.theory o (gen_enriched_document_command2 {inline=true} 
                                                            I I {markdown = true} )));
 
 (* This is just a stub at present *)
diff --git a/src/tests/OutOfOrderPresntn.thy b/src/tests/OutOfOrderPresntn.thy
index cf0dc27d..cfc99436 100644
--- a/src/tests/OutOfOrderPresntn.thy
+++ b/src/tests/OutOfOrderPresntn.thy
@@ -121,7 +121,7 @@ Tool: Sphinx.
 
 \<close>
 
-text*[aaa::B]\<open>dfg\<close>
+text*[aaa::B]\<open>dfg @{thm [display] refl}\<close>
 
 text-[dfgdfg::B]
 \<open> Lorem ipsum ...  @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>