# HG changeset patch # User wenzelm # Date 1637437361 -3600 # Node ID 0e4d8aa61ad73cb6e924827f28a0d6723419d46c # Parent 9bea6244c35acd27a3d4f02fe4786358f09191f5 more symbolic latex_output via XML (using YXML within text); diff -r 9bea6244c35a -r 0e4d8aa61ad7 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Nov 20 19:39:22 2021 +0100 +++ b/src/Pure/PIDE/markup.ML Sat Nov 20 20:42:41 2021 +0100 @@ -157,6 +157,8 @@ val latex_bodyN: string val latex_body: string -> T val latex_index_itemN: string val latex_index_item: T val latex_index_entryN: string val latex_index_entry: string -> T + val latex_delimN: string val latex_delim: string -> T + val latex_tagN: string val latex_tag: string -> T val markdown_paragraphN: string val markdown_paragraph: T val markdown_itemN: string val markdown_item: T val markdown_bulletN: string val markdown_bullet: int -> T @@ -590,6 +592,8 @@ val (latex_bodyN, latex_body) = markup_string "latex_body" kindN; 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; +val (latex_delimN, latex_delim) = markup_string "latex_delim" nameN; +val (latex_tagN, latex_tag) = markup_string "latex_tag" nameN; (* Markdown document structure *) diff -r 9bea6244c35a -r 0e4d8aa61ad7 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Nov 20 19:39:22 2021 +0100 +++ b/src/Pure/PIDE/markup.scala Sat Nov 20 20:42:41 2021 +0100 @@ -377,6 +377,9 @@ val Latex_Environment = new Markup_String("latex_environment", NAME) val Latex_Heading = new Markup_String("latex_heading", KIND) val Latex_Body = new Markup_String("latex_body", KIND) + val Latex_Delim = new Markup_String("latex_delim", NAME) + val Latex_Tag = new Markup_String("latex_tag", NAME) + val Latex_Index_Item = new Markup_Elem("latex_index_item") val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND) diff -r 9bea6244c35a -r 0e4d8aa61ad7 src/Pure/Thy/document_output.ML --- a/src/Pure/Thy/document_output.ML Sat Nov 20 19:39:22 2021 +0100 +++ b/src/Pure/Thy/document_output.ML Sat Nov 20 20:42:41 2021 +0100 @@ -241,10 +241,15 @@ if x = y then I else (case which (x, y) of NONE => I | SOME txt => fold cons (Latex.string (f txt))); -val begin_tag = edge #2 Latex.begin_tag; -val end_tag = edge #1 Latex.end_tag; -fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e; -fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e; +val markup_tag = YXML.output_markup o Markup.latex_tag; +val markup_delim = YXML.output_markup o Markup.latex_delim; +val bg_delim = #1 o markup_delim; +val en_delim = #2 o markup_delim; + +val begin_tag = edge #2 (#1 o markup_tag); +val end_tag = edge #1 (#2 o markup_tag); +fun open_delim delim e = edge #2 bg_delim e #> delim #> edge #2 en_delim e; +fun close_delim delim e = edge #1 bg_delim e #> delim #> edge #1 en_delim e; fun document_tag cmd_pos state state' tagging_stack = let diff -r 9bea6244c35a -r 0e4d8aa61ad7 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Sat Nov 20 19:39:22 2021 +0100 +++ b/src/Pure/Thy/latex.ML Sat Nov 20 20:42:41 2021 +0100 @@ -22,10 +22,6 @@ val output_syms: string -> string val symbols: Symbol_Pos.T list -> text val symbols_output: Symbol_Pos.T list -> text - val begin_delim: string -> string - val end_delim: string -> string - val begin_tag: string -> string - val end_tag: string -> string val environment_text: string -> text -> text val isabelle_body: string -> text -> text val theory_entry: string -> string @@ -196,14 +192,6 @@ text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms)); -(* tags *) - -val begin_delim = enclose_name "%\n\\isadelim" "\n"; -val end_delim = enclose_name "%\n\\endisadelim" "\n"; -val begin_tag = enclose_name "%\n\\isatag" "\n"; -fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose_name "{\\isafold" "}%\n" tg; - - (* theory presentation *) fun environment_text name = diff -r 9bea6244c35a -r 0e4d8aa61ad7 src/Pure/Thy/latex.scala --- a/src/Pure/Thy/latex.scala Sat Nov 20 19:39:22 2021 +0100 +++ b/src/Pure/Thy/latex.scala Sat Nov 20 20:42:41 2021 +0100 @@ -16,6 +16,36 @@ object Latex { + /* output name for LaTeX macros */ + + private val output_name_map: Map[Char, String] = + Map('_' -> "UNDERSCORE", + '\'' -> "PRIME", + '0' -> "ZERO", + '1' -> "ONE", + '2' -> "TWO", + '3' -> "THREE", + '4' -> "FOUR", + '5' -> "FIVE", + '6' -> "SIX", + '7' -> "SEVEN", + '8' -> "EIGHT", + '9' -> "NINE") + + def output_name(name: String): String = + if (name.exists(output_name_map.keySet)) { + val res = new StringBuilder + for (c <- name) { + output_name_map.get(c) match { + case None => res += c + case Some(s) => res ++= s + } + } + res.toString + } + else name + + /* index entries */ def index_escape(str: String): String = @@ -92,6 +122,18 @@ def latex_body(kind: String, body: Text): Text = latex_environment("isamarkup" + kind, body) + def latex_delim(name: String, body: Text): Text = + { + val s = output_name(name) + XML.enclose("%\n\\isadelim" + s + "\n", "%\n\\endisadelim" + s + "\n", body) + } + + def latex_tag(name: String, body: Text): Text = + { + val s = output_name(name) + XML.enclose("%\n\\isatag" + s + "\n", "%\n\\endisatag" + s + "\n{\\isafold" + s + "}%\n", body) + } + def index_item(item: Index_Item.Value): String = { val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@" @@ -139,6 +181,10 @@ traverse(latex_heading(kind, body)) case XML.Elem(Markup.Latex_Body(kind), body) => traverse(latex_body(kind, 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 =>