solved presentation bug (brown) and eliminated some code dups

examples/CC_ISO15408/PikeOS_study/PikeOS_ST.thy

@@ -14,15 +14,16 @@ subsection*[pkosstrefsubsec::st_ref_cls]\<open> ST Reference \<close>
 
 text"@{docitem st_def}"
 text*[pkosstref::st_ref_cls, title="''PikeOS Security Target''", st_version ="(0,4,5)",
-      authors= "[]", st_date= "''29072020''"]\<open>This document is the @{docitem st_def} for the 
+      authors= "[]", st_date= "''29072020''"]
-      Common Criteria evaluation of PikeOS. It complies with the Common Criteria for Information 
+\<open>This document is the @{docitem st_def} for the Common Criteria evaluation of PikeOS. 
-      Technology Security Evaluation Version 3.1 Revision 4.\<close>
+ It complies with the Common Criteria for Information Technology Security Evaluation 
+ Version 3.1 Revision 4.\<close>
 
 subsection*[pkossttoerefsubsec::st_ref_cls]\<open> TOE Reference \<close>
 
 text*[pkostoeref::toe_ref_cls, dev_name="''''", toe_name="''PikeOS''",
       toe_version= "(0,3,4)", prod_name="Some ''S3725''"]
-  \<open>The @{docitem toe_def} is the operating system PikeOS version 3.4 
+\<open>The @{docitem toe_def} is the operating system PikeOS version 3.4 
    running on the microprocessor family x86 hosting different applications. 
    The @{docitem toe_def} is referenced as PikeOS 3.4 base
    product build S3725 for Linux and Windows development host with PikeOS 3.4

src/DOF/Isa_DOF.thy

@@ -1231,9 +1231,15 @@ fun gen_enriched_document_command {inline=is_inline} cid_transform attr_transfor
   let  val toplvl = Toplevel.theory_toplevel
        (* checking and markup generation *)
        fun check thy = let val ctxt = Toplevel.presentation_context (toplvl thy);
-                           val _ =  Context_Position.report ctxt
+                         (*  val _ =  Context_Position.report ctxt
                                           (Input.pos_of toks) 
                                           (Markup.language_document (Input.is_delimited toks));
+                          *)
+    val pos = Input.pos_of toks;
+    val _ =
+      Context_Position.reports ctxt
+        [(pos, Markup.language_document (Input.is_delimited toks)),
+         (pos, Markup.plain_text)];
                        in thy end
        
        (* ... generating the level-attribute syntax *)
@@ -1800,6 +1806,7 @@ val _ =
 end (* struct *)
 \<close>  
 
+text\<open>dfgd\<close>
 (*
 ML\<open>
    Pretty.text;

src/tests/OutOfOrderPresntn.thy

@@ -38,17 +38,7 @@ Symtab.dest docclass_tab;
 ML\<open> 
 Pure_Syn.document_command;
 
-fun output_document state markdown src =
+val _ = Thy_Output.output_document
-  let
-    val ctxt = Toplevel.presentation_context state;
-    val _ = Context_Position.report ctxt
-                (Input.pos_of src) 
-                (Markup.language_document (Input.is_delimited src));
-  in Thy_Output.output_document ctxt markdown src end;
-  (* this thing converts also source to (latex) text ... *)
-
-output_document : Toplevel.state -> {markdown: bool} -> Input.source -> Latex.text list;
-
 
 fun gen_enriched_document_command2 cid_transform attr_transform 
                                   markdown  
@@ -59,7 +49,14 @@ fun gen_enriched_document_command2 cid_transform attr_transform
   let  val toplvl = Toplevel.theory_toplevel
 
        (* as side-effect, generates markup *)
-       fun check_n_tex_text thy = let val text = output_document (toplvl thy) markdown toks
+       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}
@@ -95,6 +92,8 @@ text*[aaa::B]\<open>dfg\<close>
 text-[dfgdfg::B]
 \<open> Lorem ipsum ...  @{thm [display] refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
 
+
+
 text-[asd::B]
 \<open>... and here is its application macro expansion: 
      @{B [display] "dfgdfg"} 
@@ -104,7 +103,12 @@ text-[asd::B]
           \<close>}
 \<close>
 
-
+text\<open>... and here is its application macro expansion: 
+     @{B [display] "dfgdfg"} 
+     @{cartouche [display] 
+         \<open>text*[dfgdfg::B]
+           \<open> Lorem ipsum ...  @{thm refl} _ Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close>  \<close>
+          \<close>}\<close>
 
 (*<*)
 text\<open>Final Status:\<close>