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;
--- 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
--- 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)
--- 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")
--- 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"