# HG changeset patch
# User wenzelm
# Date 1637764423 -3600
# Node ID 4c8d9479f916b7b3e3549c24d1dbb92a4167b381
# Parent  f0e0fc82b0b94c5c4671e5f6d582d5507ee7c00a
more uniform treatment of optional_argument for Latex elements;
discontinued somewhat pointless element position in Isabelle/Scala: semantic add-ons are better provided in Isabelle/ML;
clarified signature of class Latex: overridable unknown_elem allows to extend the markup language;

diff -r f0e0fc82b0b9 -r 4c8d9479f916 src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML	Tue Nov 23 21:43:45 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Wed Nov 24 15:33:43 2021 +0100
@@ -8,7 +8,7 @@
 sig
   val document_reports: Input.source -> Position.report list
   val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text
-  val document_output: {markdown: bool, markup: Position.T -> Latex.text -> Latex.text} ->
+  val document_output: {markdown: bool, markup: Latex.text -> Latex.text} ->
     (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val output_token: Proof.context -> Token.T -> Latex.text
@@ -119,7 +119,7 @@
       let
         val ctxt = Toplevel.presentation_context st;
         val _ = Context_Position.reports ctxt (document_reports txt);
-      in txt |> output_document ctxt {markdown = markdown} |> markup (Position.thread_data ()) end;
+      in txt |> output_document ctxt {markdown = markdown} |> markup end;
   in
     Toplevel.present (fn st =>
       (case loc of
diff -r f0e0fc82b0b9 -r 4c8d9479f916 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Tue Nov 23 21:43:45 2021 +0100
+++ b/src/Pure/Thy/latex.scala	Wed Nov 24 15:33:43 2021 +0100
@@ -107,25 +107,24 @@
   {
     def latex_output(latex_text: Text): String = apply(latex_text)
 
-    def latex_macro0(name: String): Text =
-      XML.string("\\" + name)
+    def latex_macro0(name: String, optional_argument: String = ""): Text =
+      XML.string("\\" + name + optional_argument)
 
-    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 latex_macro(name: String, body: Text, optional_argument: String = ""): Text =
+      XML.enclose("\\" + name + optional_argument + "{", "}", body)
 
-    def latex_heading(kind: String, props: Properties.T, body: Text): Text =
-    {
-      val prefix =
-        "%\n\\" + options.string("document_heading_prefix") + kind +
-        Markup.Optional_Argument.get(props)
-      XML.enclose(prefix + "{", "%\n}\n", body)
-    }
+    def latex_environment(name: String, body: Text, optional_argument: String = ""): Text =
+      XML.enclose(
+        "%\n\\begin{" + name + "}" + optional_argument + "%\n",
+        "%\n\\end{" + name + "}", body)
 
-    def latex_body(kind: String, props: Properties.T, body: Text): Text =
-      latex_environment("isamarkup" + kind, body)
+    def latex_heading(kind: String, body: Text, optional_argument: String = ""): Text =
+      XML.enclose(
+        "%\n\\" + options.string("document_heading_prefix") + kind + optional_argument + "{",
+        "%\n}\n", body)
+
+    def latex_body(kind: String, body: Text, optional_argument: String = ""): Text =
+      latex_environment("isamarkup" + kind, body, optional_argument)
 
     def latex_delim(name: String, body: Text): Text =
     {
@@ -156,46 +155,50 @@
 
     /* standard output of text with per-line positions */
 
+    def unknown_elem(elem: XML.Elem, pos: Position.T): XML.Body =
+      error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) +
+        ":\n" + XML.string_of_tree(elem))
+
     def apply(latex_text: Text, file_pos: String = ""): String =
     {
       var line = 1
       val result = new mutable.ListBuffer[String]
       val positions = new mutable.ListBuffer[String] ++= init_position(file_pos)
 
-      def traverse(body: XML.Body): Unit =
+      val file_position = if (file_pos.isEmpty) Position.none else Position.File(file_pos)
+
+      def traverse(xml: XML.Body): Unit =
       {
-        body.foreach {
+        xml.foreach {
           case XML.Text(s) =>
             line += s.count(_ == '\n')
             result += s
-          case XML.Elem(Markup.Document_Latex(props), body) =>
-            for { l <- Position.Line.unapply(props) if positions.nonEmpty } {
-              val s = position(Value.Int(line), Value.Int(l))
-              if (positions.last != s) positions += s
+          case elem @ XML.Elem(markup, body) =>
+            val a = Markup.Optional_Argument.get(markup.properties)
+            traverse {
+              markup match {
+                case Markup.Document_Latex(props) =>
+                  for (l <- Position.Line.unapply(props) if positions.nonEmpty) {
+                    val s = position(Value.Int(line), Value.Int(l))
+                    if (positions.last != s) positions += s
+                  }
+                  body
+                case Markup.Latex_Output(_) => XML.string(latex_output(body))
+                case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a)
+                case Markup.Latex_Macro(name) => latex_macro(name, body, a)
+                case Markup.Latex_Environment(name) => latex_environment(name, body, a)
+                case Markup.Latex_Heading(kind) => latex_heading(kind, body, a)
+                case Markup.Latex_Body(kind) => latex_body(kind, body, a)
+                case Markup.Latex_Delim(name) => latex_delim(name, body)
+                case Markup.Latex_Tag(name) => latex_tag(name, body)
+                case Markup.Latex_Index_Entry(_) =>
+                  elem match {
+                    case Index_Entry(entry) => index_entry(entry)
+                    case _ => unknown_elem(elem, file_position)
+                  }
+                case _ => unknown_elem(elem, file_position)
+              }
             }
-            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 XML.Elem(markup @ Markup.Latex_Heading(kind), body) =>
-            traverse(latex_heading(kind, markup.properties, body))
-          case XML.Elem(markup @ Markup.Latex_Body(kind), body) =>
-            traverse(latex_body(kind, markup.properties, body))
-          case XML.Elem(Markup.Latex_Delim(name), body) =>
-            traverse(latex_delim(name, body))
-          case XML.Elem(Markup.Latex_Tag(name), body) =>
-            traverse(latex_tag(name, body))
-          case Index_Entry(entry) =>
-            traverse(index_entry(entry))
-          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 f0e0fc82b0b9 -r 4c8d9479f916 src/Pure/ex/Alternative_Headings.thy
--- a/src/Pure/ex/Alternative_Headings.thy	Tue Nov 23 21:43:45 2021 +0100
+++ b/src/Pure/ex/Alternative_Headings.thy	Wed Nov 24 15:33:43 2021 +0100
@@ -13,9 +13,8 @@
 ML \<open>
 local
 
-fun alternative_heading name pos body =
-  let val markup = Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argument "*";
-  in [XML.Elem (markup |> Position.markup pos, body)] end;
+fun alternative_heading name body =
+  [XML.Elem (Markup.latex_heading (unsuffix "*" name) |> Markup.optional_argument "*", body)];
 
 fun document_heading (name, pos) =
   Outer_Syntax.command (name, pos) (name ^ " heading")
diff -r f0e0fc82b0b9 -r 4c8d9479f916 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Tue Nov 23 21:43:45 2021 +0100
+++ b/src/Pure/pure_syn.ML	Wed Nov 24 15:33:43 2021 +0100
@@ -13,19 +13,17 @@
 structure Pure_Syn: PURE_SYN =
 struct
 
-fun markup_pos markup pos body = [XML.Elem (markup |> Position.markup pos, body)];
-
 fun document_heading (name, pos) =
   Outer_Syntax.command (name, pos) (name ^ " heading")
     (Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") >>
       Document_Output.document_output
-        {markdown = false, markup = markup_pos (Markup.latex_heading name)});
+        {markdown = false, markup = fn body => [XML.Elem (Markup.latex_heading name, body)]});
 
 fun document_body ((name, pos), description) =
   Outer_Syntax.command (name, pos) description
     (Parse.opt_target -- Parse.document_source >>
       Document_Output.document_output
-        {markdown = true, markup = markup_pos (Markup.latex_body name)});
+        {markdown = true, markup = fn body => [XML.Elem (Markup.latex_body name, body)]});
 
 val _ =
   List.app document_heading
@@ -45,7 +43,7 @@
   Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
     (Parse.opt_target -- Parse.document_source >>
       Document_Output.document_output
-        {markdown = true, markup = fn _ => Latex.enclose_text "%\n" "\n"});
+        {markdown = true, markup = Latex.enclose_text "%\n" "\n"});
 
 val _ =
   Outer_Syntax.command ("theory", \<^here>) "begin theory"