shifted new env up into COL. Declared in the Frontmatter.

examples/technical_report/Isabelle_DOF-Manual/00_Frontmatter.thy

@@ -38,6 +38,32 @@ text\<open>Note that these setups assume that the associated \<^LaTeX> macros ar
 setup\<open>    DOF_lib.define_macro \<^binding>\<open>index\<close>   "\\index{" "}" (K(K())) (*no checking, no reporting*)
        #> DOF_lib.define_macro \<^binding>\<open>bindex\<close>  "\\bindex{" "}"(K(K()))\<close> 
 
+
+ML\<open>
+
+fun boxed_text_antiquotation name (* redefined in these more abstract terms *) =
+    DOF_lib.gen_text_antiquotation name DOF_lib.report_text 
+                           (fn ctxt => DOF_lib.string_2_text_antiquotation ctxt
+                                       #> DOF_lib.enclose_env ctxt "isarbox")
+
+
+fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) =
+    DOF_lib.gen_text_antiquotation name DOF_lib.report_theory_text 
+                           (fn ctxt => DOF_lib.string_2_theory_text_antiquotation ctxt 
+                                        #> DOF_lib.enclose_env ctxt "isarbox")
+
+\<close>
+
+setup\<open>(* std_text_antiquotation        \<^binding>\<open>my_text\<close> #> *)
+      boxed_text_antiquotation         \<^binding>\<open>boxed_text\<close> #>
+      (* std_text_antiquotation        \<^binding>\<open>my_cartouche\<close> #> *)
+      boxed_text_antiquotation         \<^binding>\<open>boxed_cartouche\<close> #>
+      (* std_theory_text_antiquotation \<^binding>\<open>my_theory_text\<close>#> *)
+      boxed_theory_text_antiquotation  \<^binding>\<open>boxed_theory_text\<close>\<close>
+
+
+
+
 open_monitor*[this::report] 
 
 (*>*)

examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex

@@ -117,3 +117,7 @@ France, and therefore granted with public funds of the Program ``Investissements
 
 \AtBeginDocument{\isabellestyle{literal}\newcommand{\lstnumberautorefname}{Line}}
 \renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}}
+
+\newenvironment{isarbox}
+{AAA - bu isarbox}
+{ZZZ - bu isarbox}

src/DOF/Isa_COL.thy

@@ -283,6 +283,100 @@ fun define_macro2 name front middle post reportNtest1 reportNtest2 =
                                end);
 end
 
+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 report_theory_text ctxt 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 () end
+
+fun prepare_text ctxt =
+  Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
+(* This also produces indent-expansion and changes space to "\_" and the introduction of "\newline",
+   I believe. Otherwise its in Thy_Output.output_source, the compiler from string to LaTeX.text. *)
+
+fun string_2_text_antiquotation ctxt text = 
+        prepare_text ctxt text
+        |> Thy_Output.output_source ctxt
+        |> Thy_Output.isabelle ctxt
+
+fun string_2_theory_text_antiquotation ctxt text =
+      let
+        val keywords = Thy_Header.get_keywords' ctxt;
+      in
+        prepare_text ctxt text
+        |> Token.explode0 keywords
+        |> maps (Thy_Output.output_token ctxt)
+        |> Thy_Output.isabelle ctxt
+      end
+
+fun gen_text_antiquotation name reportNcheck compile =
+  Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
+    (fn ctxt => fn text:Input.source =>
+      let
+        val _ = reportNcheck ctxt text;
+      in
+        compile ctxt text    
+      end);
+
+fun std_text_antiquotation name (* redefined in these more abstract terms *) =
+    gen_text_antiquotation name report_text string_2_text_antiquotation
+
+(* should be the same as (2020):
+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 std_theory_text_antiquotation name (* redefined in these more abstract terms *) =
+    gen_text_antiquotation name report_theory_text string_2_theory_text_antiquotation
+
+(* should be the same as (2020):
+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
+        |> enclose_env ctxt "isarbox"
+      end);
+*)
+
+
+
+fun enclose_env ctxt block_env body =
+  if Config.get ctxt Document_Antiquotation.thy_output_display
+  then Latex.environment_block block_env [body]
+  else body;
+
 end
 \<close>
 

src/tests/OutOfOrderPresntn.thy

@@ -245,7 +245,7 @@ fun gen_text_antiquotation name reportNcheck compile =
 fun std_text_antiquotation name (* redefined in these more abstract terms *) =
     gen_text_antiquotation name report_text string_2_text_antiquotation
 
-(* should be the same as:
+(* should be the same as (2020):
 fun text_antiquotation name =
   Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
@@ -261,7 +261,7 @@ fun text_antiquotation name =
 fun std_theory_text_antiquotation name (* redefined in these more abstract terms *) =
     gen_text_antiquotation name report_theory_text string_2_theory_text_antiquotation
 
-(* should be the same as:
+(* should be the same as (2020):
 fun theory_text_antiquotation name =
   Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
     (fn ctxt => fn text =>