# HG changeset patch
# User wenzelm
# Date 1636993591 -3600
# Node ID 3ce6fb9db485f59422efaea3a0d02e361d3d79c8
# Parent  a5c23da73fca82b770214fa89b69796fdee2b94f
more symbolic latex_output via XML;

diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -150,6 +150,9 @@
   val document_tagN: string val document_tag: string -> T
   val document_latexN: string val document_latex: T
   val latex_outputN: string val latex_output: T
+  val latex_macro0N: string val latex_macro0: string -> T
+  val latex_macroN: string val latex_macro: string -> T
+  val latex_environmentN: string val latex_environment: string -> T
   val latex_index_itemN: string val latex_index_item: T
   val latex_index_entryN: string val latex_index_entry: string -> T
   val markdown_paragraphN: string val markdown_paragraph: T
@@ -578,6 +581,9 @@
 val (document_latexN, document_latex) = markup_elem "document_latex";
 
 val (latex_outputN, latex_output) = markup_elem "latex_output";
+val (latex_macro0N, latex_macro0) = markup_string "latex_macro0" nameN;
+val (latex_macroN, latex_macro) = markup_string "latex_macro" nameN;
+val (latex_environmentN, latex_environment) = markup_string "latex_environment" nameN;
 val (latex_index_itemN, latex_index_item) = markup_elem "latex_index_item";
 val (latex_index_entryN, latex_index_entry) = markup_string "latex_index_entry" kindN;
 
diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Nov 15 17:26:31 2021 +0100
@@ -372,6 +372,9 @@
   val Document_Latex = new Markup_Elem("document_latex")
 
   val Latex_Output = new Markup_Elem("latex_output")
+  val Latex_Macro0 = new Markup_String("latex_macro0", NAME)
+  val Latex_Macro = new Markup_String("latex_macro", NAME)
+  val Latex_Environment = new Markup_String("latex_environment", NAME)
   val Latex_Index_Item = new Markup_Elem("latex_index_item")
   val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND)
 
diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/PIDE/resources.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -418,7 +418,7 @@
   Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
    (check ctxt NONE source;
     Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source))
-    |> XML.enclose "\\isatt{" "}"));
+    |> Latex.macro "isatt"));
 
 fun ML_antiq check =
   Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/System/scala_compiler.ML
--- a/src/Pure/System/scala_compiler.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/System/scala_compiler.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -58,8 +58,7 @@
 val args = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _";
 
 fun scala_name name =
-  Latex.string (Latex.output_ascii_breakable "." name)
-  |> XML.enclose "\\isatt{" "}";
+  Latex.macro "isatt" (Latex.string (Latex.output_ascii_breakable "." name));
 
 in
 
diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -131,17 +131,17 @@
 
 local
 
-fun nested_antiquotation name s1 s2 =
+fun nested_antiquotation name macro =
   Document_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
     (fn ctxt => fn txt =>
       (Context_Position.reports ctxt (Document_Output.document_reports txt);
-        XML.enclose s1 s2 (Document_Output.output_document ctxt {markdown = false} txt)));
+        Latex.macro macro (Document_Output.output_document ctxt {markdown = false} txt)));
 
 val _ =
   Theory.setup
-   (nested_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #>
-    nested_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #>
-    nested_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}");
+   (nested_antiquotation \<^binding>\<open>footnote\<close> "footnote" #>
+    nested_antiquotation \<^binding>\<open>emph\<close> "emph" #>
+    nested_antiquotation \<^binding>\<open>bold\<close> "textbf");
 
 in end;
 
@@ -423,24 +423,24 @@
         val _ =
           Context_Position.reports ctxt
             [(pos, Markup.language_url delimited), (pos, Markup.url url)];
-      in XML.enclose "\\url{" "}" (Latex.string (escape_url url)) end));
+      in Latex.macro "url" (Latex.string (escape_url url)) end));
 
 
 (* formal entities *)
 
 local
 
-fun entity_antiquotation name check bg en =
+fun entity_antiquotation name check macro =
   Document_Output.antiquotation_raw name (Scan.lift Args.name_position)
     (fn ctxt => fn (name, pos) =>
       let val _ = check ctxt (name, pos)
-      in XML.enclose bg en (Latex.string (Output.output name)) end);
+      in Latex.macro macro (Latex.string (Output.output name)) end);
 
 val _ =
   Theory.setup
