clarified access to antiquotation options;
define explicit variants of antiquotations;
output proper Latex.text;
misc tuning and clarification;

--- a/src/Doc/Main/Main_Doc.thy	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Thu Jan 18 21:41:30 2018 +0100
@@ -4,23 +4,15 @@
 begin
 
 setup \<open>
-  let
-    fun pretty_term_type_only ctxt (t, T) =
+  Thy_Output.antiquotation_pretty_source @{binding term_type_only} (Args.term -- Args.typ_abbrev)
+    (fn ctxt => fn (t, T) =>
       (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
        else error "term_type_only: type mismatch";
-       Syntax.pretty_typ ctxt T)
-  in
-    Document_Antiquotation.setup @{binding term_type_only}
-      (Args.term -- Args.typ_abbrev)
-      (fn {source, context = ctxt, ...} => fn arg =>
-        Thy_Output.output ctxt
-          (Thy_Output.maybe_pretty_source pretty_term_type_only ctxt source [arg]))
-  end
+       [Syntax.pretty_typ ctxt T]))
 \<close>
 setup \<open>
-  Document_Antiquotation.setup @{binding expanded_typ} (Args.typ >> single)
-    (fn {source, context, ...} => Thy_Output.output context o
-      Thy_Output.maybe_pretty_source Syntax.pretty_typ context source)
+  Thy_Output.antiquotation_pretty_source @{binding expanded_typ} Args.typ
+    (fn ctxt => fn T => [Syntax.pretty_typ ctxt T])
 \<close>
 (*>*)
 text\<open>

--- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Thu Jan 18 21:41:30 2018 +0100
@@ -43,20 +43,13 @@
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
-setup\<open>
-  let
-    fun pretty ctxt c =
-      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
-      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
-            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
-      end
-  in
-    Document_Antiquotation.setup @{binding "const_typ"}
-     (Scan.lift Args.embedded_inner_syntax)
-       (fn {source = src, context = ctxt, ...} => fn arg =>
-          Thy_Output.output ctxt
-            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
-  end;
+setup \<open>
+  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+    (fn ctxt => fn c =>
+      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
+        [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
+          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]]
+      end)
 \<close>
 
 end

--- a/src/Doc/antiquote_setup.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Doc/antiquote_setup.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -73,9 +73,9 @@
 fun prep_ml source =
   (Input.source_content source, ML_Lex.read_source false source);
 
