added define_macro2

src/DOF/Isa_COL.thy

@@ -228,7 +228,21 @@ end
 
 section\<open>Shortcuts, Macros, Environments\<close>
 text\<open>This is actually \<^emph>\<open>not\<close> a real ISADOF feature, rather a slightly more abstract layer over
-     somewhat buried standard features of the Isabelle document generator ... \<close>
+somewhat buried standard features of the Isabelle document generator ... (Thanks to Makarius).
+Conceptually, they are \<^emph>\<open>sub-text-elements\<close>. \<close>
+
+text\<open>This module provides mechanisms to define front-end checked:
+\<^enum> \<^emph>\<open>shortcuts\<close>, i.e. machine-checked abbreviations without arguments 
+  that were mapped to user-defined LaTeX code (Example: \<^verbatim>\<open>\ie\<close>)
+\<^enum> macro's with one argument that were mapped to user-defined code. Example: \<^verbatim>\<open>\myurl{bla}\<close>.
+  The argument can be potentially checked and reports can be sent to PIDE;
+  if no such checking is desired, this can be expressed by setting the
+  \<^theory_text>\<open>reportNtest\<close>-parameter to \<^theory_text>\<open>K(K())\<close>.
+\<^enum> macro's with two arguments, potentially independently checked. See above. 
+  Example: \<^verbatim>\<open>\myurl[ding]{dong}\<close>.
+
+Note that we deliberately refrained from a code-template definition mechanism for simplicity.
+\<close>
 
 ML\<open>
 structure DOF_lib =
@@ -237,12 +251,33 @@ fun define_shortcut name latexshcut =
        Thy_Output.antiquotation_raw name (Scan.succeed ())
           (fn _ => fn () => Latex.string latexshcut) 
 
-(* This is just a copy of Isabelle2020 function "control_antiquotation" from 
-   document_antiquotations.ML, where it is unfortunately not exported. (Thanks Makarius!)
- *)
-fun define_macro name s1 s2 =
+(* This is a generalization of the Isabelle2020 function "control_antiquotation" from 
+   document_antiquotations.ML. (Thanks Makarius!) *)
+fun define_macro name s1 s2 reportNtest =
       Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
-         (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false});
+         (fn ctxt => 
+             fn src => let val () = reportNtest ctxt src 
+                       in  src |>   Latex.enclose_block s1 s2 
+                                  o Thy_Output.output_document ctxt {markdown = false}
+                       end);
+
+local (* hide away really strange local construction *)
+fun enclose_body2 front body1 middle body2 post =
+  (if front = "" then [] else [Latex.string front]) @ body1 @
+  (if middle = "" then [] else [Latex.string middle]) @ body2 @
+  (if post = "" then [] else [Latex.string post]);
+in
+fun define_macro2 name front middle post reportNtest1 reportNtest2 =
+      Thy_Output.antiquotation_raw_embedded name (Scan.lift (   Args.cartouche_input 
+                                                             -- Args.cartouche_input))
+         (fn ctxt => 
+             fn (src1,src2) => let val () = reportNtest1 ctxt src1 
+                                   val () = reportNtest2 ctxt src2 
+                                   val T1 = Thy_Output.output_document ctxt {markdown = false} src1
+                                   val T2 = Thy_Output.output_document ctxt {markdown = false} src2
+                               in  Latex.block(enclose_body2 front T1 middle T2 post)
+                               end);
+end
 
 end
 \<close>

src/tests/OutOfOrderPresntn.thy

@@ -168,7 +168,7 @@ print_doc_classes
 section\<open>Experiments on Inline-Textelements\<close>
 text\<open>Std Abbreviations. Inspired by the block *\<open>control spacing\<close> 
      in @{file \<open>$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\<close>}.
-     We could mechanize the table-construction and even attach the LaTeX 
+     We mechanize the table-construction and even attach the LaTeX 
      quirks to be dumped into the prelude.  \<close>
 
 ML\<open>
@@ -190,10 +190,73 @@ setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<
    using the alternative \<^binding> notation (see above).*)
 
 
-setup\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}"\<close>
+setup\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\<close>
 
 textN\<open> \<^blong>\<open>asd\<close> outer  \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
 
+ML\<open>
 
+fun report_text ctxt text =
+  let val pos = Input.pos_of text in
+    Context_Position.reports ctxt
+      [(pos, Markup.language_text (Input.is_delimited text)),
+       (pos, Markup.raw_text)]
+  end;
+
+fun prepare_text ctxt =
+  Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
+
+fun text_antiquotation name =
+  Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
+    (fn ctxt => fn text =>
+      let
+        val _ = report_text ctxt text;
+      in
+        prepare_text ctxt text
+        |> Thy_Output.output_source ctxt
+        |> Thy_Output.isabelle ctxt
+      end);
+
+fun block_geraffel ctxt block_env body =
+  if Config.get ctxt Document_Antiquotation.thy_output_display
+  then Latex.environment_block block_env [body]
+  else body;
+
+
+
+fun theory_text_antiquotation name =
+  Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
+    (fn ctxt => fn text =>
+      let
+        val keywords = Thy_Header.get_keywords' ctxt;
+
+        val _ = report_text ctxt text;
+        val _ =
+          Input.source_explode text
+          |> Token.tokenize keywords {strict = true}
+          |> maps (Token.reports keywords)
+          |> Context_Position.reports_text ctxt;
+      in
+        prepare_text ctxt text
+        |> Token.explode0 keywords
+        |> maps (Thy_Output.output_token ctxt)
+        |> Thy_Output.isabelle ctxt
+        |> block_geraffel ctxt "isarbox"
+      end);
+
+
+  Theory.setup
+   (text_antiquotation        \<^binding>\<open>boxed_text\<close> #>
+    text_antiquotation        \<^binding>\<open>boxed_cartouche\<close> #>
+    theory_text_antiquotation \<^binding>\<open>boxed_theory_text\<close>); (* is overriding possible ?*)
+
+
+
+\<close>
+
+textN\<open> 
+      @{boxed_cartouche  [display] \<open>definition dfg = \<lambda>x. x\<close>}
+      @{boxed_theory_text [display] \<open>doc_class dfg = ...\<close>}  \<close>
+               
 end
 (*>*)