-   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "\\isacommand{" "}" #>
-    entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "\\isa{" "}" #>
-    entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "\\isa{" "}");
+   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command "isacommand" #>
+    entity_antiquotation \<^binding>\<open>method\<close> Method.check_name "isa" #>
+    entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name "isa");
 
 in end;
 
diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -484,13 +484,13 @@
 
 fun isabelle ctxt body =
   if Config.get ctxt Document_Antiquotation.thy_output_display
-  then Latex.environment_text "isabelle" body
-  else XML.enclose "\\isa{" "}" body;
+  then Latex.environment "isabelle" body
+  else Latex.macro "isa" body;
 
 fun isabelle_typewriter ctxt body =
   if Config.get ctxt Document_Antiquotation.thy_output_display
-  then Latex.environment_text "isabellett" body
-  else XML.enclose "\\isatt{" "}" body;
+  then Latex.environment "isabellett" body
+  else Latex.macro "isatt" body;
 
 fun typewriter ctxt s =
   isabelle_typewriter ctxt (Latex.string (Latex.output_ascii s));
diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/Thy/latex.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -11,6 +11,9 @@
   val string: string -> text
   val block: text -> XML.tree
   val output: text -> text
+  val macro0: string -> text
+  val macro: string -> text -> text
+  val environment: string -> text -> text
   val enclose_text: string -> string -> text -> text
   val output_name: string -> string
   val output_ascii: string -> string
@@ -54,6 +57,10 @@
 
 fun output body = [XML.Elem (Markup.latex_output, body)];
 
+fun macro0 name = [XML.Elem (Markup.latex_macro0 name, [])];
+fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
+fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
+
 fun enclose_text bg en body = string bg @ body @ string en;
 
 
diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Nov 15 17:26:31 2021 +0100
@@ -77,9 +77,15 @@
   {
     def latex_output(latex_text: Text): String = apply(latex_text)
 
+    def latex_macro0(name: String): Text =
+      XML.string("\\" + name)
+
     def latex_macro(name: String, body: Text): Text =
       XML.enclose("\\" + name + "{", "}", body)
 
+    def latex_environment(name: String, body: Text): Text =
+      XML.enclose("%\n\\begin{" + name + "}%\n", "%\n\\end{" + name + "}", body)
+
     def index_item(item: Index_Item.Value): String =
     {
       val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@"
@@ -117,9 +123,18 @@
             traverse(body)
           case XML.Elem(Markup.Latex_Output(_), body) =>
             traverse(XML.string(latex_output(body)))
+          case XML.Elem(Markup.Latex_Macro0(name), Nil) =>
+            traverse(latex_macro0(name))
+          case XML.Elem(Markup.Latex_Macro(name), body) =>
+            traverse(latex_macro(name, body))
+          case XML.Elem(Markup.Latex_Environment(name), body) =>
+            traverse(latex_environment(name, body))
           case Index_Entry(entry) =>
             traverse(index_entry(entry))
-          case _: XML.Elem =>
+          case t: XML.Tree =>
+            error("Bad latex markup" +
+              (if (file_pos.isEmpty) "" else Position.here(Position.File(file_pos))) + ":\n" +
+              XML.string_of_tree(t))
         }
       }
       traverse(latex_text)
diff -r a5c23da73fca -r 3ce6fb9db485 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Mon Nov 15 11:38:14 2021 +0100
+++ b/src/Pure/Tools/rail.ML	Mon Nov 15 17:26:31 2021 +0100
@@ -343,10 +343,9 @@
       Antiquote.Antiq #>
       Document_Antiquotation.evaluate Latex.symbols ctxt;
     fun output_text b s =
-      Output.output s
-      |> b ? enclose "\\isakeyword{" "}"
-      |> enclose "\\isa{" "}"
-      |> Latex.string;
+      Latex.string (Output.output s)
+      |> b ? Latex.macro "isakeyword"
+      |> Latex.macro "isa";
 
     fun output_cat c (Cat (_, rails)) = outputs c rails
     and outputs c [rail] = output c rail