-fun index_ml name kind ml = Document_Antiquotation.setup name
+fun index_ml name kind ml = Thy_Output.antiquotation_raw name
   (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
-  (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
+  (fn ctxt => fn (source1, opt_source2) =>
     let
       val (txt1, toks1) = prep_ml source1;
       val (txt2, toks2) =
@@ -98,8 +98,9 @@
           handle ERROR msg => error (msg ^ Position.here pos);
       val kind' = if kind = "" then "ML" else "ML " ^ kind;
     in
-      "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
-      (Thy_Output.verbatim_text ctxt txt')
+      Latex.block
+       [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"),
+        Thy_Output.verbatim ctxt txt']
     end);
 
 in
@@ -119,29 +120,18 @@
 (* named theorems *)
 
 val _ =
-  Theory.setup (Document_Antiquotation.setup @{binding named_thms}
+  Theory.setup (Thy_Output.antiquotation_raw @{binding named_thms}
     (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
-    (fn {context = ctxt, ...} =>
-      map (apfst (Thy_Output.pretty_thm ctxt))
-      #> (if Config.get ctxt Document_Antiquotation.thy_output_quotes
-          then map (apfst Pretty.quote) else I)
-      #> (if Config.get ctxt Document_Antiquotation.thy_output_display
-          then
-            map (fn (p, name) =>
-              Output.output
-                (Thy_Output.string_of_margin ctxt
-                  (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent) p)) ^
-              "\\rulename{" ^
-              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
-            #> space_implode "\\par\\smallskip%\n"
-            #> Latex.environment "isabelle"
-          else
-            map (fn (p, name) =>
-              Output.output (Pretty.unformatted_string_of p) ^
-              "\\rulename{" ^
-              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
-            #> space_implode "\\par\\smallskip%\n"
-            #> enclose "\\isa{" "}")));
+    (fn ctxt =>
+      map (fn (thm, name) =>
+        Output.output
+          (Document_Antiquotation.format ctxt
+            (Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^
+        enclose "\\rulename{" "}"
+          (Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name))))
+      #> space_implode "\\par\\smallskip%\n"
+      #> Latex.string #> single
+      #> Thy_Output.isabelle ctxt));
 
 
 (* Isabelle/Isar entities (with index) *)
@@ -161,11 +151,11 @@
 val arg = enclose "{" "}" o clean_string;
 
 fun entity check markup binding index =
-  Document_Antiquotation.setup
+  Thy_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) "" -- Parse.position Args.name))
-    (fn {context = ctxt, ...} => fn (logic, (name, pos)) =>
+    (fn ctxt => fn (logic, (name, pos)) =>
       let
         val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding);
         val hyper_name =
@@ -180,12 +170,12 @@
               "\\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 ();
-      in
-        idx ^
-        (Output.output name
-          |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
-          |> hyper o enclose "\\mbox{\\isa{" "}}")
-      end);
+        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 #>

--- a/src/Doc/more_antiquote.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Doc/more_antiquote.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -9,53 +9,37 @@
 
 (* class specifications *)
 
-local
-
-fun class_spec ctxt s =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val class = Sign.intern_class thy s;
-  in Thy_Output.output ctxt (Class.pretty_specification thy class) end;
-
-in
-
 val _ =
-  Theory.setup (Document_Antiquotation.setup @{binding class_spec} (Scan.lift Args.name)
-    (fn {context, ...} => class_spec context));
-
-end;
+  Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name)
+    (fn ctxt => fn s =>
+      let
+        val thy = Proof_Context.theory_of ctxt;
+        val class = Sign.intern_class thy s;
+      in Class.pretty_specification thy class end));
 
 
 (* code theorem antiquotation *)
 
-local
-
 fun no_vars ctxt thm =
   let
     val ctxt' = Variable.set_body false ctxt;
     val ((_, [thm]), _) = Variable.import true [thm] ctxt';
   in thm end;
 
-fun pretty_code_thm ctxt raw_const =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-    val const = Code.check_const thy raw_const;
-    val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
-    fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
-    val thms = Code_Preproc.cert eqngr const
-      |> Code.equations_of_cert thy
-      |> snd
-      |> these
-      |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
-      |> map (holize o no_vars ctxt o Axclass.overload ctxt);
-  in Thy_Output.output ctxt (map (Thy_Output.pretty_thm ctxt) thms) end;
-
-in
-
 val _ =
-  Theory.setup (Document_Antiquotation.setup @{binding code_thms} Args.term
-    (fn {context, ...} => pretty_code_thm context));
+  Theory.setup (Thy_Output.antiquotation_pretty @{binding code_thms} Args.term
+    (fn ctxt => fn raw_const =>
+      let
+        val thy = Proof_Context.theory_of ctxt;
+        val const = Code.check_const thy raw_const;
+        val { eqngr, ... } = Code_Preproc.obtain true { ctxt = ctxt, consts = [const], terms = [] };
+        fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm];
+        val thms = Code_Preproc.cert eqngr const
+          |> Code.equations_of_cert thy
+          |> snd
+          |> these
+          |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
+          |> map (holize o no_vars ctxt o Axclass.overload ctxt);
+      in map (Thy_Output.pretty_thm ctxt) thms end));
 
 end;
-
-end;

--- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Jan 18 21:41:30 2018 +0100
@@ -96,20 +96,13 @@
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
-setup\<open>
-  let
-    fun pretty ctxt c =
-      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c
-      in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
-            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
-      end
-  in
-    Document_Antiquotation.setup @{binding "const_typ"}
-     (Scan.lift Args.embedded_inner_syntax)
-       (fn {source = src, context = ctxt, ...} => fn arg =>
-          Thy_Output.output ctxt
-            (Thy_Output.maybe_pretty_source pretty ctxt src [arg]))
-  end;
+setup \<open>
+  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+    (fn ctxt => fn c =>
+      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
+        [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
+          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]]
+      end)
 \<close>
 
 setup\<open>

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -983,8 +983,8 @@
   end;
 
 fun fp_antiquote_setup binding =
-  Document_Antiquotation.setup binding (Args.type_name {proper = true, strict = true})
-    (fn {source = src, context = ctxt, ...} => fn fcT_name =>
+  Thy_Output.antiquotation_pretty_source binding (Args.type_name {proper = true, strict = true})
+    (fn ctxt => fn fcT_name =>
        (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
          NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
        | SOME {T = T0, ctrs = ctrs0, ...} =>
@@ -1002,9 +1002,6 @@
              Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
                Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
                flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)));
-         in
-           Thy_Output.output ctxt
-             (Thy_Output.maybe_pretty_source (K (K pretty_co_datatype)) ctxt src [()])
-         end));
+         in [pretty_co_datatype] end));
 
 end;

