diff --git a/src/Doc/antiquote_setup.ML b/src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML
+++ b/src/Doc/antiquote_setup.ML
@@ -1,158 +1,158 @@
 (*  Title:      Doc/antiquote_setup.ML
     Author:     Makarius
 
 Auxiliary antiquotations for the Isabelle manuals.
 *)
 
 structure Antiquote_Setup: sig end =
 struct
 
 (* misc utils *)
 
 fun translate f = Symbol.explode #> map f #> implode;
 
 val clean_string = translate
   (fn "_" => "\\_"
     | "#" => "\\#"
     | "$" => "\\$"
     | "%" => "\\%"
     | "<" => "$<$"
     | ">" => "$>$"
     | "{" => "\\{"
     | "|" => "$\\mid$"
     | "}" => "\\}"
     | "\<hyphen>" => "-"
     | c => c);
 
 fun clean_name "\<dots>" = "dots"
   | clean_name ".." = "ddot"
   | clean_name "." = "dot"
   | clean_name "_" = "underscore"
   | clean_name "{" = "braceleft"
   | clean_name "}" = "braceright"
   | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
 
 
 (* named theorems *)
 
 val _ =
   Theory.setup (Document_Output.antiquotation_raw \<^binding>\<open>named_thms\<close>
     (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
     (fn ctxt =>
       map (fn (thm, name) =>
         Output.output
           (Document_Antiquotation.format ctxt
             (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));
 
 
 (* Isabelle/Isar entities (with index) *)
 
 local
 
 fun no_check (_: Proof.context) (name, _: Position.T) = name;
 
 fun check_keyword ctxt (name, pos) =
   if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name
   else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos);
 
 fun check_system_option ctxt arg =
   (Completion.check_option (Options.default ()) ctxt arg; true)
     handle ERROR _ => false;
 
 val arg = enclose "{" "}" o clean_string;
 
 fun entity check markup binding index =
   Document_Output.antiquotation_raw
     (binding |> Binding.map_name (fn name => name ^
       (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
     (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name_position))
     (fn ctxt => fn (logic, (name, pos)) =>
       let
         val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
         val hyper_name =
           "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
         val hyper =
           enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
           index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
         val idx =
           (case index of
             NONE => ""
           | SOME is_def =>
               "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
         val _ =
           if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else ();
         val latex =
           idx ^
           (Output.output name
             |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
             |> hyper o enclose "\\mbox{\\isa{" "}}");
       in Latex.string latex end);
 
 fun entity_antiqs check markup kind =
   entity check markup kind NONE #>
   entity check markup kind (SOME true) #>
   entity check markup kind (SOME false);
 
 in
 
 val _ =
   Theory.setup
    (entity_antiqs no_check "" \<^binding>\<open>syntax\<close> #>
     entity_antiqs Outer_Syntax.check_command "isacommand" \<^binding>\<open>command\<close> #>
     entity_antiqs check_keyword "isakeyword" \<^binding>\<open>keyword\<close> #>
     entity_antiqs check_keyword "isakeyword" \<^binding>\<open>element\<close> #>
     entity_antiqs Method.check_name "" \<^binding>\<open>method\<close> #>
     entity_antiqs Attrib.check_name "" \<^binding>\<open>attribute\<close> #>
     entity_antiqs no_check "" \<^binding>\<open>fact\<close> #>
     entity_antiqs no_check "" \<^binding>\<open>variable\<close> #>
     entity_antiqs no_check "" \<^binding>\<open>case\<close> #>
     entity_antiqs Document_Antiquotation.check "" \<^binding>\<open>antiquotation\<close> #>
     entity_antiqs Document_Antiquotation.check_option "" \<^binding>\<open>antiquotation_option\<close> #>
     entity_antiqs Document_Marker.check "" \<^binding>\<open>document_marker\<close> #>
     entity_antiqs no_check "isasystem" \<^binding>\<open>setting\<close> #>
     entity_antiqs check_system_option "isasystem" \<^binding>\<open>system_option\<close> #>
     entity_antiqs no_check "" \<^binding>\<open>inference\<close> #>
     entity_antiqs no_check "isasystem" \<^binding>\<open>executable\<close> #>
     entity_antiqs Isabelle_Tool.check "isatool" \<^binding>\<open>tool\<close> #>
     entity_antiqs ML_Context.check_antiquotation "" \<^binding>\<open>ML_antiquotation\<close> #>
     entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\<open>action\<close>);
 
 end;
 
 
 (* show symbols *)
 
 val _ =
   Theory.setup (Document_Output.antiquotation_raw \<^binding>\<open>show_symbols\<close> (Scan.succeed ())
     (fn _ => fn _ =>
       let
         val symbol_name =
           unprefix "\\newcommand{\\isasym"
           #> raw_explode
           #> take_prefix Symbol.is_ascii_letter
           #> implode;
 
         val symbols =
           File.read \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close>
           |> split_lines
           |> map_filter (fn line =>
             (case try symbol_name line of
               NONE => NONE
             | SOME "" => NONE
             | SOME name => SOME ("\\verb,\\" ^ "<" ^ name ^ ">, & {\\isasym" ^ name ^ "}")));
 
         val eol = "\\\\\n";
         fun table (a :: b :: rest) = a ^ " & " ^ b ^ eol :: table rest
           | table [a] = [a ^ eol]
           | table [] = [];
       in
         Latex.string
           ("\\begin{supertabular}{ll@{\\qquad}ll}\n" ^ implode (table symbols) ^
            "\\end{supertabular}\n")
       end))
 
 end;
diff --git a/src/Pure/PIDE/markup.ML b/src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML
+++ b/src/Pure/PIDE/markup.ML
@@ -1,785 +1,788 @@
 (*  Title:      Pure/PIDE/markup.ML
     Author:     Makarius
 
 Quasi-abstract markup elements.
 *)
 
 signature MARKUP =
 sig
   type T = string * Properties.T
   val empty: T
   val is_empty: T -> bool
   val properties: Properties.T -> T -> T
   val nameN: string val name: string -> T -> T
   val xnameN: string val xname: string -> T -> T
   val kindN: string
   val serialN: string
   val serial_properties: int -> Properties.T
   val instanceN: string
   val meta_titleN: string val meta_title: T
   val meta_creatorN: string val meta_creator: T
   val meta_contributorN: string val meta_contributor: T
   val meta_dateN: string val meta_date: T
   val meta_licenseN: string val meta_license: T
   val meta_descriptionN: string val meta_description: T
   val languageN: string
   val symbolsN: string
   val delimitedN: string
   val is_delimited: Properties.T -> bool
   val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
   val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
   val language_Isar: bool -> T
   val language_method: T
   val language_attribute: T
   val language_sort: bool -> T
   val language_type: bool -> T
   val language_term: bool -> T
   val language_prop: bool -> T
   val language_ML: bool -> T
   val language_SML: bool -> T
   val language_document: bool -> T
   val language_document_marker: T
   val language_antiquotation: T
   val language_text: bool -> T
   val language_verbatim: bool -> T
   val language_latex: bool -> T
   val language_rail: T
   val language_path: bool -> T
   val language_url: bool -> T
   val language_mixfix: T
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
   val defN: string
   val refN: string
   val completionN: string val completion: T
   val no_completionN: string val no_completion: T
   val updateN: string val update: T
   val lineN: string
   val end_lineN: string
   val offsetN: string
   val end_offsetN: string
   val fileN: string
   val idN: string
   val position_properties: string list
   val position_property: Properties.entry -> bool
   val positionN: string val position: T
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
   val toolN: string val tool: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
   val block_properties: string list
   val indentN: string
   val widthN: string
   val blockN: string val block: bool -> int -> T
   val breakN: string val break: int -> int -> T
   val fbreakN: string val fbreak: T
   val itemN: string val item: T
   val wordsN: string val words: T
   val hiddenN: string val hidden: T
   val deleteN: string val delete: T
   val bash_functionN: string
   val scala_functionN: string
   val system_optionN: string
   val sessionN: string
   val theoryN: string
   val classN: string
   val type_nameN: string
   val constantN: string
   val fixedN: string val fixed: string -> T
   val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
   val literal_factN: string val literal_fact: string -> T
   val method_modifierN: string
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
   val freeN: string val free: T
   val skolemN: string val skolem: T
   val boundN: string val bound: T
   val varN: string val var: T
   val numeralN: string val numeral: T
   val literalN: string val literal: T
   val delimiterN: string val delimiter: T
   val inner_stringN: string val inner_string: T
   val inner_cartoucheN: string val inner_cartouche: T
   val token_rangeN: string val token_range: T
   val sortingN: string val sorting: T
   val typingN: string val typing: T
   val class_parameterN: string val class_parameter: T
   val ML_keyword1N: string val ML_keyword1: T
   val ML_keyword2N: string val ML_keyword2: T
   val ML_keyword3N: string val ML_keyword3: T
   val ML_delimiterN: string val ML_delimiter: T
   val ML_tvarN: string val ML_tvar: T
   val ML_numeralN: string val ML_numeral: T
   val ML_charN: string val ML_char: T
   val ML_stringN: string val ML_string: T
   val ML_commentN: string val ML_comment: T
   val ML_defN: string
   val ML_openN: string
   val ML_structureN: string
   val ML_typingN: string val ML_typing: T
   val ML_breakpointN: string val ML_breakpoint: int -> T
   val antiquotedN: string val antiquoted: T
   val antiquoteN: string val antiquote: T
   val file_typeN: string
   val antiquotationN: string
   val ML_antiquotationN: string
   val document_antiquotationN: string
   val document_antiquotation_optionN: string
   val raw_textN: string val raw_text: T
   val plain_textN: string val plain_text: T
   val paragraphN: string val paragraph: T
   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
   val markdown_listN: string val markdown_list: string -> T
   val itemizeN: string
   val enumerateN: string
   val descriptionN: string
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
   val commandN: string val command_properties: T -> T
   val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
   val alt_stringN: string val alt_string: T
   val verbatimN: string val verbatim: T
   val cartoucheN: string val cartouche: T
   val commentN: string val comment: T
   val keyword1N: string val keyword1: T
   val keyword2N: string val keyword2: T
   val keyword3N: string val keyword3: T
   val quasi_keywordN: string val quasi_keyword: T
   val improperN: string val improper: T
   val operatorN: string val operator: T
   val comment1N: string val comment1: T
   val comment2N: string val comment2: T
   val comment3N: string val comment3: T
   val elapsedN: string
   val cpuN: string
   val gcN: string
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
   val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
   val command_indentN: string val command_indent: int -> T
   val goalN: string val goal: T
   val subgoalN: string val subgoal: string -> T
   val taskN: string
   val forkedN: string val forked: T
   val joinedN: string val joined: T
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
   val canceledN: string val canceled: T
   val initializedN: string val initialized: T
   val finalizedN: string val finalized: T
   val consolidatingN: string val consolidating: T
   val consolidatedN: string val consolidated: T
   val exec_idN: string
   val initN: string
   val statusN: string val status: T
   val resultN: string val result: T
   val writelnN: string val writeln: T
   val stateN: string val state: T
   val informationN: string val information: T
   val tracingN: string val tracing: T
   val warningN: string val warning: T
   val legacyN: string val legacy: T
   val errorN: string val error: T
   val systemN: string val system: T
   val protocolN: string
   val reportN: string val report: T
   val no_reportN: string val no_report: T
   val badN: string val bad: unit -> T
   val intensifyN: string val intensify: T
   val browserN: string
   val graphviewN: string
   val theory_exportsN: string
   val sendbackN: string
   val paddingN: string
   val padding_line: Properties.entry
   val padding_command: Properties.entry
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val functionN: string
   val ML_statistics: {pid: int, stats_dir: string} -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val theory_timing: Properties.entry
   val session_timing: Properties.entry
   val loading_theory: string -> Properties.T
   val build_session_finished: Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
   val exportN: string
   type export_args =
    {id: string option,
     serial: serial,
     theory_name: string,
     name: string,
     executable: bool,
     compress: bool,
     strict: bool}
   val export: export_args -> Properties.T
   val debugger_state: string -> Properties.T
   val debugger_output: string -> Properties.T
   val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
   val simp_trace_hintN: string
   val simp_trace_ignoreN: string
   val simp_trace_cancel: serial -> Properties.T
   type output = Output.output * Output.output
   val no_output: output
   val add_mode: string -> (T -> output) -> unit
   val output: T -> output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markups: T list -> string -> string
   val markup_only: T -> string
   val markup_report: string -> string
 end;
 
 structure Markup: MARKUP =
 struct
 
 (** markup elements **)
 
 (* basic markup *)
 
 type T = string * Properties.T;
 
 val empty = ("", []);
 
 fun is_empty ("", _) = true
   | is_empty _ = false;
 
 
 fun properties more_props ((elem, props): T) =
   (elem, fold_rev Properties.put more_props props);
 
 fun markup_elem name = (name, (name, []): T);
 fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T);
 fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T);
 
 
 (* misc properties *)
 
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
 val xnameN = "xname";
 fun xname a = properties [(xnameN, a)];
 
 val kindN = "kind";
 
 val serialN = "serial";
 fun serial_properties i = [(serialN, Value.print_int i)];
 
 val instanceN = "instance";
 
 
 (* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *)
 
 val (meta_titleN, meta_title) = markup_elem "meta_title";
 val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
 val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
 val (meta_dateN, meta_date) = markup_elem "meta_date";
 val (meta_licenseN, meta_license) = markup_elem "meta_license";
 val (meta_descriptionN, meta_description) = markup_elem "meta_description";
 
 
 (* embedded languages *)
 
 val languageN = "language";
 val symbolsN = "symbols";
 val antiquotesN = "antiquotes";
 val delimitedN = "delimited"
 
 fun is_delimited props =
   Properties.get props delimitedN = SOME "true";
 
 fun language {name, symbols, antiquotes, delimited} =
   (languageN,
    [(nameN, name),
     (symbolsN, Value.print_bool symbols),
     (antiquotesN, Value.print_bool antiquotes),
     (delimitedN, Value.print_bool delimited)]);
 
 fun language' {name, symbols, antiquotes} delimited =
   language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
 
 val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false};
 val language_method =
   language {name = "method", symbols = true, antiquotes = false, delimited = false};
 val language_attribute =
   language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
 val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
 val language_type = language' {name = "type", symbols = true, antiquotes = false};
 val language_term = language' {name = "term", symbols = true, antiquotes = false};
 val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
 val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
 val language_document = language' {name = "document", symbols = false, antiquotes = true};
 val language_document_marker =
   language {name = "document_marker", symbols = true, antiquotes = true, delimited = true};
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
 val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false};
 val language_latex = language' {name = "latex", symbols = false, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
 val language_path = language' {name = "path", symbols = false, antiquotes = false};
 val language_url = language' {name = "url", symbols = false, antiquotes = false};
 val language_mixfix =
   language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true};
 
 
 (* formal entities *)
 
 val (bindingN, binding) = markup_elem "binding";
 
 val entityN = "entity";
 fun entity kind name =
   (entityN,
     (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
 
 val defN = "def";
 val refN = "ref";
 
 
 (* completion *)
 
 val (completionN, completion) = markup_elem "completion";
 val (no_completionN, no_completion) = markup_elem "no_completion";
 
 val (updateN, update) = markup_elem "update";
 
 
 (* position *)
 
 val lineN = "line";
 val end_lineN = "end_line";
 
 val offsetN = "offset";
 val end_offsetN = "end_offset";
 
 val fileN = "file";
 val idN = "id";
 
 val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
 fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
 
 val (positionN, position) = markup_elem "position";
 
 
 (* expression *)
 
 val expressionN = "expression";
 fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]);
 
 
 (* citation *)
 
 val (citationN, citation) = markup_string "citation" nameN;
 
 
 (* external resources *)
 
 val (pathN, path) = markup_string "path" nameN;
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
 val (toolN, tool) = markup_string "tool" nameN;
 
 
 (* pretty printing *)
 
 val markupN = "markup";
 val consistentN = "consistent";
 val unbreakableN = "unbreakable";
 val indentN = "indent";
 
 val block_properties = [markupN, consistentN, unbreakableN, indentN];
 
 val widthN = "width";
 
 val blockN = "block";
 fun block c i =
   (blockN,
     (if c then [(consistentN, Value.print_bool c)] else []) @
     (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val breakN = "break";
 fun break w i =
   (breakN,
     (if w <> 0 then [(widthN, Value.print_int w)] else []) @
     (if i <> 0 then [(indentN, Value.print_int i)] else []));
 
 val (fbreakN, fbreak) = markup_elem "fbreak";
 
 val (itemN, item) = markup_elem "item";
 
 
 (* text properties *)
 
 val (wordsN, words) = markup_elem "words";
 
 val (hiddenN, hidden) = markup_elem "hidden";
 
 val (deleteN, delete) = markup_elem "delete";
 
 
 (* misc entities *)
 
 val bash_functionN = "bash_function";
 val scala_functionN = "scala_function";
 val system_optionN = "system_option";
 
 val sessionN = "session";
 
 val theoryN = "theory";
 val classN = "class";
 val type_nameN = "type_name";
 val constantN = "constant";
 
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 val (literal_factN, literal_fact) = markup_string "literal_fact" nameN;
 
 val method_modifierN = "method_modifier";
 
 
 (* inner syntax *)
 
 val (tfreeN, tfree) = markup_elem "tfree";
 val (tvarN, tvar) = markup_elem "tvar";
 val (freeN, free) = markup_elem "free";
 val (skolemN, skolem) = markup_elem "skolem";
 val (boundN, bound) = markup_elem "bound";
 val (varN, var) = markup_elem "var";
 val (numeralN, numeral) = markup_elem "numeral";
 val (literalN, literal) = markup_elem "literal";
 val (delimiterN, delimiter) = markup_elem "delimiter";
 val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche";
 
 val (token_rangeN, token_range) = markup_elem "token_range";
 
 val (sortingN, sorting) = markup_elem "sorting";
 val (typingN, typing) = markup_elem "typing";
 val (class_parameterN, class_parameter) = markup_elem "class_parameter";
 
 
 (* ML *)
 
 val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
 val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
 val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3";
 val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
 val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
 val (ML_charN, ML_char) = markup_elem "ML_char";
 val (ML_stringN, ML_string) = markup_elem "ML_string";
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
 
 val ML_defN = "ML_def";
 val ML_openN = "ML_open";
 val ML_structureN = "ML_structure";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
 val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN;
 
 
 (* antiquotations *)
 
 val (antiquotedN, antiquoted) = markup_elem "antiquoted";
 val (antiquoteN, antiquote) = markup_elem "antiquote";
 
 val file_typeN = "file_type";
 val antiquotationN = "antiquotation";
 val ML_antiquotationN = "ML_antiquotation";
 val document_antiquotationN = "document_antiquotation";
 val document_antiquotation_optionN = "document_antiquotation_option";
 
 
 (* document text *)
 
 val (raw_textN, raw_text) = markup_elem "raw_text";
 val (plain_textN, plain_text) = markup_elem "plain_text";
 
 val (paragraphN, paragraph) = markup_elem "paragraph";
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
 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 *)
 
 val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph";
 val (markdown_itemN, markdown_item) = markup_elem "markdown_item";
 val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth";
 val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN;
 
 val itemizeN = "itemize";
 val enumerateN = "enumerate";
 val descriptionN = "description";
 
 
 (* formal input *)
 
 val inputN = "input";
 fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props);
 
 
 (* outer syntax *)
 
 val (command_keywordN, command_keyword) = markup_elem "command_keyword";
 
 val commandN = "command"; val command_properties = properties [(kindN, commandN)];
 val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
 
 val (keyword1N, keyword1) = markup_elem "keyword1";
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (keyword3N, keyword3) = markup_elem "keyword3";
 val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
 val (improperN, improper) = markup_elem "improper";
 val (operatorN, operator) = markup_elem "operator";
 val (stringN, string) = markup_elem "string";
 val (alt_stringN, alt_string) = markup_elem "alt_string";
 val (verbatimN, verbatim) = markup_elem "verbatim";
 val (cartoucheN, cartouche) = markup_elem "cartouche";
 val (commentN, comment) = markup_elem "comment";
 
 
 (* comments *)
 
 val (comment1N, comment1) = markup_elem "comment1";
 val (comment2N, comment2) = markup_elem "comment2";
 val (comment3N, comment3) = markup_elem "comment3";
 
 
 (* timing *)
 
 val elapsedN = "elapsed";
 val cpuN = "cpu";
 val gcN = "gc";
 
 fun timing_properties {elapsed, cpu, gc} =
  [(elapsedN, Value.print_time elapsed),
   (cpuN, Value.print_time cpu),
   (gcN, Value.print_time gc)];
 
 val timingN = "timing";
 fun timing t = (timingN, timing_properties t);
 
 
 (* command timing *)
 
 fun parse_command_timing_properties props =
   (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
     (SOME file, SOME offset, SOME name) =>
       SOME ({file = file, offset = Value.parse_int offset, name = name},
         Properties.seconds props elapsedN)
   | _ => NONE);
 
 
 (* indentation *)
 
 val (command_indentN, command_indent) = markup_int "command_indent" indentN;
 
 
 (* goals *)
 
 val (goalN, goal) = markup_elem "goal";
 val (subgoalN, subgoal) = markup_string "subgoal" nameN;
 
 
 (* command status *)
 
 val taskN = "task";
 
 val (forkedN, forked) = markup_elem "forked";
 val (joinedN, joined) = markup_elem "joined";
 val (runningN, running) = markup_elem "running";
 val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
 val (canceledN, canceled) = markup_elem "canceled";
 val (initializedN, initialized) = markup_elem "initialized";
 val (finalizedN, finalized) = markup_elem "finalized";
 val (consolidatingN, consolidating) = markup_elem "consolidating";
 val (consolidatedN, consolidated) = markup_elem "consolidated";
 
 
 (* messages *)
 
 val exec_idN = "exec_id";
 
 val initN = "init";
 val (statusN, status) = markup_elem "status";
 val (resultN, result) = markup_elem "result";
 val (writelnN, writeln) = markup_elem "writeln";
 val (stateN, state) = markup_elem "state"
 val (informationN, information) = markup_elem "information";
 val (tracingN, tracing) = markup_elem "tracing";
 val (warningN, warning) = markup_elem "warning";
 val (legacyN, legacy) = markup_elem "legacy";
 val (errorN, error) = markup_elem "error";
 val (systemN, system) = markup_elem "system";
 val protocolN = "protocol";
 
 val (reportN, report) = markup_elem "report";
 val (no_reportN, no_report) = markup_elem "no_report";
 
 val badN = "bad";
 fun bad () = (badN, serial_properties (serial ()));
 
 val (intensifyN, intensify) = markup_elem "intensify";
 
 
 (* active areas *)
 
 val browserN = "browser"
 val graphviewN = "graphview";
 val theory_exportsN = "theory_exports";
 
 val sendbackN = "sendback";
 val paddingN = "padding";
 val padding_line = (paddingN, "line");
 val padding_command = (paddingN, "command");
 
 val dialogN = "dialog";
 fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]);
 
 val jedit_actionN = "jedit_action";
 
 
 (* protocol message functions *)
 
 val functionN = "function"
 
 fun ML_statistics {pid, stats_dir} =
   [(functionN, "ML_statistics"), ("pid", Value.print_int pid), ("stats_dir", stats_dir)];
 
 val commands_accepted = [(functionN, "commands_accepted")];
 
 val assign_update = [(functionN, "assign_update")];
 val removed_versions = [(functionN, "removed_versions")];
 
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
 val task_statistics = (functionN, "task_statistics");
 
 val command_timing = (functionN, "command_timing");
 
 val theory_timing = (functionN, "theory_timing");
 
 val session_timing = (functionN, "session_timing");
 
 fun loading_theory name = [("function", "loading_theory"), (nameN, name)];
 
 val build_session_finished = [("function", "build_session_finished")];
 
 val print_operationsN = "print_operations";
 val print_operations = [(functionN, print_operationsN)];
 
 
 (* export *)
 
 val exportN = "export";
 
 type export_args =
  {id: string option,
   serial: serial,
   theory_name: string,
   name: string,
   executable: bool,
   compress: bool,
   strict: bool};
 
 fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) =
  [(functionN, exportN),
   (idN, the_default "" id),
   (serialN, Value.print_int serial),
   ("theory_name", theory_name),
   (nameN, name),
   ("executable", Value.print_bool executable),
   ("compress", Value.print_bool compress),
   ("strict", Value.print_bool strict)];
 
 
 (* debugger *)
 
 fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)];
 fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)];
 
 
 (* simplifier trace *)
 
 val simp_trace_panelN = "simp_trace_panel";
 
 val simp_trace_logN = "simp_trace_log";
 val simp_trace_stepN = "simp_trace_step";
 val simp_trace_recurseN = "simp_trace_recurse";
 val simp_trace_hintN = "simp_trace_hint";
 val simp_trace_ignoreN = "simp_trace_ignore";
 
 fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)];
 
 
 
 (** print mode operations **)
 
 type output = Output.output * Output.output;
 
 val no_output = ("", "");
 
 local
   val default = {output = Output_Primitives.markup_fn};
   val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
 in
   fun add_mode name output =
     Synchronized.change modes (fn tab =>
       (if not (Symtab.defined tab name) then ()
        else Output.warning ("Redefining markup mode " ^ quote name);
        Symtab.update (name, {output = output}) tab));
   fun get_mode () =
     the_default default
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;
 
 fun markup m =
   let val (bg, en) = output m
   in Library.enclose (Output.escape bg) (Output.escape en) end;
 
 val markups = fold_rev markup;
 
 fun markup_only m = markup m "";
 
 fun markup_report "" = ""
   | markup_report txt = markup report txt;
 
 end;
