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,242 +1,275 @@
 (*  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 read_antiq: Proof.context -> Antiquote.antiq ->
-    ((string * Position.T) * string) list * Token.src
   val evaluate: (Symbol_Pos.T list -> Latex.text list) -> Proof.context ->
     Antiquote.text_antiquote -> Latex.text list
+  val approx_content: Proof.context -> Input.source -> 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
 
 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 txt =
+  let
+    val pos = Input.pos_of txt;
+    val syms = Input.source_explode txt;
+    val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
+  in ants |> maps (strip_antiq ctxt) |> map strip_symbol |> implode end;
+
+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,401 +1,370 @@
 (*  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)));
 
 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 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) =
-      Document_Antiquotation.read_antiq ctxt antiq |> #2 |> tl
-      |> maps (Symbol.explode o Token.content_of);
-
-in
-
-fun clean_text ctxt txt =
-  let
-    val pos = Input.pos_of txt;
-    val syms = Input.source_explode txt;
-    val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms);
-  in ants |> maps (strip_antiq ctxt) |> map strip_symbol |> implode end;
-
-end;
-
-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 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 => clean_text ctxt txt);
+              | NONE => Document_Antiquotation.approx_content ctxt 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 ml_text name ml =
   Document_Output.antiquotation_verbatim_embedded 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 #1 (Input.source_content text) end);
 
 fun ml_enclose bg en source =
   ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;
 
 val _ = Theory.setup
  (ml_text \<^binding>\<open>ML\<close> (ml_enclose "fn _ => (" ");") #>
   ml_text \<^binding>\<open>ML_op\<close> (ml_enclose "fn _ => (op " ");") #>
   ml_text \<^binding>\<open>ML_type\<close> (ml_enclose "val _ = NONE : (" ") option;") #>
   ml_text \<^binding>\<open>ML_structure\<close>
     (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
 
   ml_text \<^binding>\<open>ML_functor\<close>   (* FIXME formal treatment of functor name (!?) *)
     (fn source =>
       ML_Lex.read ("ML_Env.check_functor " ^
         ML_Syntax.print_string (#1 (Input.source_content source)))) #>
 
   ml_text \<^binding>\<open>ML_text\<close> (K []));
 
 in 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));
 
 
 (* 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);
 
 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;