--- a/src/Doc/antiquote_setup.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Doc/antiquote_setup.ML Tue May 25 22:28:39 2021 +0200
@@ -45,7 +45,7 @@
(Document_Antiquotation.delimit ctxt (Document_Output.pretty_thm ctxt thm))) ^
enclose "\\rulename{" "}" (Output.output name))
#> space_implode "\\par\\smallskip%\n"
- #> Latex.string #> single
+ #> Latex.string
#> Document_Output.isabelle ctxt));
--- a/src/Pure/PIDE/markup.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/PIDE/markup.ML Tue May 25 22:28:39 2021 +0200
@@ -138,6 +138,7 @@
val text_foldN: string val text_fold: T
val document_markerN: string val document_marker: T
val document_tagN: string val document_tag: string -> T
+ val document_latexN: string val document_latex: 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
@@ -530,6 +531,8 @@
val (document_markerN, document_marker) = markup_elem "document_marker";
val (document_tagN, document_tag) = markup_string "document_tag" nameN;
+val (document_latexN, document_latex) = markup_elem "document_latex";
+
(* Markdown document structure *)
--- a/src/Pure/PIDE/markup.scala Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/PIDE/markup.scala Tue May 25 22:28:39 2021 +0200
@@ -356,6 +356,8 @@
}
}
+ val DOCUMENT_LATEX = "document_latex"
+
/* Markdown document structure */
--- a/src/Pure/PIDE/resources.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/PIDE/resources.ML Tue May 25 22:28:39 2021 +0200
@@ -412,10 +412,9 @@
fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) =
Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
- let
- val _ = check ctxt NONE source;
- val latex = Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source));
- in Latex.enclose_block "\\isatt{" "}" [latex] end);
+ (check ctxt NONE source;
+ Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source))
+ |> Latex.enclose_text "\\isatt{" "}"));
fun ML_antiq check =
Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) =>
--- a/src/Pure/System/scala_compiler.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/System/scala_compiler.ML Tue May 25 22:28:39 2021 +0200
@@ -58,8 +58,8 @@
val args = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _";
fun scala_name name =
- let val latex = Latex.string (Latex.output_ascii_breakable "." name)
- in Latex.enclose_block "\\isatt{" "}" [latex] end;
+ Latex.string (Latex.output_ascii_breakable "." name)
+ |> Latex.enclose_text "\\isatt{" "}";
in
--- a/src/Pure/Thy/document_antiquotation.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML Tue May 25 22:28:39 2021 +0200
@@ -33,8 +33,8 @@
val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
val boolean: string -> bool
val integer: string -> int
- val evaluate: (Symbol_Pos.T list -> Latex.text list) -> Proof.context ->
- Antiquote.text_antiquote -> Latex.text list
+ val evaluate: (Symbol_Pos.T list -> Latex.text) -> Proof.context ->
+ Antiquote.text_antiquote -> Latex.text
val approx_content: Proof.context -> string -> string
end;
@@ -184,7 +184,7 @@
val print_ctxt = Context_Position.set_visible false preview_ctxt;
val print_modes =
space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN, Pretty.regularN];
- in [Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) ()] end;
+ in Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) () end;
in
--- a/src/Pure/Thy/document_antiquotations.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Tue May 25 22:28:39 2021 +0200
@@ -131,7 +131,7 @@
Document_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
(fn ctxt => fn txt =>
(Context_Position.reports ctxt (Document_Output.document_reports txt);
- Latex.enclose_block s1 s2 (Document_Output.output_document ctxt {markdown = false} txt)));
+ Latex.enclose_text s1 s2 (Document_Output.output_document ctxt {markdown = false} txt)));
val _ =
Theory.setup
@@ -149,7 +149,7 @@
val index_like = Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "is" |-- Args.name --| Parse.$$$ ")");
val index_args = Parse.enum1 "!" (Args.embedded_input -- Scan.option index_like);
-fun output_text ctxt = Latex.block o Document_Output.output_document ctxt {markdown = false};
+fun output_text ctxt = Document_Output.output_document ctxt {markdown = false};
fun index binding def =
Document_Output.antiquotation_raw binding (Scan.lift index_args)
@@ -370,16 +370,17 @@
val main_text =
Document_Output.verbatim ctxt
((if kind = "" orelse not show_kind then "" else kind ^ " ") ^ txt0 ^ txt);
-
val index_text =
- index |> Option.map (fn def =>
- let
- val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt;
- val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")";
- val txt' = Latex.block [Document_Output.verbatim ctxt' idx, Latex.string kind'];
- val like = Document_Antiquotation.approx_content ctxt' idx;
- in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
- in Latex.block (the_list index_text @ [main_text]) end);
+ (case index of
+ NONE => []
+ | SOME def =>
+ let
+ val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt;
+ val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")";
+ val txt' = Document_Output.verbatim ctxt' idx @ Latex.string kind';
+ val like = Document_Antiquotation.approx_content ctxt' idx;
+ in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
+ in index_text @ main_text end);
fun antiquotation_ml0 test kind =
antiquotation_ml parse_ml0 test kind false;
@@ -422,7 +423,7 @@
val _ =
Context_Position.reports ctxt
[(pos, Markup.language_url delimited), (pos, Markup.url url)];
- in Latex.enclose_block "\\url{" "}" [Latex.string (escape_url url)] end));
+ in Latex.enclose_text "\\url{" "}" (Latex.string (escape_url url)) end));
(* formal entities *)
@@ -433,7 +434,7 @@
Document_Output.antiquotation_raw name (Scan.lift Args.name_position)
(fn ctxt => fn (name, pos) =>
let val _ = check ctxt (name, pos)
- in Latex.enclose_block bg en [Latex.string (Output.output name)] end);
+ in Latex.enclose_text bg en (Latex.string (Output.output name)) end);
val _ =
Theory.setup
--- a/src/Pure/Thy/document_build.scala Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/Thy/document_build.scala Tue May 25 22:28:39 2021 +0200
@@ -218,7 +218,8 @@
for (name <- document_theories)
yield {
val path = Path.basic(tex_name(name))
- val content = get_export(name.theory, document_tex_name(name)).uncompressed
+ val xml = YXML.parse_body(get_export(name.theory, document_tex_name(name)).text)
+ val content = Latex.output(xml, file_pos = name.path.implode_symbolic)
Content(path, content)
}
--- a/src/Pure/Thy/document_output.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/Thy/document_output.ML Tue May 25 22:28:39 2021 +0200
@@ -7,20 +7,18 @@
signature DOCUMENT_OUTPUT =
sig
val document_reports: Input.source -> Position.report list
- val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
+ val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text
val check_comments: Proof.context -> Symbol_Pos.T list -> unit
- val output_token: Proof.context -> Token.T -> Latex.text list
- val output_source: Proof.context -> string -> Latex.text list
+ val output_token: Proof.context -> Token.T -> Latex.text
+ val output_source: Proof.context -> string -> Latex.text
type segment =
{span: Command_Span.span, command: Toplevel.transition,
prev_state: Toplevel.state, state: Toplevel.state}
- val present_thy: Options.T -> theory -> segment list -> Latex.text list
+ val present_thy: Options.T -> theory -> segment list -> Latex.text
val pretty_term: Proof.context -> term -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
- val lines: Latex.text list -> Latex.text list
- val items: Latex.text list -> Latex.text list
- val isabelle: Proof.context -> Latex.text list -> Latex.text
- val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text
+ val isabelle: Proof.context -> Latex.text -> Latex.text
+ val isabelle_typewriter: Proof.context -> Latex.text -> Latex.text
val typewriter: Proof.context -> string -> Latex.text
val verbatim: Proof.context -> string -> Latex.text
val source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text
@@ -58,25 +56,23 @@
(pos, Markup.plain_text)]
end;
-val output_symbols = single o Latex.symbols_output;
-
fun output_comment ctxt (kind, syms) =
(case kind of
Comment.Comment =>
Input.cartouche_content syms
|> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false)
{markdown = false}
- |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
+ |> Latex.enclose_text "%\n\\isamarkupcmt{" "%\n}"
| Comment.Cancel =>
Symbol_Pos.cartouche_content syms
- |> output_symbols
- |> Latex.enclose_body "%\n\\isamarkupcancel{" "}"
- | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)]
+ |> Latex.symbols_output
+ |> Latex.enclose_text "%\n\\isamarkupcancel{" "}"
+ | Comment.Latex => Latex.symbols (Symbol_Pos.cartouche_content syms)
| Comment.Marker => [])
and output_comment_document ctxt (comment, syms) =
(case comment of
SOME kind => output_comment ctxt (kind, syms)
- | NONE => [Latex.symbols syms])
+ | NONE => Latex.symbols syms)
and output_document_text ctxt syms =
Comment.read_body syms |> maps (output_comment_document ctxt)
and output_document ctxt {markdown} source =
@@ -88,14 +84,15 @@
maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt);
fun output_line line =
- (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
+ (if Markdown.line_is_item line then Latex.string "\\item " else []) @
output_antiquotes (Markdown.line_content line);
fun output_block (Markdown.Par lines) =
- Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines))
+ separate (XML.Text "\n") (map (Latex.block o output_line) lines)
| output_block (Markdown.List {kind, body, ...}) =
- Latex.environment_block (Markdown.print_kind kind) (output_blocks body)
- and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks);
+ Latex.environment_text (Markdown.print_kind kind) (output_blocks body)
+ and output_blocks blocks =
+ separate (XML.Text "\n\n") (map (Latex.block o output_block) blocks);
in
if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then []
else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
@@ -120,16 +117,16 @@
local
val output_symbols_antiq =
- (fn Antiquote.Text syms => output_symbols syms
+ (fn Antiquote.Text syms => Latex.symbols_output syms
| Antiquote.Control {name = (name, _), body, ...} =>
- Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) ::
- output_symbols body
+ Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) @
+ Latex.symbols_output body
| Antiquote.Antiq {body, ...} =>
- Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body));
+ Latex.enclose_text "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (Latex.symbols_output body));
fun output_comment_symbols ctxt {antiq} (comment, syms) =
(case (comment, antiq) of
- (NONE, false) => output_symbols syms
+ (NONE, false) => Latex.symbols_output syms
| (NONE, true) =>
Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms
|> maps output_symbols_antiq
@@ -138,7 +135,7 @@
fun output_body ctxt antiq bg en syms =
Comment.read_body syms
|> maps (output_comment_symbols ctxt {antiq = antiq})
- |> Latex.enclose_body bg en;
+ |> Latex.enclose_text bg en;
in
@@ -203,12 +200,12 @@
Ignore => []
| Token tok => output_token ctxt tok
| Heading (cmd, source) =>
- Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
+ Latex.enclose_text ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
(output_document ctxt {markdown = false} source)
| Body (cmd, source) =>
- [Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)]
+ Latex.environment_text ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)
| Raw source =>
- Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
+ Latex.string "%\n" @ output_document ctxt {markdown = true} source @ Latex.string "\n");
(* command spans *)
@@ -242,7 +239,7 @@
fun edge which f (x: string option, y) =
if x = y then I
- else (case which (x, y) of NONE => I | SOME txt => cons (Latex.string (f txt)));
+ 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;
@@ -305,7 +302,7 @@
val ctxt' = Toplevel.presentation_context state';
val present = fold (fn (tok, (flag, 0)) =>
fold cons (present_token ctxt' tok)
- #> cons (Latex.string flag)
+ #> fold cons (Latex.string flag)
| _ => I);
val Span ((cmd_name, cmd_pos), srcs, span_newline) = span;
@@ -484,26 +481,23 @@
(* default output *)
-val lines = separate (Latex.string "\\isanewline%\n");
-val items = separate (Latex.string "\\isasep\\isanewline%\n");
-
fun isabelle ctxt body =
if Config.get ctxt Document_Antiquotation.thy_output_display
- then Latex.environment_block "isabelle" body
- else Latex.block (Latex.enclose_body "\\isa{" "}" body);
+ then Latex.environment_text "isabelle" body
+ else Latex.enclose_text "\\isa{" "}" body;
fun isabelle_typewriter ctxt body =
if Config.get ctxt Document_Antiquotation.thy_output_display
- then Latex.environment_block "isabellett" body
- else Latex.block (Latex.enclose_body "\\isatt{" "}" body);
+ then Latex.environment_text "isabellett" body
+ else Latex.enclose_text "\\isatt{" "}" body;
fun typewriter ctxt s =
- isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)];
+ isabelle_typewriter ctxt (Latex.string (Latex.output_ascii s));
fun verbatim ctxt =
if Config.get ctxt Document_Antiquotation.thy_output_display
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
- else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
+ else split_lines #> map (typewriter ctxt #> Latex.block) #> separate (XML.Text "\\isanewline%\n");
fun token_source ctxt {embedded} tok =
if Token.is_kind Token.Cartouche tok andalso embedded andalso
@@ -523,13 +517,14 @@
#> isabelle ctxt;
fun pretty ctxt =
- Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt;
+ Document_Antiquotation.output ctxt #> Latex.string #> isabelle ctxt;
fun pretty_source ctxt embedded src prt =
if is_source ctxt then source ctxt embedded src else pretty ctxt prt;
fun pretty_items ctxt =
- map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt;
+ map (Document_Antiquotation.output ctxt #> XML.Text) #>
+ separate (XML.Text "\\isasep\\isanewline%\n") #> isabelle ctxt;
fun pretty_items_source ctxt embedded src prts =
if is_source ctxt then source ctxt embedded src else pretty_items ctxt prts;
--- a/src/Pure/Thy/latex.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/Thy/latex.ML Tue May 25 22:28:39 2021 +0200
@@ -6,14 +6,13 @@
signature LATEX =
sig
- type text
- val string: string -> text
+ type text = XML.body
val text: string * Position.T -> text
- val block: text list -> text
- val enclose_body: string -> string -> text list -> text list
- val enclose_block: string -> string -> text list -> text
- val output_text: text list -> string
- val output_positions: Position.T -> text list -> string
+ val string: string -> text
+ val block: text -> XML.tree
+ val enclose_text: string -> string -> text -> text
+ val latex_text: text -> text
+ val output_text: text -> string
val output_name: string -> string
val output_ascii: string -> string
val output_ascii_breakable: string -> string -> string
@@ -25,9 +24,9 @@
val end_delim: string -> string
val begin_tag: string -> string
val end_tag: string -> string
- val environment_block: string -> text list -> text
+ val environment_text: string -> text -> text
val environment: string -> string -> string
- val isabelle_body: string -> text list -> text list
+ val isabelle_body: string -> text -> text
val theory_entry: string -> string
val index_escape: string -> string
type index_item = {text: text, like: string}
@@ -45,53 +44,24 @@
(* text with positions *)
-abstype text = Text of string * Position.T | Block of text list
-with
-
-fun string s = Text (s, Position.none);
-val text = Text;
-val block = Block;
-
-fun map_text f (Text (s, pos)) = Text (f s, pos)
- | map_text f (Block texts) = Block ((map o map_text) f texts);
+type text = XML.body;
-fun output_text texts =
- let
- fun output (Text (s, _)) = Buffer.add s
- | output (Block body) = fold output body;
- in Buffer.empty |> fold output texts |> Buffer.content end;
+fun text ("", _) = []
+ | text (s, pos) = [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
-fun output_positions file_pos texts =
- let
- fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b);
- fun add_position p positions =
- let val s = position (apply2 Value.print_int p)
- in positions |> s <> hd positions ? cons s end;
+fun string s = text (s, Position.none);
+
+fun block body = XML.Elem (Markup.document_latex, body);
- fun output (Text (s, pos)) (positions, line) =
- let
- val positions' =
- (case Position.line_of pos of
- NONE => positions
- | SOME l => add_position (line, l) positions);
- val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line;
- in (positions', line') end
- | output (Block body) res = fold output body res;
- in
- (case Position.file_of file_pos of
- NONE => ""
- | SOME file =>
- ([position (Markup.fileN, file), "\\endinput"], 1)
- |> fold output texts |> #1 |> rev |> cat_lines)
- end;
+fun latex_text text =
+ text |> maps
+ (fn XML.Elem ((name, _), body) =>
+ if name = Markup.document_latexN then latex_text body else []
+ | t => [t]);
-end;
+val output_text = XML.content_of o latex_text;
-fun enclose_body bg en body =
- (if bg = "" then [] else [string bg]) @ body @
- (if en = "" then [] else [string en]);
-
-fun enclose_block bg en = block o enclose_body bg en;
+fun enclose_text bg en body = string bg @ body @ string en;
(* output name for LaTeX macros *)
@@ -240,11 +210,11 @@
("%\n\\begin{" ^ output_name name ^ "}%\n",
"%\n\\end{" ^ output_name name ^ "}");
-fun environment_block name = environment_delim name |-> enclose_body #> block;
+fun environment_text name = environment_delim name |-> enclose_text;
fun environment name = environment_delim name |-> enclose;
fun isabelle_body name =
- enclose_body
+ enclose_text
("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
"%\n\\end{isabellebody}%\n";
@@ -266,7 +236,7 @@
val like_text =
if #like item = "" then ""
else index_escape (#like item) ^ "@";
- val item_text = index_escape (output_text [#text item]);
+ val item_text = index_escape (output_text (#text item));
in like_text ^ item_text end;
fun index_entry (entry: index_entry) =
--- a/src/Pure/Thy/latex.scala Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/Thy/latex.scala Tue May 25 22:28:39 2021 +0200
@@ -28,6 +28,44 @@
}
+ /* output text and positions */
+
+ type Text = XML.Body
+
+ def output(latex_text: Text, file_pos: String = ""): String =
+ {
+ def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%"
+
+ var positions: List[String] =
+ if (file_pos.isEmpty) Nil
+ else List(position(Markup.FILE, file_pos), "\\endinput")
+
+ var line = 1
+ var result = List.empty[String]
+
+ def output(body: XML.Body): Unit =
+ {
+ body.foreach {
+ case XML.Wrapped_Elem(_, _, _) =>
+ case XML.Elem(markup, body) =>
+ if (markup.name == Markup.DOCUMENT_LATEX) {
+ for { l <- Position.Line.unapply(markup.properties) if positions.nonEmpty } {
+ val s = position(Value.Int(line), Value.Int(l))
+ if (positions.head != s) positions ::= s
+ }
+ output(body)
+ }
+ case XML.Text(s) =>
+ line += s.count(_ == '\n')
+ result ::= s
+ }
+ }
+ output(latex_text)
+
+ result.reverse.mkString + cat_lines(positions.reverse)
+ }
+
+
/* generated .tex file */
private val File_Pattern = """^%:%file=(.+)%:%$""".r
--- a/src/Pure/Thy/thy_info.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue May 25 22:28:39 2021 +0200
@@ -78,10 +78,8 @@
let
val thy_name = Context.theory_name thy;
val document_tex_name = document_tex_name thy;
-
val latex = Latex.isabelle_body thy_name body;
- val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
- in Export.export thy document_tex_name (XML.blob output) end
+ in Export.export thy document_tex_name latex end
end));
--- a/src/Pure/Tools/rail.ML Tue May 25 21:44:01 2021 +0200
+++ b/src/Pure/Tools/rail.ML Tue May 25 22:28:39 2021 +0200
@@ -341,7 +341,7 @@
let
val output_antiq =
Antiquote.Antiq #>
- Document_Antiquotation.evaluate (single o Latex.symbols) ctxt #>
+ Document_Antiquotation.evaluate Latex.symbols ctxt #>
Latex.output_text;
fun output_text b s =
Output.output s