clarified modules;

--- a/src/Doc/Main/Main_Doc.thy	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Doc/Main/Main_Doc.thy	Tue Jan 09 15:40:12 2018 +0100
@@ -10,7 +10,7 @@
        else error "term_type_only: type mismatch";
        Syntax.pretty_typ ctxt T)
   in
-    Thy_Output.antiquotation @{binding term_type_only}
+    Document_Antiquotation.setup @{binding term_type_only}
       (Args.term -- Args.typ_abbrev)
       (fn {source, context = ctxt, ...} => fn arg =>
         Thy_Output.output ctxt
@@ -18,7 +18,7 @@
   end
 \<close>
 setup \<open>
-  Thy_Output.antiquotation @{binding expanded_typ} (Args.typ >> single)
+  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)
 \<close>

--- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Tue Jan 09 15:40:12 2018 +0100
@@ -51,7 +51,7 @@
             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end
   in
-    Thy_Output.antiquotation @{binding "const_typ"}
+    Document_Antiquotation.setup @{binding "const_typ"}
      (Scan.lift Args.embedded_inner_syntax)
        (fn {source = src, context = ctxt, ...} => fn arg =>
           Thy_Output.output ctxt

--- a/src/Doc/antiquote_setup.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -73,7 +73,7 @@
 fun prep_ml source =
   (Input.source_content source, ML_Lex.read_source false source);
 
-fun index_ml name kind ml = Thy_Output.antiquotation name
+fun index_ml name kind ml = Document_Antiquotation.setup name
   (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
   (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
     let
@@ -119,17 +119,18 @@
 (* named theorems *)
 
 val _ =
-  Theory.setup (Thy_Output.antiquotation @{binding named_thms}
+  Theory.setup (Document_Antiquotation.setup @{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 Thy_Output.quotes then map (apfst Pretty.quote) else I)
-      #> (if Config.get ctxt Thy_Output.display
+      #> (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 Thy_Output.indent) p)) ^
+                  (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"
@@ -160,7 +161,7 @@
 val arg = enclose "{" "}" o clean_string;
 
 fun entity check markup binding index =
-  Thy_Output.antiquotation
+  Document_Antiquotation.setup
     (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))
@@ -204,8 +205,8 @@
     entity_antiqs no_check "" @{binding fact} #>
     entity_antiqs no_check "" @{binding variable} #>
     entity_antiqs no_check "" @{binding case} #>
-    entity_antiqs Thy_Output.check_command "" @{binding antiquotation} #>
-    entity_antiqs Thy_Output.check_option "" @{binding antiquotation_option} #>
+    entity_antiqs Document_Antiquotation.check "" @{binding antiquotation} #>
+    entity_antiqs Document_Antiquotation.check_option "" @{binding antiquotation_option} #>
     entity_antiqs no_check "isasystem" @{binding setting} #>
     entity_antiqs check_system_option "isasystem" @{binding system_option} #>
     entity_antiqs no_check "" @{binding inference} #>

--- a/src/Doc/more_antiquote.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Doc/more_antiquote.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -20,7 +20,7 @@
 in
 
 val _ =
-  Theory.setup (Thy_Output.antiquotation @{binding class_spec} (Scan.lift Args.name)
+  Theory.setup (Document_Antiquotation.setup @{binding class_spec} (Scan.lift Args.name)
     (fn {context, ...} => class_spec context));
 
 end;
@@ -53,7 +53,7 @@
 in
 
 val _ =
-  Theory.setup (Thy_Output.antiquotation @{binding code_thms} Args.term
+  Theory.setup (Document_Antiquotation.setup @{binding code_thms} Args.term
     (fn {context, ...} => pretty_code_thm context));
 
 end;

--- a/src/HOL/Library/LaTeXsugar.thy	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Tue Jan 09 15:40:12 2018 +0100
@@ -104,7 +104,7 @@
             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end
   in
-    Thy_Output.antiquotation @{binding "const_typ"}
+    Document_Antiquotation.setup @{binding "const_typ"}
      (Scan.lift Args.embedded_inner_syntax)
        (fn {source = src, context = ctxt, ...} => fn arg =>
           Thy_Output.output ctxt

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -983,7 +983,7 @@
   end;
 
 fun fp_antiquote_setup binding =
-  Thy_Output.antiquotation binding (Args.type_name {proper = true, strict = true})
+  Document_Antiquotation.setup binding (Args.type_name {proper = true, strict = true})
     (fn {source = src, context = 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)

--- a/src/HOL/Tools/value_command.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/HOL/Tools/value_command.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -73,7 +73,7 @@
       >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t)));
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation \<^binding>\<open>value\<close>
+  (Document_Antiquotation.setup \<^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

--- a/src/Pure/PIDE/resources.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Pure/PIDE/resources.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -257,13 +257,13 @@
 in
 
 val _ = Theory.setup
- (Thy_Output.antiquotation \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
+ (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) #>
-  Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
+  Document_Antiquotation.setup \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
     (document_antiq check_path o #context) #>
-  Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
+  Document_Antiquotation.setup \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
     (document_antiq check_file o #context) #>
-  Thy_Output.antiquotation \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
+  Document_Antiquotation.setup \<^binding>\<open>dir\<close> (Scan.lift (Parse.position Parse.path))
     (document_antiq check_dir o #context) #>
   ML_Antiquotation.value \<^binding>\<open>path\<close>
     (Args.context -- Scan.lift (Parse.position Parse.path) >> uncurry (ML_antiq check_path)) #>

--- a/src/Pure/Pure.thy	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Pure/Pure.thy	Tue Jan 09 15:40:12 2018 +0100
@@ -1145,7 +1145,7 @@
   Outer_Syntax.command \<^command_keyword>\<open>print_antiquotations\<close>
     "print document antiquotations"
     (Parse.opt_bang >> (fn b =>
-      Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
+      Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_ML_antiquotations\<close>

--- a/src/Pure/ROOT.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Pure/ROOT.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -281,6 +281,7 @@
 ML_file "Thy/term_style.ML";
 ML_file "Isar/outer_syntax.ML";
 ML_file "ML/ml_antiquotations.ML";
+ML_file "Thy/document_antiquotation.ML";
 ML_file "Thy/thy_output.ML";
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";

--- a/src/Pure/Thy/bibtex.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Pure/Thy/bibtex.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -40,8 +40,8 @@
 
 val _ =
   Theory.setup
-   (Thy_Output.add_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
-    Thy_Output.antiquotation \<^binding>\<open>cite\<close>
+   (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro) #>
+    Document_Antiquotation.setup \<^binding>\<open>cite\<close>
       (Scan.lift
         (Scan.option (Parse.verbatim || Parse.cartouche) --
          Parse.and_list1 (Parse.position Args.name)))

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/document_antiquotation.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -0,0 +1,184 @@
+(*  Title:      Pure/Thy/document_antiquotation.ML
+    Author:     Makarius
+
+Document antiquotations.
+*)
+
+signature DOCUMENT_ANTIQUOTATION =
+sig
+  val thy_output_display: 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_break: bool Config.T
+  val thy_output_modes: string Config.T
+  val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
+  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
+  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
+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_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_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
+
+
+structure Wrappers = Proof_Data
+(
+  type T = ((unit -> string) -> unit -> string) list;
+  fun init _ = [];
+);
+
+fun add_wrapper wrapper = Wrappers.map (cons wrapper);
+
+val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
+
+
+(* theory data *)
+
+structure Data = Theory_Data
+(
+  type T =
+    (Token.src -> Proof.context -> string) 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 setup name scan body thy =
+  let
+    fun cmd src ctxt =
+      let val (x, ctxt') = Token.syntax scan src ctxt
+      in body {source = src, context = ctxt'} 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
+  |> Data.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> #2));
+
+
+(* syntax *)
+
+local
+
+val property =
+  Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
+
+val properties =
+  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
+
+in
+
+val antiq =
+  Parse.!!!
+    (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
+  >> (fn ((name, props), args) => (props, name :: args));
+
+end;
+
+
+(* evaluate *)
+
+local
+
+fun command src ctxt =
+  let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
+  in f 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 (opts, src) =
+  let
+    val preview_ctxt = fold option opts ctxt;
+    val print_ctxt = Context_Position.set_visible false preview_ctxt;
+
+    fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
+    val _ = cmd preview_ctxt;
+    val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
+  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
+
+in
+
+fun evaluate _ (Antiquote.Text ss) = Symbol_Pos.content 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, ...}) =
+      let val keywords = Thy_Header.get_keywords' ctxt;
+      in eval ctxt (Token.read_antiq keywords antiq (body, pos)) end;
+
+end;
+
+
+(* option syntax *)
+
+fun boolean "" = true
+  | boolean "true" = true
+  | boolean "false" = false
+  | boolean s = error ("Bad boolean value: " ^ quote s);
+
+fun integer s =
+  let
+    fun int ss =
+      (case Library.read_int ss of (i, []) => i
+      | _ => error ("Bad integer value: " ^ 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>quotes\<close> (Config.put thy_output_quotes o boolean) #>
+  setup_option \<^binding>\<open>mode\<close> (add_wrapper o Print_Mode.with_modes o single) #>
+  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>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
+
+end;

--- a/src/Pure/Thy/document_antiquotations.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -7,12 +7,99 @@
 structure Document_Antiquotations: sig end =
 struct
 
+(* basic entities *)
+
+local
+
+fun pretty_term_style ctxt (style, t: term) =
+  Thy_Output.pretty_term ctxt (style t);
+
+fun pretty_thm_style ctxt (style, th) =
+  Thy_Output.pretty_term ctxt (style (Thm.full_prop_of th));
+
+fun pretty_term_typ ctxt (style, t: term) =
+  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) =
+  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'], _) = Variable.import_terms true [t] ctxt;
+  in Thy_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' = Variable.auto_fixes 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 o Locale.extern thy o Locale.check thy) (name, pos) end;
+
+fun pretty_class ctxt =
+  Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
+
+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_clean_proof_of ctxt full;
+
+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);
+
+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));
+
+fun basic_entity name scan = basic_entities name (scan >> single);
+
+in
+
+val _ = Theory.setup
+ (basic_entities_style \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
+  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 (Parse.position Args.name)) 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) pretty_type #>
+  basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
+  basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
+  basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory);
+
+end;
+
+
 (* Markdown errors *)
 
 local
 
 fun markdown_error binding =
-  Thy_Output.antiquotation binding (Scan.succeed ())
+  Document_Antiquotation.setup binding (Scan.succeed ())
     (fn {source, ...} => fn _ =>
       error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
         Position.here (Position.no_range_position (#1 (Token.range_of source)))))
@@ -32,10 +119,14 @@
 
 val _ =
   Theory.setup
-   (Thy_Output.antiquotation \<^binding>\<open>noindent\<close> (Scan.succeed ()) (K (K "\\noindent")) #>
-    Thy_Output.antiquotation \<^binding>\<open>smallskip\<close> (Scan.succeed ()) (K (K "\\smallskip")) #>
-    Thy_Output.antiquotation \<^binding>\<open>medskip\<close> (Scan.succeed ()) (K (K "\\medskip")) #>
-    Thy_Output.antiquotation \<^binding>\<open>bigskip\<close> (Scan.succeed ()) (K (K "\\bigskip")));
+   (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")));
 
 
 (* control style *)
@@ -43,7 +134,7 @@
 local
 
 fun control_antiquotation name s1 s2 =
-  Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
+  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});
 
@@ -63,7 +154,7 @@
 local
 
 fun text_antiquotation name =
-  Thy_Output.antiquotation name (Scan.lift Args.text_input)
+  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));
@@ -83,7 +174,7 @@
 
 val _ =
   Theory.setup
-    (Thy_Output.antiquotation \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
+    (Document_Antiquotation.setup \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
       (fn {context = ctxt, ...} => fn source =>
         let
           val _ =
@@ -93,16 +184,18 @@
           val keywords = Thy_Header.get_keywords' ctxt;
           val toks =
             Input.source_explode source
-            |> not (Config.get ctxt Thy_Output.display) ? Symbol_Pos.trim_lines
+            |> not (Config.get ctxt Document_Antiquotation.thy_output_display) ?
+                Symbol_Pos.trim_lines
             |> 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 Thy_Output.indent) Symbol.space);
+            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 Thy_Output.display then
+           (if Config.get ctxt Document_Antiquotation.thy_output_display then
               split_lines #> map (prefix indentation) #> cat_lines #>
               Latex.environment "isabelle"
             else enclose "\\isa{" "}")
@@ -113,7 +206,7 @@
 
 local
 
-fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ())
+fun goal_state name main = Document_Antiquotation.setup name (Scan.succeed ())
   (fn {context = ctxt, ...} => fn () =>
     Thy_Output.output ctxt
       [Goal_Display.pretty_goal
@@ -132,7 +225,7 @@
 (* embedded lemma *)
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation \<^binding>\<open>lemma\<close>
+  (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)) =>
@@ -157,7 +250,7 @@
 
 val _ =
   Theory.setup
-    (Thy_Output.antiquotation \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
+    (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));
@@ -168,7 +261,7 @@
 
 local
 
-fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input)
+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)));
@@ -198,7 +291,7 @@
 (* URLs *)
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation \<^binding>\<open>url\<close> (Scan.lift (Parse.position Parse.embedded))
+  (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)));
@@ -207,7 +300,7 @@
 (* doc entries *)
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
+  (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])));
@@ -216,7 +309,7 @@
 (* formal entities *)
 
 fun entity_antiquotation name check output =
-  Thy_Output.antiquotation name (Scan.lift (Parse.position Args.name))
+  Document_Antiquotation.setup name (Scan.lift (Parse.position Args.name))
     (fn {context = ctxt, ...} => fn (name, pos) => (check ctxt (name, pos); output name));
 
 val _ =

--- a/src/Pure/Thy/thy_output.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -1,28 +1,11 @@
 (*  Title:      Pure/Thy/thy_output.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-Theory document output with antiquotations.
+Theory document output.
 *)
 
 signature THY_OUTPUT =
 sig
-  val display: bool Config.T
-  val quotes: bool Config.T
-  val margin: int Config.T
-  val indent: int Config.T
-  val source: bool Config.T
-  val break: bool Config.T
-  val modes: string Config.T
-  val add_wrapper: ((unit -> string) -> unit -> string) -> Proof.context -> Proof.context
-  val add_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
-  val check_command: Proof.context -> xstring * Position.T -> string
-  val check_option: Proof.context -> xstring * Position.T -> string
-  val print_antiquotations: bool -> Proof.context -> unit
-  val antiquotation: binding -> 'a context_parser ->
-    ({source: Token.src, context: Proof.context} -> 'a -> string) -> theory -> theory
-  val boolean: string -> bool
-  val integer: string -> int
-  val eval_antiquote: Proof.context -> Antiquote.text_antiquote -> string
   val output_text: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val check_token_comments: Proof.context -> Token.T -> unit
@@ -43,152 +26,6 @@
 structure Thy_Output: THY_OUTPUT =
 struct
 
-(** options **)
-
-val display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
-val break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
-val quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
-val margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
-val indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
-val source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
-val modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
-
-
-structure Wrappers = Proof_Data
-(
-  type T = ((unit -> string) -> unit -> string) list;
-  fun init _ = [];
-);
-
-fun add_wrapper wrapper = Wrappers.map (cons wrapper);
-
-val wrap = Wrappers.get #> fold (fn wrapper => fn f => wrapper f);
-
-
-
-(** maintain global antiquotations **)
-
-structure Antiquotations = Theory_Data
-(
-  type T =
-    (Token.src -> Proof.context -> string) 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 = Antiquotations.get o Proof_Context.theory_of;
-
-fun add_command name cmd thy = thy
-  |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
-
-fun add_option name opt thy = thy
-  |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
-
-fun check_command 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 command src ctxt =
-  let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
-  in f 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 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 antiquotation name scan body =
-  add_command name
-    (fn src => fn ctxt =>
-      let val (x, ctxt') = Token.syntax scan src ctxt
-      in body {source = src, context = ctxt'} x end);
-
-
-
-(** syntax of antiquotations **)
-
-(* option values *)
-
-fun boolean "" = true
-  | boolean "true" = true
-  | boolean "false" = false
-  | boolean s = error ("Bad boolean value: " ^ quote s);
-
-fun integer s =
-  let
-    fun int ss =
-      (case Library.read_int ss of (i, []) => i
-      | _ => error ("Bad integer value: " ^ quote s));
-  in (case Symbol.explode s of "-" :: ss => ~ (int ss) | ss => int ss) end;
-
-
-(* outer syntax *)
-
-local
-
-val property =
-  Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
-
-val properties =
-  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
-
-in
-
-val antiq =
-  Parse.!!!
-    (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
-  >> (fn ((name, props), args) => (props, name :: args));
-
-end;
-
-
-(* eval antiquote *)
-
-local
-
-fun eval_antiq ctxt (opts, src) =
-  let
-    val preview_ctxt = fold option opts ctxt;
-    val print_ctxt = Context_Position.set_visible false preview_ctxt;
-
-    fun cmd ctxt = wrap ctxt (fn () => command src ctxt) ();
-    val _ = cmd preview_ctxt;
-    val print_modes = space_explode "," (Config.get print_ctxt modes) @ [Latex.latexN];
-  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
-
-in
-
-fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
-  | eval_antiquote ctxt (Antiquote.Control {name, body, ...}) =
-      eval_antiq ctxt
-        ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
-  | eval_antiquote ctxt (Antiquote.Antiq {range = (pos, _), body, ...}) =
-      let val keywords = Thy_Header.get_keywords' ctxt;
-      in eval_antiq ctxt (Token.read_antiq keywords antiq (body, pos)) end;
-
-end;
-
-
-
-(** document output **)
-
 (* output text *)
 
 fun output_text ctxt {markdown} source =
@@ -199,7 +36,8 @@
     val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
 
     val output_antiquotes =
-      map (fn ant => Latex.text (eval_antiquote ctxt ant, #1 (Antiquote.range [ant])));
+      map (fn ant =>
+        Latex.text (Document_Antiquotation.evaluate ctxt ant, #1 (Antiquote.range [ant])));
 
     fun output_line line =
       (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @
@@ -572,34 +410,12 @@
 
 
 
-(** setup default output **)
-
-(* options *)
-
-val _ = Theory.setup
- (add_option \<^binding>\<open>show_types\<close> (Config.put show_types o boolean) #>
-  add_option \<^binding>\<open>show_sorts\<close> (Config.put show_sorts o boolean) #>
-  add_option \<^binding>\<open>show_structs\<close> (Config.put show_structs o boolean) #>
-  add_option \<^binding>\<open>show_question_marks\<close> (Config.put show_question_marks o boolean) #>
-  add_option \<^binding>\<open>show_abbrevs\<close> (Config.put show_abbrevs o boolean) #>
-  add_option \<^binding>\<open>names_long\<close> (Config.put Name_Space.names_long o boolean) #>
-  add_option \<^binding>\<open>names_short\<close> (Config.put Name_Space.names_short o boolean) #>
-  add_option \<^binding>\<open>names_unique\<close> (Config.put Name_Space.names_unique o boolean) #>
-  add_option \<^binding>\<open>eta_contract\<close> (Config.put Syntax_Trans.eta_contract o boolean) #>
-  add_option \<^binding>\<open>display\<close> (Config.put display o boolean) #>
-  add_option \<^binding>\<open>break\<close> (Config.put break o boolean) #>
-  add_option \<^binding>\<open>quotes\<close> (Config.put quotes o boolean) #>
-  add_option \<^binding>\<open>mode\<close> (add_wrapper o Print_Mode.with_modes o single) #>
-  add_option \<^binding>\<open>margin\<close> (Config.put margin o integer) #>
-  add_option \<^binding>\<open>indent\<close> (Config.put indent o integer) #>
-  add_option \<^binding>\<open>source\<close> (Config.put source o boolean) #>
-  add_option \<^binding>\<open>goals_limit\<close> (Config.put Goal_Display.goals_limit o integer));
-
+(** standard output operations **)
 
 (* basic pretty printing *)
 
 fun perhaps_trim ctxt =
-  not (Config.get ctxt display) ? Symbol.trim_blanks;
+  not (Config.get ctxt Document_Antiquotation.thy_output_display) ? Symbol.trim_blanks;
 
 fun pretty_text ctxt =
   Pretty.chunks o map Pretty.str o map (perhaps_trim ctxt) o split_lines;
@@ -608,55 +424,6 @@
 
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
-fun pretty_term_style ctxt (style, t) =
-  pretty_term ctxt (style t);
-
-fun pretty_thm_style ctxt (style, th) =
-  pretty_term ctxt (style (Thm.full_prop_of th));
-
-fun pretty_term_typ ctxt (style, t) =
-  let val t' = style t
-  in pretty_term ctxt (Type.constraint (Term.fastype_of t') t') end;
-
-fun pretty_term_typeof ctxt (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'], _) = Variable.import_terms true [t] ctxt;
-  in 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' = Variable.auto_fixes 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 o Locale.extern thy o Locale.check thy) (name, pos) end;
-
-fun pretty_class ctxt =
-  Pretty.str o Proof_Context.extern_class ctxt o Proof_Context.read_class ctxt;
-
-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_clean_proof_of ctxt full;
-
-fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
-
 
 (* default output *)
 
@@ -664,21 +431,24 @@
 
 fun maybe_pretty_source pretty ctxt src xs =
   map (pretty ctxt) xs  (*always pretty in order to exhibit errors!*)
-  |> (if Config.get ctxt source then K [pretty_text ctxt (str_of_source src)] else I);
+  |> (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 margin);
+fun string_of_margin ctxt =
+  Pretty.string_of_margin (Config.get ctxt Document_Antiquotation.thy_output_margin);
 
 fun output ctxt prts =
   prts
-  |> Config.get ctxt quotes ? map Pretty.quote
-  |> (if Config.get ctxt display then
-        map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output)
+  |> 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 break then string_of_margin ctxt else Pretty.unformatted_string_of)
-            #> Output.output)
+          ((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{" "}");
 
@@ -686,48 +456,14 @@
 (* verbatim text *)
 
 fun verbatim_text ctxt =
-  if Config.get ctxt display then
-    split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #>
+  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";
 
-
-(* antiquotations for basic entities *)
-
-local
-
-fun basic_entities name scan pretty =
-  antiquotation name scan (fn {source, context = ctxt, ...} =>
-    output ctxt o maybe_pretty_source pretty ctxt source);
-
-fun basic_entities_style name scan pretty =
-  antiquotation name scan (fn {source, context = ctxt, ...} => fn (style, xs) =>
-    output ctxt
-      (maybe_pretty_source (fn ctxt => fn x => pretty ctxt (style, x)) ctxt source xs));
-
-fun basic_entity name scan = basic_entities name (scan >> single);
-
-in
-
-val _ = Theory.setup
- (basic_entities_style \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms) pretty_thm_style #>
-  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 (Parse.position Args.name)) 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) pretty_type #>
-  basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
-  basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
-  basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory);
-
 end;
-
-end;

--- a/src/Pure/Tools/jedit.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Pure/Tools/jedit.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -75,7 +75,7 @@
 
 val _ =
   Theory.setup
-    (Thy_Output.antiquotation \<^binding>\<open>action\<close> (Scan.lift (Parse.position Parse.embedded))
+    (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)));

--- a/src/Pure/Tools/rail.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Pure/Tools/rail.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -332,7 +332,7 @@
 
 fun output_rules ctxt rules =
   let
-    val output_antiq = Thy_Output.eval_antiquote ctxt o Antiquote.Antiq;
+    val output_antiq = Document_Antiquotation.evaluate ctxt o Antiquote.Antiq;
     fun output_text b s =
       Output.output s
       |> b ? enclose "\\isakeyword{" "}"
@@ -374,7 +374,7 @@
   in Latex.environment "railoutput" (implode (map output_rule rules)) end;
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
+  (Document_Antiquotation.setup \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
     (fn {context = ctxt, ...} => output_rules ctxt o read ctxt));
 
 end;

--- a/src/Tools/Code/code_target.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Tools/Code/code_target.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -510,7 +510,7 @@
 in
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation @{binding code_stmts}
+  (Document_Antiquotation.setup @{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)))