--- a/src/HOL/Tools/value_command.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/HOL/Tools/value_command.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -73,11 +73,10 @@
       >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t)));
 
 val _ = Theory.setup
-  (Document_Antiquotation.setup \<^binding>\<open>value\<close>
+  (Thy_Output.antiquotation_pretty_source \<^binding>\<open>value\<close>
     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
-    (fn {source, context, ...} => fn ((name, style), t) => Thy_Output.output context
-      (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source
-        [style (value_select name context t)]))
+    (fn ctxt => fn ((name, style), t) =>
+      [Thy_Output.pretty_term ctxt (style (value_select name ctxt t))])
   #> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
   #> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
   #> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);

--- a/src/Pure/PIDE/resources.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Pure/PIDE/resources.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -243,12 +243,11 @@
   let
     val dir = master_directory (Proof_Context.theory_of ctxt);
     val _ = check ctxt dir (name, pos);
-  in
-    space_explode "/" name
-    |> map Latex.output_ascii
-    |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
-    |> enclose "\\isatt{" "}"
-  end;
+    val latex =
+      space_explode "/" name
+      |> map Latex.output_ascii
+      |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}");
+  in Latex.enclose_block "\\isatt{" "}" [Latex.string latex] end;
 
 fun ML_antiq check ctxt (name, pos) =
   let val path = check ctxt Path.current (name, pos);
@@ -257,14 +256,14 @@
 in
 
 val _ = Theory.setup
- (Document_Antiquotation.setup \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
-    (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
-  Document_Antiquotation.setup \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq check_path o #context) #>
-  Document_Antiquotation.setup \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq check_file o #context) #>
-  Document_Antiquotation.setup \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
-    (document_antiq check_dir o #context) #>
+ (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
+    (Scan.lift (Parse.position Parse.embedded)) check_session #>
+  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close>
+    (Scan.lift (Parse.position Parse.path)) (document_antiq check_path) #>
+  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close>
+    (Scan.lift (Parse.position Parse.path)) (document_antiq check_file) #>
+  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close>
+    (Scan.lift (Parse.position Parse.path)) (document_antiq check_dir) #>
   ML_Antiquotation.value \<^binding>\<open>path\<close>
     (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>
   ML_Antiquotation.value \<^binding>\<open>file\<close>

--- a/src/Pure/Thy/bibtex.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Pure/Thy/bibtex.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -41,11 +41,11 @@
 val _ =
   Theory.setup
    (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
-    Document_Antiquotation.setup \<^binding>\<open>cite\<close>
+    Thy_Output.antiquotation_raw \<^binding>\<open>cite\<close>
       (Scan.lift
         (Scan.option (Parse.verbatim || Parse.cartouche) --
          Parse.and_list1 (Parse.position Args.name)))
-      (fn {context = ctxt, ...} => fn (opt, citations) =>
+      (fn ctxt => fn (opt, citations) =>
         let
           val thy = Proof_Context.theory_of ctxt;
           val bibtex_entries = Present.get_bibtex_entries thy;
@@ -60,6 +60,6 @@
               (map (fn (name, pos) => (pos, Markup.citation name)) citations);
           val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]");
           val arg = "{" ^ space_implode "," (map #1 citations) ^ "}";
-        in "\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg end));
+        in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end));
 
 end;

--- a/src/Pure/Thy/document_antiquotation.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -13,15 +13,22 @@
   val thy_output_source: 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 quote: 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 ->
-    ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
+    ({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: Proof.context -> Antiquote.text_antiquote -> string
+  val evaluate: Proof.context -> Antiquote.text_antiquote -> Latex.text list
 end;
 
 structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
@@ -38,12 +45,44 @@
 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;
+
+
+(* output *)
+
+fun quote ctxt =
+  Config.get ctxt thy_output_quotes ? Pretty.quote;
+
+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 = quote ctxt #> indent ctxt #> format ctxt #> Output.output;
+
+
 (* theory data *)
 
 structure Data = Theory_Data
 (
   type T =
-    (Token.src -> Proof.context -> string) Name_Space.table *
+    (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,
@@ -73,7 +112,7 @@
   let
     fun cmd src ctxt =
       let val (x, ctxt') = Token.syntax scan src ctxt
-      in body {source = src, context = ctxt'} x end;
+      in body {context = ctxt', source = src, argument = x} end;
   in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> #2)) end;
 
 fun setup_option name opt thy = thy
@@ -119,11 +158,11 @@
     val preview_ctxt = fold option opts 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];
-  in Print_Mode.with_modes print_modes (fn () => command src print_ctxt) () end;
+  in [Print_Mode.with_modes print_modes (fn () => command src print_ctxt) ()] end;
 
 in
 
-fun evaluate _ (Antiquote.Text ss) = Symbol_Pos.content ss
+fun evaluate _ (Antiquote.Text ss) = [Latex.symbols ss]
   | evaluate ctxt (Antiquote.Control {name, body, ...}) =
       eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
   | evaluate ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
@@ -138,13 +177,13 @@
 fun boolean "" = true
   | boolean "true" = true
   | boolean "false" = false
-  | boolean s = error ("Bad boolean value: " ^ quote s);
+  | 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: " ^ quote s));
+      | _ => error ("Bad integer value: " ^ Library.quote s));
   in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
 
 val _ = Theory.setup

--- a/src/Pure/Thy/document_antiquotations.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -11,17 +11,19 @@
 
 local
 
-fun pretty_term_style ctxt (style, t: term) =
+type style = term -> term;
+
+fun pretty_term_style ctxt (style: style, t) =
   Thy_Output.pretty_term ctxt (style t);
 
-fun pretty_thm_style ctxt (style, th) =
+fun pretty_thm_style ctxt (style: style, th) =
   Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th));
 
-fun pretty_term_typ ctxt (style, t: term) =
+fun pretty_term_typ ctxt (style: style, t) =
   let val t' = style t
   in Thy_Output.pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
 
-fun pretty_term_typeof ctxt (style, t) =
+fun pretty_term_typeof ctxt (style: style, t) =
   Syntax.pretty_typ ctxt (Term.fastype_of (style t));
 
 fun pretty_const ctxt c =
@@ -61,15 +63,11 @@
 fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
 
 fun basic_entities name scan pretty =
-  Document_Antiquotation.setup name scan (fn {source, context = ctxt, ...} =>
-    Thy_Output.output ctxt o Thy_Output.maybe_pretty_source pretty ctxt source);
+  Thy_Output.antiquotation_pretty_source name scan (map o pretty);
 
 fun basic_entities_style name scan pretty =
-  Document_Antiquotation.setup name scan
-    (fn {source, context = ctxt, ...} => fn (style, xs) =>
-      Thy_Output.output ctxt
-        (Thy_Output.maybe_pretty_source
-          (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
+  Thy_Output.antiquotation_pretty_source name scan
+    (fn ctxt => fn (style: style, xs) => map (fn x => pretty ctxt (style, x)) xs);
 
 fun basic_entity name scan = basic_entities name (scan >> single);
 
@@ -100,9 +98,9 @@
 
 fun markdown_error binding =
   Document_Antiquotation.setup binding (Scan.succeed ())
-    (fn {source, ...} => fn _ =>
+    (fn {source = src, ...} =>
       error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
-        Position.here (Position.no_range_position (#1 (Token.range_of source)))))
+        Position.here (Position.no_range_position (#1 (Token.range_of src)))))
 
 in
 
@@ -119,14 +117,14 @@
 
 val _ =
   Theory.setup
-   (Document_Antiquotation.setup \<^binding>\<open>noindent\<close> (Scan.succeed ())
-      (K (K "\\noindent")) #>
-    Document_Antiquotation.setup \<^binding>\<open>smallskip\<close> (Scan.succeed ())
-      (K (K "\\smallskip")) #>
-    Document_Antiquotation.setup \<^binding>\<open>medskip\<close> (Scan.succeed ())
-      (K (K "\\medskip")) #>
-    Document_Antiquotation.setup \<^binding>\<open>bigskip\<close> (Scan.succeed ())
-      (K (K "\\bigskip")));
+   (Thy_Output.antiquotation_raw \<^binding>\<open>noindent\<close> (Scan.succeed ())
+      (fn _ => fn () => Latex.string "\\noindent") #>
+    Thy_Output.antiquotation_raw \<^binding>\<open>smallskip\<close> (Scan.succeed ())
+      (fn _ => fn () => Latex.string "\\smallskip") #>
+    Thy_Output.antiquotation_raw \<^binding>\<open>medskip\<close> (Scan.succeed ())
+      (fn _ => fn () => Latex.string "\\medskip") #>
+    Thy_Output.antiquotation_raw \<^binding>\<open>bigskip\<close> (Scan.succeed ())
+      (fn _ => fn () => Latex.string "\\bigskip"));
 
 
 (* control style *)
@@ -134,9 +132,8 @@
 local
 
 fun control_antiquotation name s1 s2 =
-  Document_Antiquotation.setup name (Scan.lift Args.cartouche_input)
-    (fn {context = ctxt, ...} =>
-      enclose s1 s2 o Latex.output_text o Thy_Output.output_text ctxt {markdown = false});
+  Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input)
+    (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_text ctxt {markdown = false});
 
 in
 
@@ -154,11 +151,13 @@
 local
 
 fun text_antiquotation name =
-  Document_Antiquotation.setup name (Scan.lift Args.text_input)
-    (fn {context = ctxt, ...} => fn source =>
-     (Context_Position.report ctxt (Input.pos_of source)
-        (Markup.language_text (Input.is_delimited source));
-      Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)]));
+  Thy_Output.antiquotation_raw name (Scan.lift Args.text_input)
+    (fn ctxt => fn text =>
+      let
+        val _ =
+          Context_Position.report ctxt (Input.pos_of text)
+            (Markup.language_text (Input.is_delimited text));
+      in Thy_Output.pretty ctxt [Thy_Output.pretty_text ctxt (Input.source_content text)] end);
 
 in
 
@@ -174,41 +173,37 @@
 
 val _ =
   Theory.setup
-    (Document_Antiquotation.setup \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
-      (fn {context = ctxt, ...} => fn source =>
+    (Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
+      (fn ctxt => fn text =>
         let
+          val keywords = Thy_Header.get_keywords' ctxt;
+
           val _ =
-            Context_Position.report ctxt (Input.pos_of source)
-              (Markup.language_Isar (Input.is_delimited source));
-
-          val keywords = Thy_Header.get_keywords' ctxt;
-          val toks =
-            Input.source_explode source
-            |> not (Config.get ctxt Document_Antiquotation.thy_output_display) ?
-                Symbol_Pos.trim_lines
+            Context_Position.report ctxt (Input.pos_of text)
+              (Markup.language_Isar (Input.is_delimited text));
+          val _ =
+            Input.source_explode text
             |> Source.of_list
             |> Token.source' true keywords
-            |> Source.exhaust;
-          val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
-          val indentation =
-            Latex.output_symbols
-              (replicate (Config.get ctxt Document_Antiquotation.thy_output_indent) Symbol.space);
-        in
-          Latex.output_text (maps (Thy_Output.output_token ctxt) toks) |>
-           (if Config.get ctxt Document_Antiquotation.thy_output_display then
-              split_lines #> map (prefix indentation) #> cat_lines #>
-              Latex.environment "isabelle"
-            else enclose "\\isa{" "}")
-        end));
+            |> Source.exhaust
+            |> maps (Token.reports keywords)
+            |> Context_Position.reports_text ctxt;
+
+          val toks =
+            Input.source_content text
+            |> Document_Antiquotation.trim_lines ctxt
+            |> Document_Antiquotation.indent_lines ctxt
+            |> Token.explode keywords Position.none;
+        in Thy_Output.isabelle ctxt (maps (Thy_Output.output_token ctxt) toks) end));
 
 
 (* goal state *)
 
 local
 
-fun goal_state name main = Document_Antiquotation.setup name (Scan.succeed ())
-  (fn {context = ctxt, ...} => fn () =>
-    Thy_Output.output ctxt
+fun goal_state name main =
+  Thy_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))))]);
@@ -228,7 +223,7 @@
   (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 {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) =>
+    (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} =>
       let
         val reports =
           (by_pos, Markup.keyword1 |> Markup.keyword_properties) ::
@@ -239,32 +234,30 @@
         val _ = ctxt
           |> Proof.theorem NONE (K I) [[(prop, [])]]
           |> Proof.global_terminal_proof (m1, m2);
-      in
-        Thy_Output.output ctxt
-          (Thy_Output.maybe_pretty_source
-            Thy_Output.pretty_term ctxt [hd source, prop_token] [prop])
-      end));
+      in Thy_Output.pretty_source ctxt [hd src, prop_tok] [Thy_Output.pretty_term ctxt prop] end));
 
 
 (* verbatim text *)
 
-val _ =
-  Theory.setup
-    (Document_Antiquotation.setup \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
-      (fn {context = ctxt, ...} => fn source =>
-       (Context_Position.report ctxt (Input.pos_of source)
-          (Markup.language_verbatim (Input.is_delimited source));
-        Thy_Output.verbatim_text ctxt (Input.source_content source))));
+val _ = Theory.setup
+  (Thy_Output.antiquotation_verbatim \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
+    (fn ctxt => fn text =>
+      let
+        val _ =
+          Context_Position.report ctxt (Input.pos_of text)
+            (Markup.language_verbatim (Input.is_delimited text));
+      in Input.source_content text end));
 
 
 (* ML text *)
 
 local
 
-fun ml_text name ml = Document_Antiquotation.setup name (Scan.lift Args.text_input)
-  (fn {context = ctxt, ...} => fn source =>
-   (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source);
-    Thy_Output.verbatim_text ctxt (Input.source_content source)));
+fun ml_text name ml =
+  Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input)
+    (fn ctxt => fn text =>
+      let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text)
+      in Input.source_content text end);
 
 fun ml_enclose bg en source =
   ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
@@ -291,34 +284,39 @@
 (* URLs *)
 
 val _ = Theory.setup
-  (Document_Antiquotation.setup \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
-    (fn {context = ctxt, ...} => fn (name, pos) =>
-      (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)];
-       enclose "\\url{" "}" name)));
+  (Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
+    (fn ctxt => fn (url, pos) =>
+      let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
+      in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
 
 
 (* doc entries *)
 
 val _ = Theory.setup
-  (Document_Antiquotation.setup \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
-    (fn {context = ctxt, ...} => fn (name, pos) =>
-      (Context_Position.report ctxt pos (Markup.doc name);
-        Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
+  (Thy_Output.antiquotation_pretty \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
+    (fn ctxt => fn (name, pos) =>
+      let val _ = Context_Position.report ctxt pos (Markup.doc name)
+      in [Thy_Output.pretty_text ctxt name] end));
 
 
 (* formal entities *)
 
-fun entity_antiquotation name check output =
-  Document_Antiquotation.setup name (Scan.lift (Parse.position Args.name))
-    (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
+local
+
+fun entity_antiquotation name check bg en =
+  Thy_Output.antiquotation_raw name (Scan.lift (Parse.position Args.name))
+    (fn ctxt => fn (name, pos) =>
+      let val _ = check ctxt (name, pos)
+      in Latex.enclose_block bg en [Latex.string (Output.output name)] end);
+
+in
 
 val _ =
   Theory.setup
-   (entity_antiquotation \<^binding>\<open>command\<close> Outer_Syntax.check_command
-     (enclose "\\isacommand{" "}" o Output.output) #>
-    entity_antiquotation \<^binding>\<open>method\<close> Method.check_name
-     (enclose "\\isa{" "}" o Output.output) #>
-    entity_antiquotation \<^binding>\<open>attribute\<close> Attrib.check_name
-     (enclose "\\isa{" "}" o Output.output));
+   (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{" "}");
 
 end;
+
+end;

--- a/src/Pure/Thy/thy_output.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -15,12 +15,21 @@
   val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
-  val str_of_source: Token.src -> string
-  val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
-    Token.src -> 'a list -> Pretty.T list
-  val string_of_margin: Proof.context -> Pretty.T -> string
-  val output: Proof.context -> Pretty.T list -> string
-  val verbatim_text: Proof.context -> string -> string
+  val lines: 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 typewriter: Proof.context -> string -> Latex.text
+  val verbatim: Proof.context -> string -> Latex.text
+  val pretty: Proof.context -> Pretty.T list -> Latex.text
+  val pretty_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
+  val antiquotation_pretty:
+    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory
+  val antiquotation_pretty_source:
+    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T list) -> theory -> theory
+  val antiquotation_raw:
+    binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
+  val antiquotation_verbatim:
+    binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -35,9 +44,7 @@
 
     val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
 
-    val output_antiquotes =
-      map (fn ant =>
-        Latex.text (Document_Antiquotation.evaluate ctxt ant, #1 (Antiquote.range [ant])));
+    val output_antiquotes = maps (Document_Antiquotation.evaluate ctxt);
 
     fun output_line line =
       (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
@@ -60,7 +67,7 @@
       in output_blocks blocks end
     else
       let
-        val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
+        val ants = Antiquote.parse 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
@@ -421,58 +428,63 @@
 
 (** standard output operations **)
 
-(* basic pretty printing *)
-
-fun perhaps_trim ctxt =
-  not (Config.get ctxt Document_Antiquotation.thy_output_display) ? Symbol.trim_blanks;
+(* pretty printing *)
 
 fun pretty_text ctxt =
-  Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines;
+  Pretty.chunks o map (Pretty.str o Document_Antiquotation.trim_blanks ctxt) o split_lines;
 
-fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
+fun pretty_term ctxt t =
+  Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
 
 (* default output *)
 
-val str_of_source = space_implode " " o map Token.unparse o Token.args_of_src;
+val lines = separate (Latex.string "\\isasep\\isanewline%\n");
 
-fun maybe_pretty_source pretty ctxt src xs =
-  map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
-  |> (if Config.get ctxt Document_Antiquotation.thy_output_source
-      then K [pretty_text ctxt (str_of_source src)] else I);
-
-fun string_of_margin ctxt =
-  Pretty.string_of_margin (Config.get ctxt Document_Antiquotation.thy_output_margin);
+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);
 
-fun output ctxt prts =
-  prts
-  |> Config.get ctxt Document_Antiquotation.thy_output_quotes ? map Pretty.quote
-  |> (if Config.get ctxt Document_Antiquotation.thy_output_display then
-        map (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent)
-          #> string_of_margin ctxt #> Output.output)
-        #> space_implode "\\isasep\\isanewline%\n"
-        #> Latex.environment "isabelle"
-      else
-        map
-          ((if Config.get ctxt Document_Antiquotation.thy_output_break
-            then string_of_margin ctxt else Pretty.unformatted_string_of) #> Output.output)
-        #> space_implode "\\isasep\\isanewline%\n"
-        #> enclose "\\isa{" "}");
+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);
+
+fun typewriter ctxt 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;
 
 
-(* verbatim text *)
+(* pretty output *)
+
+fun pretty ctxt =
+  map (Document_Antiquotation.output ctxt #> Latex.string) #> lines #> isabelle ctxt;
+
+fun pretty_source ctxt src prts =
+  if Config.get ctxt Document_Antiquotation.thy_output_source then
+    pretty ctxt [pretty_text ctxt (space_implode " " (map Token.unparse (Token.args_of_src src)))]
+  else pretty ctxt prts;
 
-fun verbatim_text ctxt =
-  if Config.get ctxt Document_Antiquotation.thy_output_display then
-    split_lines #>
-    map (prefix (Symbol.spaces (Config.get ctxt Document_Antiquotation.thy_output_indent))) #>
-    cat_lines #>
-    Latex.output_ascii #> Latex.environment "isabellett"
-  else
-    split_lines #>
-    map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
-    space_implode "\\isasep\\isanewline%\n";
+fun antiquotation_pretty name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
+
+fun antiquotation_pretty_source name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
+
+fun antiquotation_raw name scan f =
+  Document_Antiquotation.setup name scan
+    (fn {context = ctxt, argument = x, ...} => f ctxt x);
+
+fun antiquotation_verbatim name scan f =
+  antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
 
 end;

--- a/src/Pure/Tools/jedit.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Pure/Tools/jedit.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -75,10 +75,14 @@
 
 val _ =
   Theory.setup
-    (Document_Antiquotation.setup \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
-      (fn {context = ctxt, ...} => fn (name, pos) =>
-       (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
-        Thy_Output.verbatim_text ctxt name)));
+    (Thy_Output.antiquotation_verbatim \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
+      (fn ctxt => fn (name, pos) =>
+        let
+          val _ =
+            if Context_Position.is_reported ctxt pos
+            then ignore (check_action (name, pos))
+            else ();
+        in name end));
 
 end;
 

--- a/src/Pure/Tools/rail.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Pure/Tools/rail.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -17,7 +17,7 @@
     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 -> string
+  val output_rules: Proof.context -> (string Antiquote.antiquote * rail) list -> Latex.text
 end;
 
 structure Rail: RAIL =
@@ -339,7 +339,8 @@
 
 fun output_rules ctxt rules =
   let
-    val output_antiq = Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
+    val output_antiq =
+      Latex.output_text o Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
     fun output_text b s =
       Output.output s
       |> b ? enclose "\\isakeyword{" "}"
@@ -378,11 +379,11 @@
         output "" rail' ^
         "\\rail@end\n"
       end;
-  in Latex.environment "railoutput" (implode (map output_rule rules)) end;
+  in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end;
 
 val _ = Theory.setup
-  (Document_Antiquotation.setup \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
-    (fn {context = ctxt, ...} => output_rules ctxt o read ctxt));
+  (Thy_Output.antiquotation_raw \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
+    (fn ctxt => output_rules ctxt o read ctxt));
 
 end;
 

--- a/src/Tools/Code/code_target.ML	Thu Jan 18 21:29:28 2018 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Jan 18 21:41:30 2018 +0100
@@ -510,14 +510,15 @@
 in
 
 val _ = Theory.setup
-  (Document_Antiquotation.setup @{binding code_stmts}
+  (Thy_Output.antiquotation_raw @{binding code_stmts}
     (parse_const_terms --
       Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
       -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
-    (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
-        present_code ctxt (mk_cs ctxt)
+    (fn ctxt => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
+      Latex.string
+        (present_code ctxt (mk_cs ctxt)
           (maps (fn f => f ctxt) mk_stmtss)
-          target_name some_width "Example" []));
+          target_name some_width "Example" [])));
 
 end;