diff --git a/src/Pure/PIDE/markup.scala b/src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala
+++ b/src/Pure/PIDE/markup.scala
@@ -1,741 +1,743 @@
 /*  Title:      Pure/PIDE/markup.scala
     Author:     Makarius
 
 Quasi-abstract markup elements.
 */
 
 package isabelle
 
 
 object Markup
 {
   /* elements */
 
   object Elements
   {
     def apply(elems: Set[String]): Elements = new Elements(elems)
     def apply(elems: String*): Elements = apply(Set(elems: _*))
     val empty: Elements = apply()
     val full: Elements =
       new Elements(Set.empty)
       {
         override def apply(elem: String): Boolean = true
         override def toString: String = "Elements.full"
       }
   }
 
   sealed class Elements private[Markup](private val rep: Set[String])
   {
     def apply(elem: String): Boolean = rep.contains(elem)
     def + (elem: String): Elements = new Elements(rep + elem)
     def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep)
     def - (elem: String): Elements = new Elements(rep - elem)
     def -- (elems: Elements): Elements = new Elements(rep -- elems.rep)
     override def toString: String = rep.mkString("Elements(", ",", ")")
   }
 
 
   /* properties */
 
   val NAME = "name"
   val Name = new Properties.String(NAME)
 
   val XNAME = "xname"
   val XName = new Properties.String(XNAME)
 
   val KIND = "kind"
   val Kind = new Properties.String(KIND)
 
   val CONTENT = "content"
   val Content = new Properties.String(CONTENT)
 
   val SERIAL = "serial"
   val Serial = new Properties.Long(SERIAL)
 
   val INSTANCE = "instance"
   val Instance = new Properties.String(INSTANCE)
 
 
   /* basic markup */
 
   val Empty: Markup = Markup("", Nil)
   val Broken: Markup = Markup("broken", Nil)
 
   class Markup_String(val name: String, prop: String)
   {
     private val Prop = new Properties.String(prop)
 
     def apply(s: String): Markup = Markup(name, Prop(s))
     def unapply(markup: Markup): Option[String] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
   class Markup_Int(val name: String, prop: String)
   {
     private val Prop = new Properties.Int(prop)
 
     def apply(i: Int): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
   class Markup_Long(val name: String, prop: String)
   {
     private val Prop = new Properties.Long(prop)
 
     def apply(i: Long): Markup = Markup(name, Prop(i))
     def unapply(markup: Markup): Option[Long] =
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
 
   /* meta data */
 
   val META_TITLE = "meta_title"
   val META_CREATOR = "meta_creator"
   val META_CONTRIBUTOR = "meta_contributor"
   val META_DATE = "meta_date"
   val META_LICENSE = "meta_license"
   val META_DESCRIPTION = "meta_description"
 
 
   /* formal entities */
 
   val BINDING = "binding"
   val ENTITY = "entity"
 
   val Def = new Properties.Long("def")
   val Ref = new Properties.Long("ref")
 
   object Entity
   {
     object Def
     {
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None
     }
     object Ref
     {
       def unapply(markup: Markup): Option[Long] =
         if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None
     }
     object Occ
     {
       def unapply(markup: Markup): Option[Long] =
         Def.unapply(markup) orElse Ref.unapply(markup)
     }
 
     def unapply(markup: Markup): Option[(String, String)] =
       markup match {
         case Markup(ENTITY, props) =>
           val kind = Kind.unapply(props).getOrElse("")
           val name = Name.unapply(props).getOrElse("")
           Some((kind, name))
         case _ => None
       }
   }
 
 
   /* completion */
 
   val COMPLETION = "completion"
   val NO_COMPLETION = "no_completion"
 
   val UPDATE = "update"
 
 
   /* position */
 
   val LINE = "line"
   val END_LINE = "line"
   val OFFSET = "offset"
   val END_OFFSET = "end_offset"
   val FILE = "file"
   val ID = "id"
 
   val DEF_LINE = "def_line"
   val DEF_OFFSET = "def_offset"
   val DEF_END_OFFSET = "def_end_offset"
   val DEF_FILE = "def_file"
   val DEF_ID = "def_id"
 
   val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
   def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
 
   val POSITION = "position"
 
 
   /* expression */
 
   val EXPRESSION = "expression"
   object Expression
   {
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(EXPRESSION, Kind(kind)) => Some(kind)
         case Markup(EXPRESSION, _) => Some("")
         case _ => None
       }
   }
 
 
   /* citation */
 
   val CITATION = "citation"
   val Citation = new Markup_String(CITATION, NAME)
 
 
   /* embedded languages */
 
   val Symbols = new Properties.Boolean("symbols")
   val Antiquotes = new Properties.Boolean("antiquotes")
   val Delimited = new Properties.Boolean("delimited")
 
   val LANGUAGE = "language"
   object Language
   {
     val DOCUMENT = "document"
     val ML = "ML"
     val SML = "SML"
     val PATH = "path"
     val UNKNOWN = "unknown"
 
     def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
       markup match {
         case Markup(LANGUAGE, props) =>
           (props, props, props, props) match {
             case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) =>
               Some((name, symbols, antiquotes, delimited))
             case _ => None
           }
         case _ => None
       }
 
     object Path
     {
       def unapply(markup: Markup): Option[Boolean] =
         markup match {
           case Language(PATH, _, _, delimited) => Some(delimited)
           case _ => None
         }
     }
   }
 
 
   /* external resources */
 
   val PATH = "path"
   val Path = new Markup_String(PATH, NAME)
 
   val EXPORT_PATH = "export_path"
   val Export_Path = new Markup_String(EXPORT_PATH, NAME)
 
   val URL = "url"
   val Url = new Markup_String(URL, NAME)
 
   val DOC = "doc"
   val Doc = new Markup_String(DOC, NAME)
 
 
   /* pretty printing */
 
   val Consistent = new Properties.Boolean("consistent")
   val Indent = new Properties.Int("indent")
   val Width = new Properties.Int("width")
 
   object Block
   {
     val name = "block"
     def apply(c: Boolean, i: Int): Markup =
       Markup(name,
         (if (c) Consistent(c) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Boolean, Int)] =
       if (markup.name == name) {
         val c = Consistent.unapply(markup.properties).getOrElse(false)
         val i = Indent.unapply(markup.properties).getOrElse(0)
         Some((c, i))
       }
       else None
   }
 
   object Break
   {
     val name = "break"
     def apply(w: Int, i: Int): Markup =
       Markup(name,
         (if (w != 0) Width(w) else Nil) :::
         (if (i != 0) Indent(i) else Nil))
     def unapply(markup: Markup): Option[(Int, Int)] =
       if (markup.name == name) {
         val w = Width.unapply(markup.properties).getOrElse(0)
         val i = Indent.unapply(markup.properties).getOrElse(0)
         Some((w, i))
       }
       else None
   }
 
   val ITEM = "item"
   val BULLET = "bullet"
 
   val SEPARATOR = "separator"
 
 
   /* text properties */
 
   val WORDS = "words"
 
   val HIDDEN = "hidden"
 
   val DELETE = "delete"
 
 
   /* misc entities */
 
   val THEORY = "theory"
   val CLASS = "class"
   val TYPE_NAME = "type_name"
   val FIXED = "fixed"
   val CASE = "case"
   val CONSTANT = "constant"
   val DYNAMIC_FACT = "dynamic_fact"
 
 
   /* inner syntax */
 
   val TFREE = "tfree"
   val TVAR = "tvar"
   val FREE = "free"
   val SKOLEM = "skolem"
   val BOUND = "bound"
   val VAR = "var"
   val NUMERAL = "numeral"
   val LITERAL = "literal"
   val DELIMITER = "delimiter"
   val INNER_STRING = "inner_string"
   val INNER_CARTOUCHE = "inner_cartouche"
 
   val TOKEN_RANGE = "token_range"
 
   val SORTING = "sorting"
   val TYPING = "typing"
   val CLASS_PARAMETER = "class_parameter"
 
   val ATTRIBUTE = "attribute"
   val METHOD = "method"
 
 
   /* antiquotations */
 
   val ANTIQUOTED = "antiquoted"
   val ANTIQUOTE = "antiquote"
 
   val ML_ANTIQUOTATION = "ML_antiquotation"
   val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
   /* document text */
 
   val RAW_TEXT = "raw_text"
   val PLAIN_TEXT = "plain_text"
 
   val PARAGRAPH = "paragraph"
   val TEXT_FOLD = "text_fold"
 
   object Document_Tag
   {
     val ELEMENT = "document_tag"
     val IMPORTANT = "important"
     val UNIMPORTANT = "unimportant"
 
     def unapply(markup: Markup): Option[String] =
       markup match {
         case Markup(ELEMENT, Name(name)) => Some(name)
         case _ => None
       }
   }
 
+  val DOCUMENT_LATEX = "document_latex"
+
 
   /* Markdown document structure */
 
   val MARKDOWN_PARAGRAPH = "markdown_paragraph"
   val MARKDOWN_ITEM = "markdown_item"
   val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth")
   val Markdown_List = new Markup_String("markdown_list", "kind")
 
   val ITEMIZE = "itemize"
   val ENUMERATE = "enumerate"
   val DESCRIPTION = "description"
 
 
   /* ML */
 
   val ML_KEYWORD1 = "ML_keyword1"
   val ML_KEYWORD2 = "ML_keyword2"
   val ML_KEYWORD3 = "ML_keyword3"
   val ML_DELIMITER = "ML_delimiter"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
   val ML_COMMENT = "ML_comment"
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
   val ML_STRUCTURE = "ML_structure"
   val ML_TYPING = "ML_typing"
 
   val ML_BREAKPOINT = "ML_breakpoint"
 
 
   /* outer syntax */
 
   val COMMAND = "command"
   val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"
   val KEYWORD2 = "keyword2"
   val KEYWORD3 = "keyword3"
   val QUASI_KEYWORD = "quasi_keyword"
   val IMPROPER = "improper"
   val OPERATOR = "operator"
   val STRING = "string"
   val ALT_STRING = "alt_string"
   val VERBATIM = "verbatim"
   val CARTOUCHE = "cartouche"
   val COMMENT = "comment"
 
   val LOAD_COMMAND = "load_command"
 
 
   /* comments */
 
   val COMMENT1 = "comment1"
   val COMMENT2 = "comment2"
   val COMMENT3 = "comment3"
 
 
   /* timing */
 
   val Elapsed = new Properties.Double("elapsed")
   val CPU = new Properties.Double("cpu")
   val GC = new Properties.Double("gc")
 
   object Timing_Properties
   {
     def apply(timing: isabelle.Timing): Properties.T =
       Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds)
 
     def unapply(props: Properties.T): Option[isabelle.Timing] =
       (props, props, props) match {
         case (Elapsed(elapsed), CPU(cpu), GC(gc)) =>
           Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
         case _ => None
       }
 
     def parse(props: Properties.T): isabelle.Timing =
       unapply(props) getOrElse isabelle.Timing.zero
   }
 
   val TIMING = "timing"
 
   object Timing
   {
     def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
 
     def unapply(markup: Markup): Option[isabelle.Timing] =
       markup match {
         case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
         case _ => None
       }
   }
 
 
   /* process result */
 
   val Return_Code = new Properties.Int("return_code")
 
   object Process_Result
   {
     def apply(result: Process_Result): Properties.T =
       Return_Code(result.rc) :::
         (if (result.timing.is_zero) Nil else Timing_Properties(result.timing))
 
     def unapply(props: Properties.T): Option[Process_Result] =
       props match {
         case Return_Code(rc) =>
           val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
           Some(isabelle.Process_Result(rc, timing = timing))
         case _ => None
       }
   }
 
 
   /* command indentation */
 
   object Command_Indent
   {
     val name = "command_indent"
     def unapply(markup: Markup): Option[Int] =
       if (markup.name == name) Indent.unapply(markup.properties) else None
   }
 
 
   /* goals */
 
   val GOAL = "goal"
   val SUBGOAL = "subgoal"
 
 
   /* command status */
 
   val TASK = "task"
 
   val ACCEPTED = "accepted"
   val FORKED = "forked"
   val JOINED = "joined"
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
   val CANCELED = "canceled"
   val INITIALIZED = "initialized"
   val FINALIZED = "finalized"
   val CONSOLIDATING = "consolidating"
   val CONSOLIDATED = "consolidated"
 
 
   /* interactive documents */
 
   val VERSION = "version"
   val ASSIGN = "assign"
 
 
   /* prover process */
 
   val PROVER_COMMAND = "prover_command"
   val PROVER_ARG = "prover_arg"
 
 
   /* messages */
 
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"
   val RESULT = "result"
   val WRITELN = "writeln"
   val STATE = "state"
   val INFORMATION = "information"
   val TRACING = "tracing"
   val WARNING = "warning"
   val LEGACY = "legacy"
   val ERROR = "error"
   val NODES_STATUS = "nodes_status"
   val PROTOCOL = "protocol"
   val SYSTEM = "system"
   val STDOUT = "stdout"
   val STDERR = "stderr"
   val EXIT = "exit"
 
   val WRITELN_MESSAGE = "writeln_message"
   val STATE_MESSAGE = "state_message"
   val INFORMATION_MESSAGE = "information_message"
   val TRACING_MESSAGE = "tracing_message"
   val WARNING_MESSAGE = "warning_message"
   val LEGACY_MESSAGE = "legacy_message"
   val ERROR_MESSAGE = "error_message"
 
   val messages = Map(
     WRITELN -> WRITELN_MESSAGE,
     STATE -> STATE_MESSAGE,
     INFORMATION -> INFORMATION_MESSAGE,
     TRACING -> TRACING_MESSAGE,
     WARNING -> WARNING_MESSAGE,
     LEGACY -> LEGACY_MESSAGE,
     ERROR -> ERROR_MESSAGE)
 
   val message: String => String = messages.withDefault((s: String) => s)
 
   val NO_REPORT = "no_report"
 
   val BAD = "bad"
 
   val INTENSIFY = "intensify"
 
 
   /* active areas */
 
   val BROWSER = "browser"
   val GRAPHVIEW = "graphview"
   val THEORY_EXPORTS = "theory_exports"
 
   val SENDBACK = "sendback"
   val PADDING = "padding"
   val PADDING_LINE = (PADDING, "line")
   val PADDING_COMMAND = (PADDING, "command")
 
   val DIALOG = "dialog"
   val Result = new Properties.String(RESULT)
 
   val JEDIT_ACTION = "jedit_action"
 
 
   /* protocol message functions */
 
   val FUNCTION = "function"
 
   class Function(val name: String)
   {
     val PROPERTY: Properties.Entry = (FUNCTION, name)
   }
 
   class Properties_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[Properties.T] =
       props match {
         case PROPERTY :: args => Some(args)
         case _ => None
       }
   }
 
   class Name_Function(name: String) extends Function(name)
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
   object ML_Statistics extends Function("ML_statistics")
   {
     def unapply(props: Properties.T): Option[(Long, String)] =
       props match {
         case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) =>
           Some((pid, stats_dir))
         case _ => None
       }
   }
 
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
   def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
 
   object Command_Timing extends Properties_Function("command_timing")
   object Theory_Timing extends Properties_Function("theory_timing")
   object Session_Timing extends Properties_Function("session_timing")
   {
     val Threads = new Properties.Int("threads")
   }
   object Task_Statistics extends Properties_Function("task_statistics")
 
   object Loading_Theory extends Properties_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
   object Commands_Accepted extends Function("commands_accepted")
   object Assign_Update extends Function("assign_update")
   object Removed_Versions extends Function("removed_versions")
 
   object Invoke_Scala extends Function("invoke_scala")
   {
     def unapply(props: Properties.T): Option[(String, String)] =
       props match {
         case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
         case _ => None
       }
   }
 
   object Cancel_Scala extends Function("cancel_scala")
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (ID, id)) => Some(id)
         case _ => None
       }
   }
 
   val PRINT_OPERATIONS = "print_operations"
 
 
   /* export */
 
   val EXPORT = "export"
   val THEORY_NAME = "theory_name"
   val EXECUTABLE = "executable"
   val COMPRESS = "compress"
   val STRICT = "strict"
 
 
   /* debugger output */
 
   val DEBUGGER_STATE = "debugger_state"
   object Debugger_State
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
   val DEBUGGER_OUTPUT = "debugger_output"
   object Debugger_Output
   {
     def unapply(props: Properties.T): Option[String] =
       props match {
         case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name)
         case _ => None
       }
   }
 
 
   /* simplifier trace */
 
   val SIMP_TRACE_PANEL = "simp_trace_panel"
 
   val SIMP_TRACE_LOG = "simp_trace_log"
   val SIMP_TRACE_STEP = "simp_trace_step"
   val SIMP_TRACE_RECURSE = "simp_trace_recurse"
   val SIMP_TRACE_HINT = "simp_trace_hint"
   val SIMP_TRACE_IGNORE = "simp_trace_ignore"
 
   val SIMP_TRACE_CANCEL = "simp_trace_cancel"
   object Simp_Trace_Cancel
   {
     def unapply(props: Properties.T): Option[Long] =
       props match {
         case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i)
         case _ => None
       }
   }
 
 
   /* XML data representation */
 
   def encode: XML.Encode.T[Markup] = (markup: Markup) =>
   {
     import XML.Encode._
     pair(string, properties)((markup.name, markup.properties))
   }
 
   def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
   {
     import XML.Decode._
     val (name, props) = pair(string, properties)(body)
     Markup(name, props)
   }
 }
 
 
 sealed case class Markup(name: String, properties: Properties.T)
 {
   def is_empty: Boolean = name.isEmpty
 
   def markup(s: String): String =
     YXML.string_of_tree(XML.Elem(this, List(XML.Text(s))))
 
   def update_properties(more_props: Properties.T): Markup =
     if (more_props.isEmpty) this
     else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) })
 
   def + (entry: Properties.Entry): Markup =
     Markup(name, Properties.put(properties, entry))
 }
diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML
+++ b/src/Pure/PIDE/resources.ML
@@ -1,443 +1,442 @@
 (*  Title:      Pure/PIDE/resources.ML
     Author:     Makarius
 
 Resources for theories and auxiliary files.
 *)
 
 signature RESOURCES =
 sig
   val default_qualifier: string
   val init_session:
     {session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
      session_chapters: (string * string) list,
      bibtex_entries: (string * string list) list,
      command_timings: Properties.T list,
      scala_functions: (string * (bool * Position.T)) list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
   val init_session_yxml: string -> unit
   val init_session_file: Path.T -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val check_session: Proof.context -> string * Position.T -> string
   val session_chapter: string -> string
   val last_timing: Toplevel.transition -> Time.time
   val scala_functions: unit -> string list
   val check_scala_function: Proof.context -> string * Position.T -> string * bool
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
   val theory_bibtex_entries: string -> string list
   val find_theory_file: string -> Path.T option
   val import_name: string -> Path.T -> string ->
     {node_name: Path.T, master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
   val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser
   val parse_file: (theory -> Token.file) parser
   val provide: Path.T * SHA1.digest -> theory -> theory
   val provide_file: Token.file -> theory -> theory
   val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser
   val provide_parse_file: (theory -> Token.file * theory) parser
   val loaded_files_current: theory -> bool
   val check_path: Proof.context -> Path.T option -> Input.source -> Path.T
   val check_file: Proof.context -> Path.T option -> Input.source -> Path.T
   val check_dir: Proof.context -> Path.T option -> Input.source -> Path.T
   val check_session_dir: Proof.context -> Path.T option -> Input.source -> Path.T
 end;
 
 structure Resources: RESOURCES =
 struct
 
 (* command timings *)
 
 type timings = ((string * Time.time) Inttab.table) Symtab.table;  (*file -> offset -> name, time*)
 
 val empty_timings: timings = Symtab.empty;
 
 fun update_timings props =
   (case Markup.parse_command_timing_properties props of
     SOME ({file, offset, name}, time) =>
       Symtab.map_default (file, Inttab.empty)
         (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time)))
   | NONE => I);
 
 fun make_timings command_timings =
   fold update_timings command_timings empty_timings;
 
 fun approximative_id name pos =
   (case (Position.file_of pos, Position.offset_of pos) of
     (SOME file, SOME offset) =>
       if name = "" then NONE else SOME {file = file, offset = offset, name = name}
   | _ => NONE);
 
 fun get_timings timings tr =
   (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of
     SOME {file, offset, name} =>
       (case Symtab.lookup timings file of
         SOME offsets =>
           (case Inttab.lookup offsets offset of
             SOME (name', time) => if name = name' then SOME time else NONE
           | NONE => NONE)
       | NONE => NONE)
   | NONE => NONE)
   |> the_default Time.zeroTime;
 
 
 (* session base *)
 
 val default_qualifier = "Draft";
 
 type entry = {pos: Position.T, serial: serial};
 
 fun make_entry props : entry =
   {pos = Position.of_properties props, serial = serial ()};
 
 val empty_session_base =
   ({session_positions = []: (string * entry) list,
     session_directories = Symtab.empty: Path.T list Symtab.table,
     session_chapters = Symtab.empty: string Symtab.table,
     bibtex_entries = Symtab.empty: string list Symtab.table,
     timings = empty_timings,
     scala_functions = Symtab.empty: (bool * Position.T) Symtab.table},
    {global_theories = Symtab.empty: string Symtab.table,
     loaded_theories = Symtab.empty: unit Symtab.table});
 
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
 fun init_session
     {session_positions, session_directories, session_chapters, bibtex_entries,
       command_timings, scala_functions, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
       ({session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
         session_directories =
           fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
             session_directories Symtab.empty,
         session_chapters = Symtab.make session_chapters,
         bibtex_entries = Symtab.make bibtex_entries,
         timings = make_timings command_timings,
         scala_functions = Symtab.make scala_functions},
        {global_theories = Symtab.make global_theories,
         loaded_theories = Symtab.make_set loaded_theories}));
 
 fun init_session_yxml yxml =
   let
     val (session_positions, (session_directories, (session_chapters, (bibtex_entries,
         (command_timings, (scala_functions, (global_theories, loaded_theories))))))) =
       YXML.parse_body yxml |>
         let open XML.Decode in
           (pair (list (pair string properties))
             (pair (list (pair string string)) (pair (list (pair string string))
               (pair (list (pair string (list string))) (pair (list properties)
                 (pair (list (pair string (pair bool properties)))
                   (pair (list (pair string string)) (list string))))))))
         end;
   in
     init_session
       {session_positions = session_positions,
        session_directories = session_directories,
        session_chapters = session_chapters,
        bibtex_entries = bibtex_entries,
        command_timings = command_timings,
        scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions,
        global_theories = global_theories,
        loaded_theories = loaded_theories}
   end;
 
 fun init_session_file path =
   init_session_yxml (File.read path) before File.rm path;
 
 fun finish_session_base () =
   Synchronized.change global_session_base
     (apfst (K (#1 empty_session_base)));
 
 fun get_session_base f = f (Synchronized.value global_session_base);
 fun get_session_base1 f = get_session_base (f o #1);
 fun get_session_base2 f = get_session_base (f o #2);
 
 fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a;
 fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a;
 
 fun check_session ctxt arg =
   Completion.check_item "session"
     (fn (name, {pos, serial}) =>
       Markup.entity Markup.sessionN name
       |> Markup.properties (Position.entity_properties_of false serial pos))
     (get_session_base1 #session_positions) ctxt arg;
 
 fun session_chapter name =
   the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name);
 
 fun last_timing tr = get_timings (get_session_base1 #timings) tr;
 
 
 (* Scala functions *)
 
 (*raw bootstrap environment*)
 fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
 
 (*regular resources*)
 fun scala_function a =
   (a, the_default (false, Position.none) (Symtab.lookup (get_session_base1 #scala_functions) a));
 
 fun check_scala_function ctxt arg =
   let
     val funs = scala_functions () |> sort_strings |> map scala_function;
     val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg;
     val multi =
       (case AList.lookup (op =) funs name of
         SOME (multi, _) => multi
       | NONE => false);
   in (name, multi) end;
 
 val _ = Theory.setup
  (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close>
     (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #>
   ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
     (Args.context -- Scan.lift Parse.embedded_position
       >> (uncurry check_scala_function #> #1 #> ML_Syntax.print_string)) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
       let
         val (name, multi) = check_scala_function ctxt arg;
         val func = if multi then "Scala.function" else "Scala.function1";
       in ML_Syntax.atomic (func ^ " " ^ ML_Syntax.print_string name) end)));
 
 
 (* manage source files *)
 
 type files =
  {master_dir: Path.T,  (*master directory of theory source*)
   imports: (string * Position.T) list,  (*source specification of imports*)
   provided: (Path.T * SHA1.digest) list};  (*source path, digest*)
 
 fun make_files (master_dir, imports, provided): files =
  {master_dir = master_dir, imports = imports, provided = provided};
 
 structure Files = Theory_Data
 (
   type T = files;
   val empty = make_files (Path.current, [], []);
   val extend = I;
   fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) =
     let val provided' = Library.merge (op =) (provided1, provided2)
     in make_files (master_dir, imports, provided') end
 );
 
 fun map_files f =
   Files.map (fn {master_dir, imports, provided} =>
     make_files (f (master_dir, imports, provided)));
 
 
 val master_directory = #master_dir o Files.get;
 val imports_of = #imports o Files.get;
 
 fun begin_theory master_dir {name, imports, keywords} parents =
   Theory.begin_theory name parents
   |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, []))
   |> Thy_Header.add_keywords keywords;
 
 
 (* theory files *)
 
 val thy_path = Path.ext "thy";
 
 fun theory_qualifier theory =
   (case global_theory theory of
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
 fun theory_name qualifier theory =
   if Long_Name.is_qualified theory orelse is_some (global_theory theory)
   then theory
   else Long_Name.qualify qualifier theory;
 
 fun theory_bibtex_entries theory =
   Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory);
 
 fun find_theory_file thy_name =
   let
     val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name));
     val session = theory_qualifier thy_name;
     val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session;
   in
     dirs |> get_first (fn dir =>
       let val path = dir + thy_file
       in if File.is_file path then SOME path else NONE end)
   end;
 
 fun make_theory_node node_name theory =
   {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory};
 
 fun loaded_theory_node theory =
   {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory};
 
 fun import_name qualifier dir s =
   let
     val theory = theory_name qualifier (Thy_Header.import_name s);
     fun theory_node () =
       make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory;
   in
     if not (Thy_Header.is_base_name s) then theory_node ()
     else if loaded_theory theory then loaded_theory_node theory
     else
       (case find_theory_file theory of
         SOME node_name => make_theory_node node_name theory
       | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ())
   end;
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
 fun check_thy dir thy_name =
   let
     val thy_base_name = Long_Name.base_name thy_name;
     val master_file =
       (case find_theory_file thy_name of
         SOME path => check_file Path.current path
       | NONE => check_file dir (thy_path (Path.basic thy_base_name)));
     val text = File.read master_file;
 
     val {name = (name, pos), imports, keywords} =
       Thy_Header.read (Path.position master_file) text;
     val _ =
       thy_base_name <> name andalso
         error ("Bad theory name " ^ quote name ^
           " for file " ^ Path.print (Path.base master_file) ^ Position.here pos);
   in
    {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, keywords = keywords}
   end;
 
 
 (* load files *)
 
 fun parse_files make_paths =
   Scan.ahead Parse.not_eof -- Parse.path_input >> (fn (tok, source) => fn thy =>
     (case Token.get_files tok of
       [] =>
         let
           val master_dir = master_directory thy;
           val name = Input.string_of source;
           val pos = Input.pos_of source;
           val delimited = Input.is_delimited source;
           val src_paths = make_paths (Path.explode name);
         in map (Command.read_file master_dir pos delimited) src_paths end
     | files => map Exn.release files));
 
 val parse_file = parse_files single >> (fn f => f #> the_single);
 
 
 fun provide (src_path, id) =
   map_files (fn (master_dir, imports, provided) =>
     if AList.defined (op =) provided src_path then
       error ("Duplicate use of source file: " ^ Path.print src_path)
     else (master_dir, imports, (src_path, id) :: provided));
 
 fun provide_file (file: Token.file) = provide (#src_path file, #digest file);
 
 fun provide_parse_files make_paths =
   parse_files make_paths >> (fn files => fn thy =>
     let
       val fs = files thy;
       val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy;
     in (fs, thy') end);
 
 val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single);
 
 
 fun load_file thy src_path =
   let
     val full_path = check_file (master_directory thy) src_path;
     val text = File.read full_path;
     val id = SHA1.digest text;
   in ((full_path, id), text) end;
 
 fun loaded_files_current thy =
   #provided (Files.get thy) |>
     forall (fn (src_path, id) =>
       (case try (load_file thy) src_path of
         NONE => false
       | SOME ((_, id'), _) => id = id'));
 
 
 (* formal check *)
 
 fun formal_check check_file ctxt opt_dir source =
   let
     val name = Input.string_of source;
     val pos = Input.pos_of source;
     val delimited = Input.is_delimited source;
 
     val _ = Context_Position.report ctxt pos (Markup.language_path delimited);
 
     fun err msg = error (msg ^ Position.here pos);
     val dir =
       (case opt_dir of
         SOME dir => dir
       | NONE => master_directory (Proof_Context.theory_of ctxt));
     val path = dir + Path.explode name handle ERROR msg => err msg;
     val _ = Path.expand path handle ERROR msg => err msg;
     val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
     val _ : Path.T = check_file path handle ERROR msg => err msg;
   in path end;
 
 val check_path = formal_check I;
 val check_file = formal_check File.check_file;
 val check_dir = formal_check File.check_dir;
 
 fun check_session_dir ctxt opt_dir s =
   let
     val dir = Path.expand (check_dir ctxt opt_dir s);
     val ok =
       File.is_file (dir + Path.explode("ROOT")) orelse
       File.is_file (dir + Path.explode("ROOTS"));
   in
     if ok then dir
     else
       error ("Bad session root directory (missing ROOT or ROOTS): " ^
         Path.print dir ^ Position.here (Input.pos_of s))
   end;
 
 
 (* antiquotations *)
 
 local
 
 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) =>
     check ctxt (SOME Path.current) source |> ML_Syntax.print_path);
 
 in
 
 val _ = Theory.setup
  (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>session\<close>
     (Scan.lift Parse.embedded_position) check_session #>
   Document_Output.antiquotation_raw_embedded \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
   Document_Output.antiquotation_raw_embedded \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
   Document_Output.antiquotation_raw_embedded \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>path\<close> (ML_antiq check_path) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>file\<close> (ML_antiq check_file) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
   ML_Antiquotation.value_embedded \<^binding>\<open>path_binding\<close>
     (Scan.lift (Parse.position Parse.path) >>
       (ML_Syntax.print_path_binding o Path.explode_binding)) #>
   ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
     (Args.theory >> (ML_Syntax.print_path o master_directory)));
 
 end;
 
 end;
diff --git a/src/Pure/System/scala_compiler.ML b/src/Pure/System/scala_compiler.ML
--- a/src/Pure/System/scala_compiler.ML
+++ b/src/Pure/System/scala_compiler.ML
@@ -1,99 +1,99 @@
 (*  Title:      Pure/System/scala_compiler.ML
     Author:     Makarius
 
 Scala compiler operations.
 *)
 
 signature SCALA_COMPILER =
 sig
   val toplevel: bool -> string -> unit
   val static_check: string * Position.T -> unit
 end;
 
 structure Scala_Compiler: SCALA_COMPILER =
 struct
 
 (* check declaration *)
 
 fun toplevel interpret source =
   let val errors =
     (interpret, source)
     |> let open XML.Encode in pair bool string end
     |> YXML.string_of_body
     |> \<^scala>\<open>scala_toplevel\<close>
     |> YXML.parse_body
     |> let open XML.Decode in list string end
   in if null errors then () else error (cat_lines errors) end;
 
 fun static_check (source, pos) =
   toplevel false ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
     handle ERROR msg => error (msg ^ Position.here pos);
 
 
 (* antiquotations *)
 
 local
 
 fun make_list bg en = space_implode "," #> enclose bg en;
 
 fun print_args [] = ""
   | print_args xs = make_list "(" ")" xs;
 
 fun print_types [] = ""
   | print_types Ts = make_list "[" "]" Ts;
 
 fun print_class (c, Ts) = c ^ print_types Ts;
 
 val types =
   Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [];
 
 val class =
   Scan.option
     (Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.name -- types  --| Parse.$$$ ")"));
 
 val arguments =
   (Parse.nat >> (fn n => replicate n "_") ||
     Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args;
 
 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
 
 val _ =
   Theory.setup
     (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala\<close>
       (Scan.lift Args.embedded_position)
       (fn _ => fn (s, pos) => (static_check (s, pos); s)) #>
 
     Document_Output.antiquotation_raw_embedded \<^binding>\<open>scala_type\<close>
       (Scan.lift (Args.embedded_position -- (types >> print_types)))
       (fn _ => fn ((t, pos), type_args) =>
         (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args, pos);
           scala_name (t ^ type_args))) #>
 
     Document_Output.antiquotation_raw_embedded \<^binding>\<open>scala_object\<close>
       (Scan.lift Args.embedded_position)
       (fn _ => fn (x, pos) => (static_check ("val _test_ = " ^ x, pos); scala_name x)) #>
 
     Document_Output.antiquotation_raw_embedded \<^binding>\<open>scala_method\<close>
       (Scan.lift (class -- Args.embedded_position -- types -- args))
       (fn _ => fn (((class_context, (method, pos)), method_types), method_args) =>
         let
           val class_types = (case class_context of SOME (_, Ts) => Ts | NONE => []);
           val def = "def _test_" ^ print_types (merge (op =) (method_types, class_types));
           val def_context =
             (case class_context of
               NONE => def ^ " = "
             | SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_.");
           val source = def_context ^ method ^ method_args;
           val _ = static_check (source, pos);
           val text = (case class_context of NONE => method | SOME c => print_class c ^ "." ^ method);
         in scala_name text end));
 
 end;
 
 end;
diff --git a/src/Pure/Thy/document_antiquotation.ML b/src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML
+++ b/src/Pure/Thy/document_antiquotation.ML
@@ -1,276 +1,276 @@
 (*  Title:      Pure/Thy/document_antiquotation.ML
     Author:     Makarius
 
 Document antiquotations.
 *)
 
 signature DOCUMENT_ANTIQUOTATION =
 sig
   val thy_output_display: bool Config.T
   val thy_output_cartouche: bool Config.T
   val thy_output_quotes: bool Config.T
   val thy_output_margin: int Config.T
   val thy_output_indent: int Config.T
   val thy_output_source: bool Config.T
   val thy_output_source_cartouche: bool Config.T
   val thy_output_break: bool Config.T
   val thy_output_modes: string Config.T
   val trim_blanks: Proof.context -> string -> string
   val trim_lines: Proof.context -> string -> string
   val indent_lines: Proof.context -> string -> string
   val prepare_lines: Proof.context -> string -> string
   val delimit: Proof.context -> Pretty.T -> Pretty.T
   val indent: Proof.context -> Pretty.T -> Pretty.T
   val format: Proof.context -> Pretty.T -> string
   val output: Proof.context -> Pretty.T -> Output.output
   val print_antiquotations: bool -> Proof.context -> unit
   val check: Proof.context -> xstring * Position.T -> string
   val check_option: Proof.context -> xstring * Position.T -> string
   val setup: binding -> 'a context_parser ->
     ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
   val setup_embedded: binding -> 'a context_parser ->
     ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
   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;
 
 structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
 struct
 
 (* options *)
 
 val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
 val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
 val thy_output_cartouche = Attrib.setup_option_bool ("thy_output_cartouche", \<^here>);
 val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
 val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
 val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
 val thy_output_source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
 val thy_output_source_cartouche = Attrib.setup_option_bool ("thy_output_source_cartouche", \<^here>);
 val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
 
 
 (* blanks *)
 
 fun trim_blanks ctxt =
   not (Config.get ctxt thy_output_display) ? Symbol.trim_blanks;
 
 fun trim_lines ctxt =
   if not (Config.get ctxt thy_output_display) then
     split_lines #> map Symbol.trim_blanks #> space_implode " "
   else I;
 
 fun indent_lines ctxt =
   if Config.get ctxt thy_output_display then
     prefix_lines (Symbol.spaces (Config.get ctxt thy_output_indent))
   else I;
 
 fun prepare_lines ctxt = trim_lines ctxt #> indent_lines ctxt;
 
 
 (* output *)
 
 fun delimit ctxt =
   if Config.get ctxt thy_output_cartouche then Pretty.cartouche
   else if Config.get ctxt thy_output_quotes then Pretty.quote
   else I;
 
 fun indent ctxt =
   Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
 
 fun format ctxt =
   if Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break
   then Pretty.string_of_margin (Config.get ctxt thy_output_margin)
   else Pretty.unformatted_string_of;
 
 fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;
 
 
 (* theory data *)
 
 structure Data = Theory_Data
 (
   type T =
     (bool * (Token.src -> Proof.context -> Latex.text)) Name_Space.table *
       (string -> Proof.context -> Proof.context) Name_Space.table;
   val empty : T =
     (Name_Space.empty_table Markup.document_antiquotationN,
       Name_Space.empty_table Markup.document_antiquotation_optionN);
   val extend = I;
   fun merge ((commands1, options1), (commands2, options2)) : T =
     (Name_Space.merge_tables (commands1, commands2),
       Name_Space.merge_tables (options1, options2));
 );
 
 val get_antiquotations = Data.get o Proof_Context.theory_of;
 
 fun print_antiquotations verbose ctxt =
   let
     val (commands, options) = get_antiquotations ctxt;
     val command_names = map #1 (Name_Space.markup_table verbose ctxt commands);
     val option_names = map #1 (Name_Space.markup_table verbose ctxt options);
   in
     [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
      Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
   end |> Pretty.writeln_chunks;
 
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
 
 fun gen_setup name embedded scan body thy =
   let
     fun cmd src ctxt =
       let val (x, ctxt') = Token.syntax scan src ctxt
       in body {context = ctxt', source = src, argument = x} end;
     val entry = (name, (embedded, cmd));
   in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true entry #> #2)) end;
 
 fun setup name = gen_setup name false;
 fun setup_embedded name = gen_setup name true;
 
 fun setup_option name opt thy = thy
   |> Data.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> #2));
 
 
 (* syntax *)
 
 local
 
 val property =
   Parse.name_position -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
 
 val properties =
   Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
 
 in
 
 val parse_antiq =
   Parse.!!!
     (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
   >> (fn ((name, opts), args) => (opts, name :: args));
 
 end;
 
 
 (* evaluate *)
 
 local
 
 fun command pos (opts, src) ctxt =
   let
     val (src', (embedded, scan)) = Token.check_src ctxt (#1 o get_antiquotations) src;
     val _ =
       if null opts andalso Options.default_bool "update_control_cartouches" then
         Context_Position.reports_text ctxt
           (Antiquote.update_reports embedded pos (map Token.content_of src'))
       else ();
   in scan src' ctxt end;
 
 fun option ((xname, pos), s) ctxt =
   let
     val (_, opt) =
       Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   in opt s ctxt end;
 
 fun eval ctxt pos (opts, src) =
   let
     val preview_ctxt = fold option opts (Config.put show_markup false ctxt);
     val _ = command pos (opts, src) preview_ctxt;
 
     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
 
 fun read_antiq ctxt ({range = (pos, _), body, ...}: Antiquote.antiq) =
   let val keywords = Thy_Header.get_keywords' ctxt;
   in Token.read_antiq keywords parse_antiq (body, pos) end;
 
 fun evaluate eval_text ctxt antiq =
   (case antiq of
     Antiquote.Text ss => eval_text ss
   | Antiquote.Control {name, body, ...} =>
       eval ctxt Position.none
         ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
   | Antiquote.Antiq antiq => eval ctxt (#1 (#range antiq)) (read_antiq ctxt antiq));
 
 end;
 
 
 (* approximative content, e.g. for index entries *)
 
 local
 
 val strip_symbols = [Symbol.open_, Symbol.close, "'", "\"", "`"];
 
 fun strip_symbol sym =
   if member (op =) strip_symbols sym then ""
   else
     (case Symbol.decode sym of
       Symbol.Char s => s
     | Symbol.UTF8 s => s
     | Symbol.Sym s => s
     | Symbol.Control s => s
     | _ => "");
 
 fun strip_antiq _ (Antiquote.Text body) = map Symbol_Pos.symbol body
   | strip_antiq _ (Antiquote.Control {body, ...}) = map Symbol_Pos.symbol body
   | strip_antiq ctxt (Antiquote.Antiq antiq) =
       read_antiq ctxt antiq |> #2 |> tl
       |> maps (Symbol.explode o Token.content_of);
 
 in
 
 fun approx_content ctxt =
   Symbol_Pos.explode0
   #> trim (Symbol.is_blank o Symbol_Pos.symbol)
   #> Antiquote.parse_comments Position.none
   #> maps (strip_antiq ctxt)
   #> map strip_symbol
   #> implode;
 
 end;
 
 
 (* option syntax *)
 
 fun boolean "" = true
   | boolean "true" = true
   | boolean "false" = false
   | boolean s = error ("Bad boolean value: " ^ Library.quote s);
 
 fun integer s =
   let
     fun int ss =
       (case Library.read_int ss of (i, []) => i
       | _ => error ("Bad integer value: " ^ Library.quote s));
   in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
 
 val _ = Theory.setup
  (setup_option \<^binding>\<open>show_types\<close> (Config.put show_types o boolean) #>
   setup_option \<^binding>\<open>show_sorts\<close> (Config.put show_sorts o boolean) #>
   setup_option \<^binding>\<open>show_structs\<close> (Config.put show_structs o boolean) #>
   setup_option \<^binding>\<open>show_question_marks\<close> (Config.put show_question_marks o boolean) #>
   setup_option \<^binding>\<open>show_abbrevs\<close> (Config.put show_abbrevs o boolean) #>
   setup_option \<^binding>\<open>names_long\<close> (Config.put Name_Space.names_long o boolean) #>
   setup_option \<^binding>\<open>names_short\<close> (Config.put Name_Space.names_short o boolean) #>
   setup_option \<^binding>\<open>names_unique\<close> (Config.put Name_Space.names_unique o boolean) #>
   setup_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
   setup_option \<^binding>\<open>display\<close> (Config.put thy_output_display o boolean) #>
   setup_option \<^binding>\<open>break\<close> (Config.put thy_output_break o boolean) #>
   setup_option \<^binding>\<open>cartouche\<close> (Config.put thy_output_cartouche o boolean) #>
   setup_option \<^binding>\<open>quotes\<close> (Config.put thy_output_quotes o boolean) #>
   setup_option \<^binding>\<open>mode\<close> (Config.put thy_output_modes) #>
   setup_option \<^binding>\<open>margin\<close> (Config.put thy_output_margin o integer) #>
   setup_option \<^binding>\<open>indent\<close> (Config.put thy_output_indent o integer) #>
   setup_option \<^binding>\<open>source\<close> (Config.put thy_output_source o boolean) #>
   setup_option \<^binding>\<open>source_cartouche\<close> (Config.put thy_output_source_cartouche o boolean) #>
   setup_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
 
 end;
diff --git a/src/Pure/Thy/document_antiquotations.ML b/src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML
+++ b/src/Pure/Thy/document_antiquotations.ML
@@ -1,446 +1,447 @@
 (*  Title:      Pure/Thy/document_antiquotations.ML
     Author:     Makarius
 
 Miscellaneous document antiquotations.
 *)
 
 structure Document_Antiquotations: sig end =
 struct
 
 (* basic entities *)
 
 local
 
 type style = term -> term;
 
 fun pretty_term_style ctxt (style: style, t) =
   Document_Output.pretty_term ctxt (style t);
 
 fun pretty_thms_style ctxt (style: style, ths) =
   map (fn th => Document_Output.pretty_term ctxt (style (Thm.full_prop_of th))) ths;
 
 fun pretty_term_typ ctxt (style: style, t) =
   let val t' = style t
   in Document_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
 
 fun pretty_term_typeof ctxt (style: style, t) =
   Syntax.pretty_typ ctxt (Term.fastype_of (style t));
 
 fun pretty_const ctxt c =
   let
     val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
       handle TYPE (msg, _, _) => error msg;
     val (t', _) = yield_singleton (Variable.import_terms true) t ctxt;
   in Document_Output.pretty_term ctxt t' end;
 
 fun pretty_abbrev ctxt s =
   let
     val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
     fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
     val (head, args) = Term.strip_comb t;
     val (c, T) = Term.dest_Const head handle TERM _ => err ();
     val (U, u) = Consts.the_abbreviation (Proof_Context.consts_of ctxt) c
       handle TYPE _ => err ();
     val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
     val eq = Logic.mk_equals (t, t');
     val ctxt' = Proof_Context.augment eq ctxt;
   in Proof_Context.pretty_term_abbrev ctxt' eq end;
 
 fun pretty_locale ctxt (name, pos) =
   let val thy = Proof_Context.theory_of ctxt
   in Pretty.str (Locale.extern thy (Locale.check thy (name, pos))) end;
 
 fun pretty_class ctxt s =
   Pretty.str (Proof_Context.extern_class ctxt (Proof_Context.read_class ctxt s));
 
 fun pretty_type ctxt s =
   let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
   in Pretty.str (Proof_Context.extern_type ctxt name) end;
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_standard_proof_of ctxt full;
 
 fun pretty_theory ctxt (name, pos) =
   (Theory.check {long = true} ctxt (name, pos); Pretty.str name);
 
 val basic_entity = Document_Output.antiquotation_pretty_source_embedded;
 
 fun basic_entities name scan pretty =
   Document_Antiquotation.setup name scan
     (fn {context = ctxt, source = src, argument = xs} =>
       Document_Output.pretty_items_source ctxt {embedded = false} src (map (pretty ctxt) xs));
 
 val _ = Theory.setup
  (basic_entity \<^binding>\<open>prop\<close> (Term_Style.parse -- Args.prop) pretty_term_style #>
   basic_entity \<^binding>\<open>term\<close> (Term_Style.parse -- Args.term) pretty_term_style #>
   basic_entity \<^binding>\<open>term_type\<close> (Term_Style.parse -- Args.term) pretty_term_typ #>
   basic_entity \<^binding>\<open>typeof\<close> (Term_Style.parse -- Args.term) pretty_term_typeof #>
   basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
   basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
   basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
   basic_entity \<^binding>\<open>locale\<close> (Scan.lift Args.embedded_position) pretty_locale #>
   basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
   basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded_inner_syntax) pretty_type #>
   basic_entity \<^binding>\<open>theory\<close> (Scan.lift Args.embedded_position) pretty_theory #>
   basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
   basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
   Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms)
     (fn {context = ctxt, source = src, argument = arg} =>
       Document_Output.pretty_items_source ctxt {embedded = false} src (pretty_thms_style ctxt arg)));
 
 in end;
 
 
 (* Markdown errors *)
 
 local
 
 fun markdown_error binding =
   Document_Antiquotation.setup binding (Scan.succeed ())
     (fn {source = src, ...} =>
       error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
         Position.here (Position.no_range_position (#1 (Token.range_of src)))))
 
 val _ =
   Theory.setup
    (markdown_error \<^binding>\<open>item\<close> #>
     markdown_error \<^binding>\<open>enum\<close> #>
     markdown_error \<^binding>\<open>descr\<close>);
 
 in end;
 
 
 (* control spacing *)
 
 val _ =
   Theory.setup
    (Document_Output.antiquotation_raw \<^binding>\<open>noindent\<close> (Scan.succeed ())
       (fn _ => fn () => Latex.string "\\noindent") #>
     Document_Output.antiquotation_raw \<^binding>\<open>smallskip\<close> (Scan.succeed ())
       (fn _ => fn () => Latex.string "\\smallskip") #>
     Document_Output.antiquotation_raw \<^binding>\<open>medskip\<close> (Scan.succeed ())
       (fn _ => fn () => Latex.string "\\medskip") #>
     Document_Output.antiquotation_raw \<^binding>\<open>bigskip\<close> (Scan.succeed ())
       (fn _ => fn () => Latex.string "\\bigskip"));
 
 
 (* nested document text *)
 
 local
 
 fun nested_antiquotation name s1 s2 =
   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
    (nested_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #>
     nested_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #>
     nested_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}");
 
 in end;
 
 
 (* index entries *)
 
 local
 
 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)
     (fn ctxt => fn args =>
       let
         val _ = Context_Position.reports ctxt (maps (Document_Output.document_reports o #1) args);
         fun make_item (txt, opt_like) =
           let
             val text = output_text ctxt txt;
             val like =
               (case opt_like of
                 SOME s => s
               | NONE => Document_Antiquotation.approx_content ctxt (Input.string_of txt));
             val _ =
               if is_none opt_like andalso Context_Position.is_visible ctxt then
                 writeln ("(" ^ Markup.markup Markup.keyword2 "is" ^ " " ^ quote like ^ ")" ^
                   Position.here (Input.pos_of txt))
               else ();
           in {text = text, like = like} end;
       in Latex.index_entry {items = map make_item args, def = def} end);
 
 val _ = Theory.setup (index \<^binding>\<open>index_ref\<close> false #> index \<^binding>\<open>index_def\<close> true);
 
 in end;
 
 
 (* quasi-formal text (unchecked) *)
 
 local
 
 fun report_text ctxt text =
   let val pos = Input.pos_of text in
     Context_Position.reports ctxt
       [(pos, Markup.language_text (Input.is_delimited text)),
        (pos, Markup.raw_text)]
   end;
 
 fun prepare_text ctxt =
   Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
 
 fun text_antiquotation name =
   Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let
         val _ = report_text ctxt text;
       in
         prepare_text ctxt text
         |> Document_Output.output_source ctxt
         |> Document_Output.isabelle ctxt
       end);
 
 val theory_text_antiquotation =
   Document_Output.antiquotation_raw_embedded \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let
         val keywords = Thy_Header.get_keywords' ctxt;
 
         val _ = report_text ctxt text;
         val _ =
           Input.source_explode text
           |> Token.tokenize keywords {strict = true}
           |> maps (Token.reports keywords)
           |> Context_Position.reports_text ctxt;
       in
         prepare_text ctxt text
         |> Token.explode0 keywords
         |> maps (Document_Output.output_token ctxt)
         |> Document_Output.isabelle ctxt
       end);
 
 val _ =
   Theory.setup
    (text_antiquotation \<^binding>\<open>text\<close> #>
     text_antiquotation \<^binding>\<open>cartouche\<close> #>
     theory_text_antiquotation);
 
 in end;
 
 
 (* goal state *)
 
 local
 
 fun goal_state name main =
   Document_Output.antiquotation_pretty name (Scan.succeed ())
     (fn ctxt => fn () =>
       Goal_Display.pretty_goal
         (Config.put Goal_Display.show_main_goal main ctxt)
         (#goal (Proof.goal (Toplevel.proof_of (Toplevel.presentation_state ctxt)))));
 
 val _ = Theory.setup
  (goal_state \<^binding>\<open>goals\<close> true #>
   goal_state \<^binding>\<open>subgoals\<close> false);
 
 in end;
 
 
 (* embedded lemma *)
 
 val _ = Theory.setup
   (Document_Antiquotation.setup \<^binding>\<open>lemma\<close>
     (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop --
       Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse))
     (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} =>
       let
         val reports =
           (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
             maps Method.reports_of (m1 :: the_list m2);
         val _ = Context_Position.reports ctxt reports;
 
         (* FIXME check proof!? *)
         val _ = ctxt
           |> Proof.theorem NONE (K I) [[(prop, [])]]
           |> Proof.global_terminal_proof (m1, m2);
       in
         Document_Output.pretty_source ctxt {embedded = false}
           [hd src, prop_tok] (Document_Output.pretty_term ctxt prop)
       end));
 
 
 (* verbatim text *)
 
 val _ = Theory.setup
   (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let
         val pos = Input.pos_of text;
         val _ =
           Context_Position.reports ctxt
             [(pos, Markup.language_verbatim (Input.is_delimited text)),
              (pos, Markup.raw_text)];
       in #1 (Input.source_content text) end));
 
 
 (* bash functions *)
 
 val _ = Theory.setup
   (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>bash_function\<close>
     (Scan.lift Args.embedded_position) Isabelle_System.check_bash_function);
 
 
 (* system options *)
 
 val _ = Theory.setup
   (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>system_option\<close>
     (Scan.lift Args.embedded_position)
     (fn ctxt => fn (name, pos) =>
       let val _ = Completion.check_option (Options.default ()) ctxt (name, pos);
       in name end));
 
 
 (* ML text *)
 
 local
 
 fun test_val (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read ");"
   | test_val (ml1, ml2) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read ");";
 
 fun test_op (ml1, ml2) = test_val (ML_Lex.read "op " @ ml1, ml2);
 
 fun test_type (ml1, []) = ML_Lex.read "val _ = NONE : (" @ ml1 @ ML_Lex.read ") option;"
   | test_type (ml1, ml2) =
       ML_Lex.read "val _ = [NONE : (" @ ml1 @ ML_Lex.read ") option, NONE : (" @
       ml2 @ ML_Lex.read ") option];";
 
 fun test_exn (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : exn);"
   | test_exn (ml1, ml2) =
       ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read " -> exn);";
 
 fun test_struct (ml, _) =
   ML_Lex.read "functor XXX() = struct structure XX = " @ ml @ ML_Lex.read " end;";
 
 fun test_functor (Antiquote.Text tok :: _, _) =
       ML_Lex.read "ML_Env.check_functor " @
       ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
   | test_functor _ = raise Fail "Bad ML functor specification";
 
 val parse_ml0 = Args.text_input >> (fn source => ("", (source, Input.empty)));
 
 val parse_ml =
   Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty >> pair "";
 
 val parse_exn =
   Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty >> pair "";
 
 val parse_type =
   (Parse.type_args >> (fn [] => "" | [a] => a ^ " " | bs => enclose "(" ") " (commas bs))) --
     (Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty);
 
 fun eval ctxt pos ml =
   ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos ml
     handle ERROR msg => error (msg ^ Position.here pos);
 
 fun make_text sep sources =
   let
     val (txt1, txt2) = apply2 (#1 o Input.source_content) sources;
     val is_ident =
       (case try List.last (Symbol.explode txt1) of
         NONE => false
       | SOME s => Symbol.is_ascii_letdig s);
     val txt =
       if txt2 = "" then txt1
       else if sep = ":" andalso is_ident then txt1 ^ ": " ^ txt2
       else txt1 ^ " " ^ sep ^ " " ^ txt2
   in (txt, txt1) end;
 
 fun antiquotation_ml parse test kind show_kind binding index =
   Document_Output.antiquotation_raw binding (Scan.lift parse)
     (fn ctxt => fn (txt0, sources) =>
       let
         val (ml1, ml2) = apply2 ML_Lex.read_source sources;
         val ml0 = ML_Lex.read_source (Input.string txt0);
         val _ = test (ml0 @ ml1, ml2) |> eval ctxt (Input.pos_of (#1 sources));
 
         val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":";
         val (txt, idx) = make_text sep sources;
 
         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;
 
 fun antiquotation_ml1 parse test kind binding =
   antiquotation_ml parse test kind true binding (SOME true);
 
 in
 
 val _ =
   Theory.setup
    (Latex.index_variants (antiquotation_ml0 test_val "") \<^binding>\<open>ML\<close> #>
     Latex.index_variants (antiquotation_ml0 test_op "infix") \<^binding>\<open>ML_infix\<close> #>
     Latex.index_variants (antiquotation_ml0 test_type "type") \<^binding>\<open>ML_type\<close> #>
     Latex.index_variants (antiquotation_ml0 test_struct "structure") \<^binding>\<open>ML_structure\<close> #>
     Latex.index_variants (antiquotation_ml0 test_functor "functor") \<^binding>\<open>ML_functor\<close> #>
     antiquotation_ml0 (K []) "text" \<^binding>\<open>ML_text\<close> NONE #>
     antiquotation_ml1 parse_ml test_val "" \<^binding>\<open>define_ML\<close> #>
     antiquotation_ml1 parse_ml test_op "infix" \<^binding>\<open>define_ML_infix\<close> #>
     antiquotation_ml1 parse_type test_type "type" \<^binding>\<open>define_ML_type\<close> #>
     antiquotation_ml1 parse_exn test_exn "exception" \<^binding>\<open>define_ML_exception\<close> #>
     antiquotation_ml1 parse_ml0 test_struct "structure" \<^binding>\<open>define_ML_structure\<close> #>
     antiquotation_ml1 parse_ml0 test_functor "functor" \<^binding>\<open>define_ML_functor\<close>);
 
 end;
 
 
 (* URLs *)
 
 val escape_url =
   translate_string (fn c => if c = "%" orelse c = "#" orelse c = "^" then "\\" ^ c else c);
 
 val _ = Theory.setup
   (Document_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_input)
     (fn ctxt => fn source =>
       let
         val url = Input.string_of source;
         val pos = Input.pos_of source;
         val delimited = Input.is_delimited source;
         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 *)
 
 local
 
 fun entity_antiquotation name check bg en =
   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
    (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;
 
 end;
diff --git a/src/Pure/Thy/document_build.scala b/src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala
+++ b/src/Pure/Thy/document_build.scala
@@ -1,548 +1,549 @@
 /*  Title:      Pure/Thy/document_build.scala
     Author:     Makarius
 
 Build theory document (PDF) from session database.
 */
 
 package isabelle
 
 
 object Document_Build
 {
   /* document variants */
 
   object Content
   {
     def apply(path: Path, content: Bytes): Content = new Content_Bytes(path, content)
     def apply(path: Path, content: String): Content = new Content_String(path, content)
   }
   trait Content
   {
     def write(dir: Path): Unit
   }
   final class Content_Bytes private[Document_Build](path: Path, content: Bytes) extends Content
   {
     def write(dir: Path): Unit = Bytes.write(dir + path, content)
   }
   final class Content_String private[Document_Build](path: Path, content: String) extends Content
   {
     def write(dir: Path): Unit = File.write(dir + path, content)
   }
 
   abstract class Document_Name
   {
     def name: String
     def path: Path = Path.basic(name)
 
     override def toString: String = name
   }
 
   object Document_Variant
   {
     def parse(name: String, tags: String): Document_Variant =
       Document_Variant(name, Library.space_explode(',', tags))
 
     def parse(opt: String): Document_Variant =
       Library.space_explode('=', opt) match {
         case List(name) => Document_Variant(name, Nil)
         case List(name, tags) => parse(name, tags)
         case _ => error("Malformed document variant: " + quote(opt))
       }
   }
 
   sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name
   {
     def print_tags: String = tags.mkString(",")
     def print: String = if (tags.isEmpty) name else name + "=" + print_tags
 
     def isabelletags: Content =
     {
       val path = Path.explode("isabelletags.sty")
       val content =
         Library.terminate_lines(
           tags.map(tag =>
             tag.toList match {
               case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
               case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
               case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
               case cs => "\\isakeeptag{" + cs.mkString + "}"
             }))
       Content(path, content)
     }
   }
 
   sealed case class Document_Input(name: String, sources: SHA1.Digest)
     extends Document_Name
 
   sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
     extends Document_Name
   {
     def log: String = log_xz.uncompress().text
     def log_lines: List[String] = split_lines(log)
 
     def write(db: SQL.Database, session_name: String): Unit =
       write_document(db, session_name, this)
 
     def write(dir: Path): Path =
     {
       val path = dir + Path.basic(name).pdf
       Isabelle_System.make_directory(path.expand.dir)
       Bytes.write(path, pdf)
       path
     }
   }
 
 
   /* SQL data model */
 
   object Data
   {
     val session_name = SQL.Column.string("session_name").make_primary_key
     val name = SQL.Column.string("name").make_primary_key
     val sources = SQL.Column.string("sources")
     val log_xz = SQL.Column.bytes("log_xz")
     val pdf = SQL.Column.bytes("pdf")
 
     val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
       "WHERE " + Data.session_name.equal(session_name) +
         (if (name == "") "" else " AND " + Data.name.equal(name))
   }
 
   def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
   {
     val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name))
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res =>
       {
         val name = res.string(Data.name)
         val sources = res.string(Data.sources)
         Document_Input(name, SHA1.fake(sources))
       }).toList)
   }
 
   def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
   {
     val select = Data.table.select(sql = Data.where_equal(session_name, name))
     db.using_statement(select)(stmt =>
     {
       val res = stmt.execute_query()
       if (res.next()) {
         val name = res.string(Data.name)
         val sources = res.string(Data.sources)
         val log_xz = res.bytes(Data.log_xz)
         val pdf = res.bytes(Data.pdf)
         Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf))
       }
       else None
     })
   }
 
   def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit =
   {
     db.using_statement(Data.table.insert())(stmt =>
     {
       stmt.string(1) = session_name
       stmt.string(2) = doc.name
       stmt.string(3) = doc.sources.toString
       stmt.bytes(4) = doc.log_xz
       stmt.bytes(5) = doc.pdf
       stmt.execute()
     })
   }
 
 
   /* context */
 
   val isabelle_styles: List[Path] =
     List("comment.sty", "isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
       map(name => Path.explode("~~/lib/texinputs") + Path.basic(name))
 
   def context(
     session: String,
     deps: Sessions.Deps,
     db_context: Sessions.Database_Context,
     progress: Progress = new Progress): Context =
   {
     val info = deps.sessions_structure(session)
     val base = deps(session)
     val hierarchy = deps.sessions_structure.hierarchy(session)
     new Context(info, base, hierarchy, db_context, progress)
   }
 
   final class Context private[Document_Build](
     info: Sessions.Info,
     base: Sessions.Base,
     hierarchy: List[String],
     db_context: Sessions.Database_Context,
     val progress: Progress = new Progress)
   {
     /* session info */
 
     def session: String = info.name
     def options: Options = info.options
 
     def document_bibliography: Boolean = options.bool("document_bibliography")
 
     def document_preprocessor: Option[String] =
       proper_string(options.string("document_preprocessor"))
 
     def document_logo: Option[String] =
       options.string("document_logo") match {
         case "" => None
         case "_" => Some("")
         case name => Some(name)
       }
 
     def document_build: String = options.string("document_build")
 
     def get_engine(): Engine =
     {
       val name = document_build
       engines.find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
     }
 
     def get_export(theory: String, name: String): Export.Entry =
       db_context.get_export(hierarchy, theory, name)
 
 
     /* document content */
 
     def documents: List[Document_Variant] = info.documents
 
     def session_theories: List[Document.Node.Name] = base.session_theories
     def document_theories: List[Document.Node.Name] = session_theories ::: base.document_theories
 
     lazy val tex_files: List[Content] =
       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)
       }
 
     lazy val session_graph: Content =
     {
       val path = Presentation.session_graph_path
       val content = graphview.Graph_File.make_pdf(options, base.session_graph_display)
       Content(path, content)
     }
 
     lazy val session_tex: Content =
     {
       val path = Path.basic("session.tex")
       val content =
         Library.terminate_lines(
           base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))
       Content(path, content)
     }
 
     lazy val isabelle_logo: Option[Content] =
     {
       document_logo.map(logo_name =>
         Isabelle_System.with_tmp_file("logo", ext = "pdf")(tmp_path =>
         {
           Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
           val path = Path.basic("isabelle_logo.pdf")
           val content = Bytes.read(tmp_path)
           Content(path, content)
         }))
     }
 
 
     /* document directory */
 
     def prepare_directory(dir: Path, doc: Document_Variant): Directory =
     {
       val doc_dir = dir + Path.basic(doc.name)
       Isabelle_System.make_directory(doc_dir)
 
 
       /* sources */
 
       isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir))
       doc.isabelletags.write(doc_dir)
 
       for ((base_dir, src) <- info.document_files) {
         Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir)
       }
 
       session_tex.write(doc_dir)
       tex_files.foreach(_.write(doc_dir))
 
       val root_name1 = "root_" + doc.name
       val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
 
       for (name <- document_preprocessor) {
         def message(s: String): String = s + " for document_preprocessor=" + quote(name)
         val path = doc_dir + Path.explode(name)
         if (path.is_file) {
           try { Isabelle_System.bash(File.bash_path(path), cwd = doc_dir.file).check }
           catch { case ERROR(msg) => cat_error(msg, message("The error(s) above occurred")) }
         }
         else error(message("Missing executable"))
       }
 
       val digests1 = List(doc.print, document_logo.toString, document_build).map(SHA1.digest)
       val digests2 = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
       val sources = SHA1.digest_set(digests1 ::: digests2)
 
 
       /* derived material (without SHA1 digest) */
 
       isabelle_logo.foreach(_.write(doc_dir))
 
       session_graph.write(doc_dir)
 
       Directory(doc_dir, doc, root_name, sources)
     }
 
     def old_document(directory: Directory): Option[Document_Output] =
       for {
         old_doc <- db_context.input_database(session)(read_document(_, _, directory.doc.name))
         if old_doc.sources == directory.sources
       }
       yield old_doc
   }
 
   sealed case class Directory(
     doc_dir: Path,
     doc: Document_Variant,
     root_name: String,
     sources: SHA1.Digest)
   {
     def root_name_script(ext: String = ""): String =
       Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext)
 
     def conditional_script(ext: String, exe: String, after: String = ""): String =
       "if [ -f " + root_name_script(ext) + " ]\n" +
       "then\n" +
       "  " + exe + " " + root_name_script() + "\n" +
       (if (after.isEmpty) "" else "  " + after) +
       "fi\n"
 
     def log_errors(): List[String] =
       Latex.latex_errors(doc_dir, root_name) :::
       Bibtex.bibtex_errors(doc_dir, root_name)
 
     def make_document(log: List[String], errors: List[String]): Document_Output =
     {
       val root_pdf = Path.basic(root_name).pdf
       val result_pdf = doc_dir + root_pdf
 
       if (errors.nonEmpty) {
         val errors1 = errors ::: List("Failed to build document " + quote(doc.name))
         throw new Build_Error(log, Exn.cat_message(errors1: _*))
       }
       else if (!result_pdf.is_file) {
         val message = "Bad document result: expected to find " + root_pdf
         throw new Build_Error(log, message)
       }
       else {
         val log_xz = Bytes(cat_lines(log)).compress()
         val pdf = Bytes.read(result_pdf)
         Document_Output(doc.name, sources, log_xz, pdf)
       }
     }
   }
 
 
   /* build engines */
 
   lazy val engines: List[Engine] = Isabelle_System.make_services(classOf[Engine])
 
   abstract class Engine(val name: String) extends Isabelle_System.Service
   {
     override def toString: String = name
 
     def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory
     def build_document(context: Context, directory: Directory, verbose: Boolean): Document_Output
   }
 
   abstract class Bash_Engine(name: String) extends Engine(name)
   {
     def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory =
       context.prepare_directory(dir, doc)
 
     def use_pdflatex: Boolean = false
     def latex_script(context: Context, directory: Directory): String =
       (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
         " " + directory.root_name_script() + "\n"
 
     def bibtex_script(context: Context, directory: Directory, latex: Boolean = false): String =
     {
       val ext = if (context.document_bibliography) "aux" else "bib"
       directory.conditional_script(ext, "$ISABELLE_BIBTEX",
         after = if (latex) latex_script(context, directory) else "")
     }
 
     def makeindex_script(context: Context, directory: Directory, latex: Boolean = false): String =
       directory.conditional_script("idx", "$ISABELLE_MAKEINDEX",
         after = if (latex) latex_script(context, directory) else "")
 
     def use_build_script: Boolean = false
     def build_script(context: Context, directory: Directory): String =
     {
       val has_build_script = (directory.doc_dir + Path.explode("build")).is_file
 
       if (!use_build_script && has_build_script) {
         error("Unexpected document build script for option document_build=" +
           quote(context.document_build))
       }
       else if (use_build_script && !has_build_script) error("Missing document build script")
       else if (has_build_script) "./build pdf " + Bash.string(directory.doc.name)
       else {
         "set -e\n" +
         latex_script(context, directory) +
         bibtex_script(context, directory, latex = true) +
         makeindex_script(context, directory) +
         latex_script(context, directory) +
         makeindex_script(context, directory, latex = true)
       }
     }
 
     def build_document(context: Context, directory: Directory, verbose: Boolean): Document_Output =
     {
       val result =
         context.progress.bash(
           build_script(context, directory),
           cwd = directory.doc_dir.file,
           echo = verbose,
           watchdog = Time.seconds(0.5))
 
       val log = result.out_lines ::: result.err_lines
       val errors = (if (result.ok) Nil else List(result.err)) ::: directory.log_errors()
       directory.make_document(log, errors)
     }
   }
 
   class LuaLaTeX_Engine extends Bash_Engine("lualatex")
   class PDFLaTeX_Engine extends Bash_Engine("pdflatex") { override def use_pdflatex: Boolean = true }
   class Build_Engine extends Bash_Engine("build") { override def use_build_script: Boolean = true }
 
 
   /* build documents */
 
   def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex"
   def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name)
 
   class Build_Error(val log_lines: List[String], val message: String)
     extends Exn.User_Error(message)
 
   def build_documents(
     context: Context,
     output_sources: Option[Path] = None,
     output_pdf: Option[Path] = None,
     verbose: Boolean = false): List[Document_Output] =
   {
     val progress = context.progress
     val engine = context.get_engine()
 
     val documents =
       for (doc <- context.documents)
       yield {
         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
         {
           progress.echo("Preparing " + context.session + "/" + doc.name + " ...")
           val start = Time.now()
 
           output_sources.foreach(engine.prepare_directory(context, _, doc))
           val directory = engine.prepare_directory(context, tmp_dir, doc)
 
           val document =
             context.old_document(directory) getOrElse
               engine.build_document(context, directory, verbose)
 
           val stop = Time.now()
           val timing = stop - start
 
           progress.echo("Finished " + context.session + "/" + doc.name +
             " (" + timing.message_hms + " elapsed time)")
 
           document
         })
       }
 
     for (dir <- output_pdf; doc <- documents) {
       val path = doc.write(dir)
       progress.echo("Document at " + path.absolute)
     }
 
     documents
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args =>
     {
       var output_sources: Option[Path] = None
       var output_pdf: Option[Path] = None
       var verbose_latex = false
       var dirs: List[Path] = Nil
       var options = Options.init()
       var verbose_build = false
 
       val getopts = Getopts(
         """
 Usage: isabelle document [OPTIONS] SESSION
 
   Options are:
     -O DIR       output directory for LaTeX sources and resulting PDF
     -P DIR       output directory for resulting PDF
     -S DIR       output directory for LaTeX sources
     -V           verbose latex
     -d DIR       include session directory
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -v           verbose build
 
   Prepare the theory document of a session.
 """,
         "O:" -> (arg =>
           {
             val dir = Path.explode(arg)
             output_sources = Some(dir)
             output_pdf = Some(dir)
           }),
         "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }),
         "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }),
         "V" -> (_ => verbose_latex = true),
         "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
         "o:" -> (arg => options = options + arg),
         "v" -> (_ => verbose_build = true))
 
       val more_args = getopts(args)
       val session =
         more_args match {
           case List(a) => a
           case _ => getopts.usage()
         }
 
       val progress = new Console_Progress(verbose = verbose_build)
       val store = Sessions.store(options)
 
       progress.interrupt_handler {
         val res =
           Build.build(options, selection = Sessions.Selection.session(session),
             dirs = dirs, progress = progress, verbose = verbose_build)
         if (!res.ok) error("Failed to build session " + quote(session))
 
         val deps =
           Sessions.load_structure(options + "document=pdf", dirs = dirs).
             selection_deps(Sessions.Selection.session(session))
 
         if (output_sources.isEmpty && output_pdf.isEmpty) {
           progress.echo_warning("No output directory")
         }
 
         using(store.open_database_context())(db_context =>
         {
           build_documents(context(session, deps, db_context, progress = progress),
             output_sources = output_sources, output_pdf = output_pdf,
             verbose = verbose_latex)
         })
       }
     })
 }
diff --git a/src/Pure/Thy/document_output.ML b/src/Pure/Thy/document_output.ML
--- a/src/Pure/Thy/document_output.ML
+++ b/src/Pure/Thy/document_output.ML
@@ -1,577 +1,572 @@
 (*  Title:      Pure/Thy/document_output.ML
     Author:     Makarius
 
 Theory document output.
 *)
 
 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
   val pretty: Proof.context -> Pretty.T -> Latex.text
   val pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text
   val pretty_items: Proof.context -> Pretty.T list -> Latex.text
   val pretty_items_source: Proof.context -> {embedded: bool} -> Token.src ->
     Pretty.T list -> Latex.text
   val antiquotation_pretty:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_embedded:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_source:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_source_embedded:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_raw:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   val antiquotation_raw_embedded:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   val antiquotation_verbatim:
     binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
   val antiquotation_verbatim_embedded:
     binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
 end;
 
 structure Document_Output: DOCUMENT_OUTPUT =
 struct
 
 (* output document source *)
 
 fun document_reports txt =
   let val pos = Input.pos_of txt in
     [(pos, Markup.language_document (Input.is_delimited txt)),
      (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 =
   let
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
 
     val output_antiquotes =
       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
     then
       let
         val ants = Antiquote.parse_comments pos syms;
         val reports = Antiquote.antiq_reports ants;
         val blocks = Markdown.read_antiquotes ants;
         val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks);
       in output_blocks blocks end
     else
       let
         val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
         val reports = Antiquote.antiq_reports ants;
         val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants);
       in output_antiquotes ants end
   end;
 
 
 (* output tokens with formal comments *)
 
 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
   | (SOME comment, _) => output_comment ctxt (comment, syms));
 
 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
 
 fun output_token ctxt tok =
   let
     fun output antiq bg en =
       output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
   in
     (case Token.kind_of tok of
       Token.Comment NONE => []
     | Token.Comment (SOME Comment.Marker) => []
     | Token.Command => output false "\\isacommand{" "}"
     | Token.Keyword =>
         if Symbol.is_ascii_identifier (Token.content_of tok)
         then output false "\\isakeyword{" "}"
         else output false "" ""
     | Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}"
     | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
     | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
     | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
     | _ => output false "" "")
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
 fun output_source ctxt s =
   output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none));
 
 fun check_comments ctxt =
   Comment.read_body #> List.app (fn (comment, syms) =>
     let
       val pos = #1 (Symbol_Pos.range syms);
       val _ =
         comment |> Option.app (fn kind =>
           Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups kind)));
       val _ = output_comment_symbols ctxt {antiq = false} (comment, syms);
     in if comment = SOME Comment.Comment then check_comments ctxt syms else () end);
 
 end;
 
 
 
 (** present theory source **)
 
 (* presentation tokens *)
 
 datatype token =
     Ignore
   | Token of Token.T
   | Heading of string * Input.source
   | Body of string * Input.source
   | Raw of Input.source;
 
 fun token_with pred (Token tok) = pred tok
   | token_with _ _ = false;
 
 val white_token = token_with Document_Source.is_white;
 val white_comment_token = token_with Document_Source.is_white_comment;
 val blank_token = token_with Token.is_blank;
 val newline_token = token_with Token.is_newline;
 
 fun present_token ctxt tok =
   (case tok of
     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 *)
 
 type command = string * Position.T;   (*name, position*)
 type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
 
 datatype span = Span of command * (source * source * source * source) * bool;
 
 fun make_span cmd src =
   let
     fun chop_newline (tok :: toks) =
           if newline_token (fst tok) then ([tok], toks, true)
           else ([], tok :: toks, false)
       | chop_newline [] = ([], [], false);
     val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
       src
       |> chop_prefix (white_token o fst)
       ||>> chop_suffix (white_token o fst)
       ||>> chop_prefix (white_comment_token o fst)
       ||> chop_newline;
   in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
 
 
 (* present spans *)
 
 local
 
 fun err_bad_nesting here =
   error ("Bad nesting of commands in presentation" ^ here);
 
 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;
 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;
 
 fun document_tag cmd_pos state state' tagging_stack =
   let
     val ctxt' = Toplevel.presentation_context state';
     val nesting = Toplevel.level state' - Toplevel.level state;
 
     val (tagging, taggings) = tagging_stack;
     val (tag', tagging') = Document_Source.update_tagging ctxt' tagging;
 
     val tagging_stack' =
       if nesting = 0 andalso not (Toplevel.is_proof state) then tagging_stack
       else if nesting >= 0 then (tagging', replicate nesting tagging @ taggings)
       else
         (case drop (~ nesting - 1) taggings of
           tg :: tgs => (tg, tgs)
         | [] => err_bad_nesting (Position.here cmd_pos));
   in (tag', tagging_stack') end;
 
 fun read_tag s =
   (case space_explode "%" s of
     ["", b] => (SOME b, NONE)
   | [a, b] => (NONE, SOME (a, b))
   | _ => error ("Bad document_tags specification: " ^ quote s));
 
 in
 
 fun make_command_tag options keywords =
   let
     val document_tags =
       map read_tag (space_explode "," (Options.string options \<^system_option>\<open>document_tags\<close>));
     val document_tags_default = map_filter #1 document_tags;
     val document_tags_command = map_filter #2 document_tags;
   in
     fn cmd_name => fn state => fn state' => fn active_tag =>
       let
         val keyword_tags =
           if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
           else Keyword.command_tags keywords cmd_name;
         val command_tags =
           the_list (AList.lookup (op =) document_tags_command cmd_name) @
           keyword_tags @ document_tags_default;
         val active_tag' =
           (case command_tags of
             default_tag :: _ => SOME default_tag
           | [] =>
               if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
               then active_tag
               else NONE);
       in active_tag' end
   end;
 
 fun present_span command_tag span state state'
     (tagging_stack, active_tag, newline, latex, present_cont) =
   let
     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;
 
     val (tag', tagging_stack') = document_tag cmd_pos state state' tagging_stack;
     val active_tag' =
       if is_some tag' then Option.map #1 tag'
       else command_tag cmd_name state state' active_tag;
     val edge = (active_tag, active_tag');
 
     val newline' =
       if is_none active_tag' then span_newline else newline;
 
     val latex' =
       latex
       |> end_tag edge
       |> close_delim (fst present_cont) edge
       |> snd present_cont
       |> open_delim (present (#1 srcs)) edge
       |> begin_tag edge
       |> present (#2 srcs);
     val present_cont' =
       if newline then (present (#3 srcs), present (#4 srcs))
       else (I, present (#3 srcs) #> present (#4 srcs));
   in (tagging_stack', active_tag', newline', latex', present_cont') end;
 
 fun present_trailer ((_, tags), active_tag, _, latex, present_cont) =
   if not (null tags) then err_bad_nesting " at end of theory"
   else
     latex
     |> end_tag (active_tag, NONE)
     |> close_delim (fst present_cont) (active_tag, NONE)
     |> snd present_cont;
 
 end;
 
 
 (* present_thy *)
 
 local
 
 val markup_true = "\\isamarkuptrue%\n";
 val markup_false = "\\isamarkupfalse%\n";
 
 val opt_newline = Scan.option (Scan.one Token.is_newline);
 
 val ignore =
   Scan.depend (fn d => opt_newline |-- Scan.one Token.is_begin_ignore
     >> pair (d + 1)) ||
   Scan.depend (fn d => Scan.one Token.is_end_ignore --|
     (if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of meta-comments")) else opt_newline)
     >> pair (d - 1));
 
 val locale =
   Scan.option ((Parse.$$$ "(" -- Document_Source.improper -- Parse.$$$ "in") |--
     Parse.!!!
       (Document_Source.improper |-- Parse.name --| (Document_Source.improper -- Parse.$$$ ")")));
 
 in
 
 type segment =
   {span: Command_Span.span, command: Toplevel.transition,
    prev_state: Toplevel.state, state: Toplevel.state};
 
 fun present_thy options thy (segments: segment list) =
   let
     val keywords = Thy_Header.get_keywords thy;
 
 
     (* tokens *)
 
     val ignored = Scan.state --| ignore
       >> (fn d => (NONE, (Ignore, ("", d))));
 
     fun markup pred mk flag = Scan.peek (fn d =>
       Document_Source.improper |--
         Parse.position (Scan.one (fn tok =>
           Token.is_command tok andalso pred keywords (Token.content_of tok))) --
       (Document_Source.annotation |--
         Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
           Parse.document_source --| Document_Source.improper_end))
             >> (fn ((tok, pos'), source) =>
               let val name = Token.content_of tok
               in (SOME (name, pos'), (mk (name, source), (flag, d))) end));
 
     val command = Scan.peek (fn d =>
       Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
       Scan.one Token.is_command --| Document_Source.annotation
       >> (fn (cmd_mod, cmd) =>
         map (fn tok => (NONE, (Token tok, ("", d)))) cmd_mod @
           [(SOME (Token.content_of cmd, Token.pos_of cmd),
             (Token cmd, (markup_false, d)))]));
 
     val cmt = Scan.peek (fn d =>
       Scan.one Document_Source.is_black_comment >> (fn tok => (NONE, (Token tok, ("", d)))));
 
     val other = Scan.peek (fn d =>
        Parse.not_eof >> (fn tok => (NONE, (Token tok, ("", d)))));
 
     val tokens =
       (ignored ||
         markup Keyword.is_document_heading Heading markup_true ||
         markup Keyword.is_document_body Body markup_true ||
         markup Keyword.is_document_raw (Raw o #2) "") >> single ||
       command ||
       (cmt || other) >> single;
 
 
     (* spans *)
 
     val is_eof = fn (_, (Token x, _)) => Token.is_eof x | _ => false;
     val stopper = Scan.stopper (K (NONE, (Token Token.eof, ("", 0)))) is_eof;
 
     val cmd = Scan.one (is_some o fst);
     val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
 
     val white_comments = Scan.many (white_comment_token o fst o snd);
     val blank = Scan.one (blank_token o fst o snd);
     val newline = Scan.one (newline_token o fst o snd);
     val before_cmd =
       Scan.option (newline -- white_comments) --
       Scan.option (newline -- white_comments) --
       Scan.option (blank -- white_comments) -- cmd;
 
     val span =
       Scan.repeat non_cmd -- cmd --
         Scan.repeat (Scan.unless before_cmd non_cmd) --
         Scan.option (newline >> (single o snd))
       >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
 
     val spans = segments
       |> maps (Command_Span.content o #span)
       |> drop_suffix Token.is_space
       |> Source.of_list
       |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))
       |> Source.source stopper (Scan.error (Scan.bulk span))
       |> Source.exhaust;
 
     val command_results =
       segments |> map_filter (fn {command, state, ...} =>
         if Toplevel.is_ignored command then NONE else SOME (command, state));
 
 
     (* present commands *)
 
     val command_tag = make_command_tag options keywords;
 
     fun present_command tr span st st' =
       Toplevel.setmp_thread_position tr (present_span command_tag span st st');
 
     fun present _ [] = I
       | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
   in
     if length command_results = length spans then
       (([], []), NONE, true, [], (I, I))
       |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
       |> present_trailer
       |> rev
     else error "Messed-up outer syntax for presentation"
   end;
 
 end;
 
 
 
 (** standard output operations **)
 
 (* pretty printing *)
 
 fun pretty_term ctxt t =
   Syntax.pretty_term (Proof_Context.augment t ctxt) t;
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
 
 (* 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
     not (Config.get ctxt Document_Antiquotation.thy_output_source_cartouche)
   then Token.content_of tok
   else Token.unparse tok;
 
 fun is_source ctxt =
   Config.get ctxt Document_Antiquotation.thy_output_source orelse
   Config.get ctxt Document_Antiquotation.thy_output_source_cartouche;
 
 fun source ctxt embedded =
   Token.args_of_src
   #> map (token_source ctxt embedded #> Document_Antiquotation.prepare_lines ctxt)
   #> space_implode " "
   #> output_source ctxt
   #> 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;
 
 
 (* antiquotation variants *)
 
 local
 
 fun gen_setup name embedded =
   if embedded
   then Document_Antiquotation.setup_embedded name
   else Document_Antiquotation.setup name;
 
 fun gen_antiquotation_pretty name embedded scan f =
   gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
 
 fun gen_antiquotation_pretty_source name embedded scan f =
   gen_setup name embedded scan
     (fn {context = ctxt, source = src, argument = x} =>
       pretty_source ctxt {embedded = embedded} src (f ctxt x));
 
 fun gen_antiquotation_raw name embedded scan f =
   gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
 
 fun gen_antiquotation_verbatim name embedded scan f =
   gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
 
 in
 
 fun antiquotation_pretty name = gen_antiquotation_pretty name false;
 fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
 
 fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
 fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
 
 fun antiquotation_raw name = gen_antiquotation_raw name false;
 fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
 
 fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
 fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
 
 end;
 
 end;
diff --git a/src/Pure/Thy/latex.ML b/src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML
+++ b/src/Pure/Thy/latex.ML
@@ -1,307 +1,277 @@
 (*  Title:      Pure/Thy/latex.ML
     Author:     Makarius
 
 LaTeX output of theory sources.
 *)
 
 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
   val output_symbols: Symbol.symbol list -> string
   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_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}
   type index_entry = {items: index_item list, def: bool}
   val index_entry: index_entry -> text
   val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
   val latexN: string
   val latex_output: string -> string * int
   val latex_markup: string * Properties.T -> Markup.output
   val latex_indent: string -> int -> string
 end;
 
 structure Latex: LATEX =
 struct
 
 (* 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);
-
-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 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;
+type text = XML.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 text ("", _) = []
+  | text (s, pos) = [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
 
-end;
+fun string s = text (s, Position.none);
 
-fun enclose_body bg en body =
-  (if bg = "" then [] else [string bg]) @ body @
-  (if en = "" then [] else [string en]);
+fun block body = XML.Elem (Markup.document_latex, body);
 
-fun enclose_block bg en = block o enclose_body bg en;
+fun latex_text text =
+  text |> maps
+    (fn XML.Elem ((name, _), body) =>
+          if name = Markup.document_latexN then latex_text body else []
+      | t => [t]);
+
+val output_text = XML.content_of o latex_text;
+
+fun enclose_text bg en body = string bg @ body @ string en;
 
 
 (* output name for LaTeX macros *)
 
 val output_name =
   translate_string
     (fn "_" => "UNDERSCORE"
       | "'" => "PRIME"
       | "0" => "ZERO"
       | "1" => "ONE"
       | "2" => "TWO"
       | "3" => "THREE"
       | "4" => "FOUR"
       | "5" => "FIVE"
       | "6" => "SIX"
       | "7" => "SEVEN"
       | "8" => "EIGHT"
       | "9" => "NINE"
       | s => s);
 
 fun enclose_name bg en = enclose bg en o output_name;
 
 
 (* output verbatim ASCII *)
 
 val output_ascii =
   translate_string
     (fn " " => "\\ "
       | "\t" => "\\ "
       | "\n" => "\\isanewline\n"
       | s =>
           s
           |> exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" ? enclose "{\\char`\\" "}"
           |> suffix "{\\kern0pt}");
 
 fun output_ascii_breakable sep =
   space_explode sep
   #> map output_ascii
   #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
 
 
 (* output symbols *)
 
 local
 
 val char_table =
   Symtab.make
    [("\007", "{\\isacharbell}"),
     ("!", "{\\isacharbang}"),
     ("\"", "{\\isachardoublequote}"),
     ("#", "{\\isacharhash}"),
     ("$", "{\\isachardollar}"),
     ("%", "{\\isacharpercent}"),
     ("&", "{\\isacharampersand}"),
     ("'", "{\\isacharprime}"),
     ("(", "{\\isacharparenleft}"),
     (")", "{\\isacharparenright}"),
     ("*", "{\\isacharasterisk}"),
     ("+", "{\\isacharplus}"),
     (",", "{\\isacharcomma}"),
     ("-", "{\\isacharminus}"),
     (".", "{\\isachardot}"),
     ("/", "{\\isacharslash}"),
     (":", "{\\isacharcolon}"),
     (";", "{\\isacharsemicolon}"),
     ("<", "{\\isacharless}"),
     ("=", "{\\isacharequal}"),
     (">", "{\\isachargreater}"),
     ("?", "{\\isacharquery}"),
     ("@", "{\\isacharat}"),
     ("[", "{\\isacharbrackleft}"),
     ("\\", "{\\isacharbackslash}"),
     ("]", "{\\isacharbrackright}"),
     ("^", "{\\isacharcircum}"),
     ("_", "{\\isacharunderscore}"),
     ("`", "{\\isacharbackquote}"),
     ("{", "{\\isacharbraceleft}"),
     ("|", "{\\isacharbar}"),
     ("}", "{\\isacharbraceright}"),
     ("~", "{\\isachartilde}")];
 
 fun output_chr " " = "\\ "
   | output_chr "\t" = "\\ "
   | output_chr "\n" = "\\isanewline\n"
   | output_chr c =
       (case Symtab.lookup char_table c of
         SOME s => s ^ "{\\kern0pt}"
       | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
 
 fun output_sym sym =
   (case Symbol.decode sym of
     Symbol.Char s => output_chr s
   | Symbol.UTF8 s => s
   | Symbol.Sym s => enclose_name "{\\isasym" "}" s
   | Symbol.Control s => enclose_name "\\isactrl" " " s
   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   | Symbol.EOF => error "Bad EOF symbol");
 
 open Basic_Symbol_Pos;
 
 val scan_latex_length =
   Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s)
     >> (Symbol.length o map Symbol_Pos.symbol) ||
   $$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
 
 val scan_latex =
   $$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: "
     >> (implode o map Symbol_Pos.symbol) ||
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
 
 fun read scan syms =
   Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
 
 in
 
 fun length_symbols syms =
   fold Integer.add (these (read scan_latex_length syms)) 0;
 
 fun output_symbols syms =
   if member (op =) syms Symbol.latex then
     (case read scan_latex syms of
       SOME ss => implode ss
     | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
   else implode (map output_sym syms);
 
 val output_syms = output_symbols o Symbol.explode;
 
 end;
 
 fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
 fun symbols_output syms =
   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 "{\\isafold" "}%\n" tg;
 
 
 (* theory presentation *)
 
 fun environment_delim name =
  ("%\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";
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
 
 
 (* index entries *)
 
 type index_item = {text: text, like: string};
 type index_entry = {items: index_item list, def: bool};
 
 val index_escape =
   translate_string (fn s =>
     if member_string "!\"@|" s then "\\char" ^ string_of_int (ord s)
     else if member_string "\\{}#" s then "\"" ^ s else s);
 
 fun index_item (item: index_item) =
   let
     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) =
   (space_implode "!" (map index_item (#items entry)) ^
     "|" ^ index_escape (if #def entry then "isaindexdef" else "isaindexref"))
   |> enclose "\\index{" "}"
   |> string;
 
 fun index_binding NONE = I
   | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
 
 fun index_variants setup binding =
   fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
 
 
 (* print mode *)
 
 val latexN = "latex";
 
 fun latex_output str =
   let val syms = Symbol.explode str
   in (output_symbols syms, length_symbols syms) end;
 
 fun latex_markup (s, _: Properties.T) =
   if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
   then ("\\isacommand{", "}")
   else if s = Markup.keyword2N
   then ("\\isakeyword{", "}")
   else Markup.no_output;
 
 fun latex_indent "" _ = ""
   | latex_indent s _ = enclose "\\isaindent{" "}" s;
 
 val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
 val _ = Markup.add_mode latexN latex_markup;
 val _ = Pretty.add_mode latexN latex_indent;
 
 end;
diff --git a/src/Pure/Thy/latex.scala b/src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala
+++ b/src/Pure/Thy/latex.scala
@@ -1,182 +1,220 @@
 /*  Title:      Pure/Thy/latex.scala
     Author:     Makarius
 
 Support for LaTeX.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
 import scala.util.matching.Regex
 
 
 object Latex
 {
   /** latex errors **/
 
   def latex_errors(dir: Path, root_name: String): List[String] =
   {
     val root_log_path = dir + Path.explode(root_name).ext("log")
     if (root_log_path.is_file) {
       for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
       yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)
     }
     else Nil
   }
 
 
+  /* 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
   private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
 
   def read_tex_file(tex_file: Path): Tex_File =
   {
     val positions =
       Line.logical_lines(File.read(tex_file)).reverse.
         takeWhile(_ != "\\endinput").reverse
 
     val source_file =
       positions match {
         case File_Pattern(file) :: _ => Some(file)
         case _ => None
       }
 
     val source_lines =
       if (source_file.isEmpty) Nil
       else
         positions.flatMap(line =>
           line match {
             case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
             case _ => None
           })
 
     new Tex_File(tex_file, source_file, source_lines)
   }
 
   final class Tex_File private[Latex](
     tex_file: Path, source_file: Option[String], source_lines: List[(Int, Int)])
   {
     override def toString: String = tex_file.toString
 
     def source_position(l: Int): Option[Position.T] =
       source_file match {
         case None => None
         case Some(file) =>
           val source_line =
             source_lines.iterator.takeWhile({ case (m, _) => m <= l }).
               foldLeft(0) { case (_, (_, n)) => n }
           if (source_line == 0) None else Some(Position.Line_File(source_line, file))
       }
 
     def position(line: Int): Position.T =
       source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
   }
 
 
   /* latex log */
 
   def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] =
   {
     val seen_files = Synchronized(Map.empty[JFile, Tex_File])
 
     def check_tex_file(path: Path): Option[Tex_File] =
       seen_files.change_result(seen =>
         seen.get(path.file) match {
           case None =>
             if (path.is_file) {
               val tex_file = read_tex_file(path)
               (Some(tex_file), seen + (path.file -> tex_file))
             }
             else (None, seen)
           case some => (some, seen)
         })
 
     def tex_file_position(path: Path, line: Int): Position.T =
       check_tex_file(path) match {
         case Some(tex_file) => tex_file.position(line)
         case None => Position.Line_File(line, path.implode)
       }
 
     object File_Line_Error
     {
       val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
       def unapply(line: String): Option[(Path, Int, String)] =
         line match {
           case Pattern(file, Value.Int(line), message) =>
             val path = File.standard_path(file)
             if (Path.is_wellformed(path)) {
               val file = (dir + Path.explode(path)).canonical
               val msg = Library.perhaps_unprefix("LaTeX Error: ", message)
               if (file.is_file) Some((file, line, msg)) else None
             }
             else None
           case _ => None
         }
     }
 
     val Line_Error = """^l\.\d+ (.*)$""".r
     val More_Error =
       List(
         "<argument>",
         "<template>",
         "<recently read>",
         "<to be read again>",
         "<inserted text>",
         "<output>",
         "<everypar>",
         "<everymath>",
         "<everydisplay>",
         "<everyhbox>",
         "<everyvbox>",
         "<everyjob>",
         "<everycr>",
         "<mark>",
         "<everyeof>",
         "<write>").mkString("^(?:", "|", ") (.*)$").r
 
     val Bad_Font = """^LaTeX Font Warning: (Font .*\btxmia\b.* undefined).*$""".r
     val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
 
     val error_ignore =
       Set(
         "See the LaTeX manual or LaTeX Companion for explanation.",
         "Type  H <return>  for immediate help.")
 
     def error_suffix1(lines: List[String]): Option[String] =
     {
       val lines1 =
         lines.take(20).takeWhile({ case File_Line_Error((_, _, _)) => false case _ => true })
       lines1.zipWithIndex.collectFirst({
         case (Line_Error(msg), i) =>
           cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
     }
     def error_suffix2(lines: List[String]): Option[String] =
       lines match {
         case More_Error(msg) :: _ => Some(msg)
         case _ => None
       }
 
     @tailrec def filter(lines: List[String], result: List[(String, Position.T)])
       : List[(String, Position.T)] =
     {
       lines match {
         case File_Line_Error((file, line, msg1)) :: rest1 =>
           val pos = tex_file_position(file, line)
           val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
           filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
         case Bad_Font(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case Bad_File(msg) :: rest =>
           filter(rest, (msg, Position.none) :: result)
         case _ :: rest => filter(rest, result)
         case Nil => result.reverse
       }
     }
 
     filter(Line.logical_lines(root_log), Nil)
   }
 }
diff --git a/src/Pure/Thy/thy_info.ML b/src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML
+++ b/src/Pure/Thy/thy_info.ML
@@ -1,483 +1,481 @@
 (*  Title:      Pure/Thy/thy_info.ML
     Author:     Makarius
 
 Global theory info database, with auto-loading according to theory and
 file dependencies, and presentation of theory documents.
 *)
 
 signature THY_INFO =
 sig
   type presentation_context =
     {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
       segments: Document_Output.segment list}
   val adjust_pos_properties: presentation_context -> Position.T -> Properties.T
   val apply_presentation: presentation_context -> theory -> unit
   val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories: Options.T -> string -> (string * Position.T) list -> unit
   val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
 
 structure Thy_Info: THY_INFO =
 struct
 
 (** theory presentation **)
 
 (* artefact names *)
 
 fun document_name ext thy =
   Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext);
 
 val document_tex_name = document_name "tex";
 
 
 (* hook for consolidated theory *)
 
 type presentation_context =
   {options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
     segments: Document_Output.segment list};
 
 fun adjust_pos_properties (context: presentation_context) pos =
   Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos;
 
 structure Presentation = Theory_Data
 (
   type T = ((presentation_context -> theory -> unit) * stamp) list;
   val empty = [];
   val extend = I;
   fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
 fun sequential_presentation options =
   not (Options.bool options \<^system_option>\<open>parallel_presentation\<close>);
 
 fun apply_presentation (context: presentation_context) thy =
   Par_List.map'
     {name = "apply_presentation", sequential = sequential_presentation (#options context)}
     (fn (f, _) => f context thy) (Presentation.get thy)
   |> ignore;
 
 fun add_presentation f = Presentation.map (cons (f, stamp ()));
 
 val _ =
   Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
     if exists (Toplevel.is_skipped_proof o #state) segments then ()
     else
       let
         val body = Document_Output.present_thy options thy segments;
       in
         if Options.string options "document" = "false" then ()
         else
           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));
 
 
 
 (** thy database **)
 
 (* messages *)
 
 val show_path = space_implode " via " o map quote;
 
 fun cycle_msg names = "Cyclic dependency of " ^ show_path names;
 
 
 (* derived graph operations *)
 
 fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
   handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
 
 fun new_entry name parents entry =
   String_Graph.new_node (name, entry) #> add_deps name parents;
 
 
 (* global thys *)
 
 type deps =
  {master: (Path.T * SHA1.digest),  (*master dependencies for thy file*)
   imports: (string * Position.T) list};  (*source specification of imports (partially qualified)*)
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
 fun master_dir_deps (d: deps option) =
   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 
 local
   val global_thys =
     Synchronized.var "Thy_Info.thys"
       (String_Graph.empty: (deps option * theory option) String_Graph.T);
 in
   fun get_thys () = Synchronized.value global_thys;
   fun change_thys f = Synchronized.change global_thys f;
 end;
 
 fun get_names () = String_Graph.topological_order (get_thys ());
 
 
 (* access thy *)
 
 fun lookup thys name = try (String_Graph.get_node thys) name;
 fun lookup_thy name = lookup (get_thys ()) name;
 
 fun get thys name =
   (case lookup thys name of
     SOME thy => thy
   | NONE => error ("Theory loader: nothing known about theory " ^ quote name));
 
 fun get_thy name = get (get_thys ()) name;
 
 
 (* access deps *)
 
 val lookup_deps = Option.map #1 o lookup_thy;
 
 val master_directory = master_dir_deps o #1 o get_thy;
 
 
 (* access theory *)
 
 fun lookup_theory name =
   (case lookup_thy name of
     SOME (_, SOME theory) => SOME theory
   | _ => NONE);
 
 fun get_theory name =
   (case lookup_theory name of
     SOME theory => theory
   | _ => error ("Theory loader: undefined entry for theory " ^ quote name));
 
 val get_imports = Resources.imports_of o get_theory;
 
 
 
 (** thy operations **)
 
 (* remove *)
 
 fun remove name thys =
   (case lookup thys name of
     NONE => thys
   | SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name)
   | SOME _ =>
       let
         val succs = String_Graph.all_succs thys [name];
         val _ = writeln ("Theory loader: removing " ^ commas_quote succs);
       in fold String_Graph.del_node succs thys end);
 
 val remove_thy = change_thys o remove;
 
 
 (* update *)
 
 fun update deps theory thys =
   let
     val name = Context.theory_long_name theory;
     val parents = map Context.theory_long_name (Theory.parents_of theory);
 
     val thys' = remove name thys;
     val _ = map (get thys') parents;
   in new_entry name parents (SOME deps, SOME theory) thys' end;
 
 fun update_thy deps theory = change_thys (update deps theory);
 
 
 (* scheduling loader tasks *)
 
 datatype result =
   Result of {theory: theory, exec_id: Document_ID.exec,
     present: unit -> unit, commit: unit -> unit, weight: int};
 
 fun theory_result theory =
   Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0};
 
 fun result_theory (Result {theory, ...}) = theory;
 fun result_present (Result {present, ...}) = present;
 fun result_commit (Result {commit, ...}) = commit;
 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
 
 fun join_theory (Result {theory, exec_id, ...}) =
   let
     val _ = Execution.join [exec_id];
     val res = Exn.capture Thm.consolidate_theory theory;
     val exns = maps Task_Queue.group_status (Execution.peek exec_id);
   in res :: map Exn.Exn exns end;
 
 datatype task =
   Task of string list * (theory list -> result) |
   Finished of theory;
 
 fun task_finished (Task _) = false
   | task_finished (Finished _) = true;
 
 fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
 
 val schedule_seq =
   String_Graph.schedule (fn deps => fn (_, task) =>
     (case task of
       Task (parents, body) =>
         let
           val result = body (task_parents deps parents);
           val _ = Par_Exn.release_all (join_theory result);
           val _ = result_present result ();
           val _ = result_commit result ();
         in result_theory result end
     | Finished thy => thy)) #> ignore;
 
 val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
   let
     val futures = tasks
       |> String_Graph.schedule (fn deps => fn (name, task) =>
         (case task of
           Task (parents, body) =>
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = NONE,
                 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
               (fn () =>
                 (case filter (not o can Future.join o #2) deps of
                   [] => body (map (result_theory o Future.join) (task_parents deps parents))
                 | bad =>
                     error
                       ("Failed to load theory " ^ quote name ^
                         " (unresolved " ^ commas_quote (map #1 bad) ^ ")")))
         | Finished theory => Future.value (theory_result theory)));
 
     val results1 = futures
       |> maps (fn future =>
           (case Future.join_result future of
             Exn.Res result => join_theory result
           | Exn.Exn exn => [Exn.Exn exn]));
 
     val results2 = futures
       |> map_filter (Exn.get_res o Future.join_result)
       |> sort result_ord
       |> Par_List.map'
           {name = "present", sequential = sequential_presentation (Options.default ())}
           (fn result => Exn.capture (result_present result) ());
 
     (* FIXME more precise commit order (!?) *)
     val results3 = futures
       |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
 
     (* FIXME avoid global Execution.reset (!??) *)
     val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
 
     val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
   in () end);
 
 
 (* eval theory *)
 
 fun eval_thy options master_dir header text_pos text parents =
   let
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
 
     val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
     val elements = Thy_Element.parse_elements keywords spans;
 
     val text_id = Position.copy_id text_pos Position.none;
 
     fun init () = Resources.begin_theory master_dir header parents;
 
     fun excursion () =
       let
         fun element_result span_elem (st, _) =
           let
             fun prepare span =
               let
                 val tr =
                   Position.setmp_thread_data text_id
                     (fn () => Command.read_span keywords st master_dir init span) ();
               in Toplevel.timing (Resources.last_timing tr) tr end;
             val elem = Thy_Element.map_element prepare span_elem;
             val (results, st') = Toplevel.element_result keywords elem st;
             val pos' = Toplevel.pos_of (Thy_Element.last_element elem);
           in (results, (st', pos')) end;
 
         val (results, (end_state, end_pos)) =
           fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
 
         val thy = Toplevel.end_theory end_pos end_state;
       in (results, thy) end;
 
     val (results, thy) = cond_timeit true ("theory " ^ quote name) excursion;
 
     fun present () =
       let
         val segments =
           (spans ~~ maps Toplevel.join_results results) |> map (fn (span, (st, tr, st')) =>
             {span = span, prev_state = st, command = tr, state = st'});
         val context: presentation_context =
           {options = options, file_pos = text_pos, adjust_pos = I, segments = segments};
       in apply_presentation context thy end;
 
   in (thy, present, size text) end;
 
 
 (* require_thy -- checking database entries wrt. the file-system *)
 
 local
 
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
 fun load_thy options initiators deps text (name, header_pos) keywords parents =
   let
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
 
     val exec_id = Document_ID.make ();
     val id = Document_ID.print exec_id;
     val put_id = Position.put_id id;
     val _ =
       Execution.running Document_ID.none exec_id [] orelse
         raise Fail ("Failed to register execution: " ^ id);
 
     val text_pos = put_id (Path.position thy_path);
     val text_props = Position.properties_of text_pos;
 
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
     val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]];
 
     val _ =
       Position.setmp_thread_data (Position.id_only id) (fn () =>
         (parents, map #2 imports) |> ListPair.app (fn (thy, pos) =>
           Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) ();
 
     val timing_start = Timing.start ();
 
     val header = Thy_Header.make (name, put_id header_pos) imports keywords;
     val (theory, present, weight) =
       eval_thy options dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
     val timing_result = Timing.result timing_start;
     val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
     val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
 
     fun commit () = update_thy deps theory;
   in
     Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
   end;
 
 fun check_thy_deps dir name =
   (case lookup_deps name of
     SOME NONE => (true, NONE, Position.none, get_imports name, [])
   | NONE =>
       let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name
       in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end
   | SOME (SOME {master, ...}) =>
       let
         val {master = master', text = text', theory_pos = theory_pos', imports = imports',
           keywords = keywords'} = Resources.check_thy dir name;
         val deps' = SOME (make_deps master' imports', text');
         val current =
           #2 master = #2 master' andalso
             (case lookup_theory name of
               NONE => false
             | SOME theory => Resources.loaded_files_current theory);
       in (current, deps', theory_pos', imports', keywords') end);
 
 in
 
 fun require_thys options initiators qualifier dir strs tasks =
       fold_map (require_thy options initiators qualifier dir) strs tasks |>> forall I
 and require_thy options initiators qualifier dir (s, require_pos) tasks =
   let
     val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
   in
     (case try (String_Graph.get_node tasks) theory_name of
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
 
           val (current, deps, theory_pos, imports, keywords) = check_thy_deps master_dir theory_name
             handle ERROR msg =>
               cat_error msg
                 ("The error(s) above occurred for theory " ^ quote theory_name ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
           val qualifier' = Resources.theory_qualifier theory_name;
           val dir' = dir + master_dir_deps (Option.map #1 deps);
 
           val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
           val (parents_current, tasks') =
             require_thys options (theory_name :: initiators) qualifier' dir' imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
             if all_current then Finished (get_theory theory_name)
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
               | SOME (dep, text) =>
                   Task (parents,
                     load_thy options initiators dep text (theory_name, theory_pos) keywords));
 
           val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
   end;
 
 end;
 
 
 (* use theories *)
 
 fun use_theories options qualifier imports =
   let val (_, tasks) = require_thys options [] qualifier Path.current imports String_Graph.empty
   in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end;
 
 fun use_thy name =
   use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)];
 
 
 (* toplevel scripting -- without maintaining database *)
 
 fun script_thy pos txt thy =
   let
     val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
     val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
     val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
   in Toplevel.end_theory end_pos end_state end;
 
 
 (* register theory *)
 
 fun register_thy theory =
   let
     val name = Context.theory_long_name theory;
     val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
     val imports = Resources.imports_of theory;
   in
     change_thys (fn thys =>
       let
         val thys' = remove name thys;
         val _ = writeln ("Registering theory " ^ quote name);
       in update (make_deps master imports) theory thys' end)
   end;
 
 
 (* finish all theories *)
 
 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
 
 end;
 
 fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);
diff --git a/src/Pure/Tools/rail.ML b/src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML
+++ b/src/Pure/Tools/rail.ML
@@ -1,392 +1,392 @@
 (*  Title:      Pure/Tools/rail.ML
     Author:     Michael Kerscher, TU München
     Author:     Makarius
 
 Railroad diagrams in LaTeX.
 *)
 
 signature RAIL =
 sig
   datatype rails =
     Cat of int * rail list
   and rail =
     Bar of rails list |
     Plus of rails * rails |
     Newline of int |
     Nonterminal of string |
     Terminal of bool * string |
     Antiquote of bool * Antiquote.antiq
   val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
   val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> Latex.text
 end;
 
 structure Rail: RAIL =
 struct
 
 (** lexical syntax **)
 
 (* singleton keywords *)
 
 val keywords =
   Symtab.make [
     ("|", Markup.keyword3),
     ("*", Markup.keyword3),
     ("+", Markup.keyword3),
     ("?", Markup.keyword3),
     ("(", Markup.empty),
     (")", Markup.empty),
     ("\<newline>", Markup.keyword2),
     (";", Markup.keyword2),
     (":", Markup.keyword2),
     ("@", Markup.keyword1)];
 
 
 (* datatype token *)
 
 datatype kind =
   Keyword | Ident | String | Space | Comment of Comment.kind | Antiq of Antiquote.antiq | EOF;
 
 datatype token = Token of Position.range * (kind * string);
 
 fun pos_of (Token ((pos, _), _)) = pos;
 fun end_pos_of (Token ((_, pos), _)) = pos;
 
 fun range_of (toks as tok :: _) =
       let val pos' = end_pos_of (List.last toks)
       in Position.range (pos_of tok, pos') end
   | range_of [] = Position.no_range;
 
 fun kind_of (Token (_, (k, _))) = k;
 fun content_of (Token (_, (_, x))) = x;
 
 fun is_proper (Token (_, (Space, _))) = false
   | is_proper (Token (_, (Comment _, _))) = false
   | is_proper _ = true;
 
 
 (* diagnostics *)
 
 val print_kind =
  fn Keyword => "rail keyword"
   | Ident => "identifier"
   | String => "single-quoted string"
   | Space => "white space"
   | Comment _ => "formal comment"
   | Antiq _ => "antiquotation"
   | EOF => "end-of-input";
 
 fun print (Token ((pos, _), (k, x))) =
   (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
   Position.here pos;
 
 fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
 
 fun reports_of_token (Token ((pos, _), (Keyword, x))) =
       map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
   | reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
   | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports [Antiquote.Antiq antiq]
   | reports_of_token _ = [];
 
 
 (* stopper *)
 
 fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
 val eof = mk_eof Position.none;
 
 fun is_eof (Token (_, (EOF, _))) = true
   | is_eof _ = false;
 
 val stopper =
   Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
 
 
 (* tokenize *)
 
 local
 
 fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
 
 fun antiq_token antiq =
   [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))];
 
 val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
 
 val scan_keyword =
   Scan.one (Symtab.defined keywords o Symbol_Pos.symbol);
 
 val err_prefix = "Rail lexical error: ";
 
 val scan_token =
   scan_space >> token Space ||
   Comment.scan_inner >> (fn (kind, ss) => token (Comment kind) ss) ||
   Antiquote.scan_antiq >> antiq_token ||
   scan_keyword >> (token Keyword o single) ||
   Lexicon.scan_id >> token Ident ||
   Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
     [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]);
 
 val scan =
   Scan.repeats scan_token --|
     Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
       (Scan.ahead (Scan.one Symbol_Pos.is_eof));
 
 in
 
 val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan);
 
 end;
 
 
 
 (** parsing **)
 
 (* parser combinators *)
 
 fun !!! scan =
   let
     val prefix = "Rail syntax error";
 
     fun get_pos [] = " (end-of-input)"
       | get_pos (tok :: _) = Position.here (pos_of tok);
 
     fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
       | err (toks, SOME msg) =
           (fn () =>
             let val s = msg () in
               if String.isPrefix prefix s then s
               else prefix ^ get_pos toks ^ ": " ^ s
             end);
   in Scan.!! err scan end;
 
 fun $$$ x =
   Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
   Scan.fail_with
     (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found")
       | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
 
 fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
 fun enum sep scan = enum1 sep scan || Scan.succeed [];
 
 val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
 val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
 
 val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
 
 fun RANGE scan = Scan.trace scan >> apsnd range_of;
 fun RANGE_APP scan = RANGE scan >> (fn (f, r) => f r);
 
 
 (* parse trees *)
 
 datatype trees =
   CAT of tree list * Position.range
 and tree =
   BAR of trees list * Position.range |
   STAR of (trees * trees) * Position.range |
   PLUS of (trees * trees) * Position.range |
   MAYBE of tree * Position.range |
   NEWLINE of Position.range |
   NONTERMINAL of string * Position.range |
   TERMINAL of (bool * string) * Position.range |
   ANTIQUOTE of (bool * Antiquote.antiq) * Position.range;
 
 fun reports_of_tree ctxt =
   if Context_Position.reports_enabled ctxt then
     let
       fun reports r =
         if r = Position.no_range then []
         else [(Position.range_position r, Markup.expression "")];
       fun trees (CAT (ts, r)) = reports r @ maps tree ts
       and tree (BAR (Ts, r)) = reports r @ maps trees Ts
         | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
         | tree (PLUS ((T1, T2), r)) = reports r @ trees T1 @ trees T2
         | tree (MAYBE (t, r)) = reports r @ tree t
         | tree (NEWLINE r) = reports r
         | tree (NONTERMINAL (_, r)) = reports r
         | tree (TERMINAL (_, r)) = reports r
         | tree (ANTIQUOTE (_, r)) = reports r;
     in distinct (op =) o tree end
   else K [];
 
 local
 
 val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
 
 fun body x = (RANGE (enum1 "|" body1) >> BAR) x
 and body0 x = (RANGE (enum "|" body1) >> BAR) x
 and body1 x =
  (RANGE_APP (body2 :|-- (fn a =>
    $$$ "*" |-- !!! body4e >> (fn b => fn r => CAT ([STAR ((a, b), r)], r)) ||
    $$$ "+" |-- !!! body4e >> (fn b => fn r => CAT ([PLUS ((a, b), r)], r)) ||
    Scan.succeed (K a)))) x
 and body2 x = (RANGE (Scan.repeat1 body3) >> CAT) x
 and body3 x =
  (RANGE_APP (body4 :|-- (fn a =>
    $$$ "?" >> K (curry MAYBE a) ||
    Scan.succeed (K a)))) x
 and body4 x =
  ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
   RANGE_APP
    ($$$ "\<newline>" >> K NEWLINE ||
     ident >> curry NONTERMINAL ||
     at_mode -- string >> curry TERMINAL ||
     at_mode -- antiq >> curry ANTIQUOTE)) x
 and body4e x =
   (RANGE (Scan.option body4) >> (fn (a, r) => CAT (the_list a, r))) x;
 
 val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
 val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
 val rules = enum1 ";" (Scan.option rule) >> map_filter I;
 
 in
 
 fun parse_rules toks =
   #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks);
 
 end;
 
 
 (** rail expressions **)
 
 (* datatype *)
 
 datatype rails =
   Cat of int * rail list
 and rail =
   Bar of rails list |
   Plus of rails * rails |
   Newline of int |
   Nonterminal of string |
   Terminal of bool * string |
   Antiquote of bool * Antiquote.antiq;
 
 fun is_newline (Newline _) = true | is_newline _ = false;
 
 
 (* prepare *)
 
 local
 
 fun cat rails = Cat (0, rails);
 
 val empty = cat [];
 fun is_empty (Cat (_, [])) = true | is_empty _ = false;
 
 fun bar [Cat (_, [rail])] = rail
   | bar cats = Bar cats;
 
 fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
 and reverse (Bar cats) = Bar (map reverse_cat cats)
   | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
   | reverse x = x;
 
 fun plus (cat1, cat2) = Plus (cat1, reverse_cat cat2);
 
 in
 
 fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts)
 and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts)
   | prepare_tree (STAR (Ts, _)) =
       let val (cat1, cat2) = apply2 prepare_trees Ts in
         if is_empty cat2 then plus (empty, cat1)
         else bar [empty, cat [plus (cat1, cat2)]]
       end
   | prepare_tree (PLUS (Ts, _)) = plus (apply2 prepare_trees Ts)
   | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]]
   | prepare_tree (NEWLINE _) = Newline 0
   | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a
   | prepare_tree (TERMINAL (a, _)) = Terminal a
   | prepare_tree (ANTIQUOTE (a, _)) = Antiquote a;
 
 end;
 
 
 (* read *)
 
 fun read ctxt source =
   let
     val _ = Context_Position.report ctxt (Input.pos_of source) Markup.language_rail;
     val toks = tokenize (Input.source_explode source);
     val _ = Context_Position.reports ctxt (maps reports_of_token toks);
     val rules = parse_rules (filter is_proper toks);
     val _ = Context_Position.reports ctxt (maps (reports_of_tree ctxt o #2) rules);
   in map (apsnd prepare_tree) rules end;
 
 
 (* latex output *)
 
 local
 
 fun vertical_range_cat (Cat (_, rails)) y =
   let val (rails', (_, y')) =
     fold_map (fn rail => fn (y0, y') =>
       if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
       else
         let val (rail', y0') = vertical_range rail y0;
         in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
   in (Cat (y, rails'), y') end
 
 and vertical_range (Bar cats) y =
       let val (cats', y') = fold_map vertical_range_cat cats y
       in (Bar cats', Int.max (y + 1, y')) end
   | vertical_range (Plus (cat1, cat2)) y =
       let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
       in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
   | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   | vertical_range atom y = (atom, y + 1);
 
 in
 
 fun output_rules ctxt rules =
   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
       |> b ? enclose "\\isakeyword{" "}"
       |> enclose "\\isa{" "}";
 
     fun output_cat c (Cat (_, rails)) = outputs c rails
     and outputs c [rail] = output c rail
       | outputs _ rails = implode (map (output "") rails)
     and output _ (Bar []) = ""
       | output c (Bar [cat]) = output_cat c cat
       | output _ (Bar (cat :: cats)) =
           "\\rail@bar\n" ^ output_cat "" cat ^
           implode (map (fn Cat (y, rails) =>
               "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
           "\\rail@endbar\n"
       | output c (Plus (cat, Cat (y, rails))) =
           "\\rail@plus\n" ^ output_cat c cat ^
           "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
           "\\rail@endplus\n"
       | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
       | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n"
       | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n"
       | output c (Antiquote (b, a)) =
           "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
 
     fun output_rule (name, rail) =
       let
         val (rail', y') = vertical_range rail 0;
         val out_name =
           (case name of
             Antiquote.Text "" => ""
           | Antiquote.Text s => output_text false s
           | Antiquote.Antiq a => output_antiq a);
       in
         "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
         output "" rail' ^
         "\\rail@end\n"
       end;
   in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end;
 
 val _ = Theory.setup
   (Document_Output.antiquotation_raw_embedded \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
     (fn ctxt => output_rules ctxt o read ctxt));
 
 end;
 
 end;