diff --git a/lib/texinputs/isabelle.sty b/lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty
+++ b/lib/texinputs/isabelle.sty
@@ -1,297 +1,303 @@
 %%
 %% macros for Isabelle generated LaTeX output
 %%
 
 %%% Simple document preparation (based on theory token language and symbols)
 
 % isabelle environments
 
 \newcommand{\isabellecontext}{UNKNOWN}
 \newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
 
 \newcommand{\isastyle}{\UNDEF}
 \newcommand{\isastylett}{\UNDEF}
 \newcommand{\isastyleminor}{\UNDEF}
 \newcommand{\isastyleminortt}{\UNDEF}
 \newcommand{\isastylescript}{\UNDEF}
 \newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
 \newcommand{\isastyletxt}{\normalfont\rmfamily}
 \newcommand{\isastylecmt}{\normalfont\rmfamily}
 
 \newcommand{\isaspacing}{%
   \sfcode 42 1000 % .
   \sfcode 63 1000 % ?
   \sfcode 33 1000 % !
   \sfcode 58 1000 % :
   \sfcode 59 1000 % ;
   \sfcode 44 1000 % ,
 }
 
 %symbol markup -- \emph achieves decent spacing via italic corrections
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
 
 %blackboard-bold (requires font txmia from pxfonts)
 \DeclareSymbolFont{bbbfont}{U}{txmia}{m}{it}
 \SetSymbolFont{bbbfont}{bold}{U}{txmia}{bx}{it}
 \DeclareMathSymbol{\bbbA}{\mathord}{bbbfont}{129}
 \DeclareMathSymbol{\bbbB}{\mathord}{bbbfont}{130}
 \DeclareMathSymbol{\bbbC}{\mathord}{bbbfont}{131}
 \DeclareMathSymbol{\bbbD}{\mathord}{bbbfont}{132}
 \DeclareMathSymbol{\bbbE}{\mathord}{bbbfont}{133}
 \DeclareMathSymbol{\bbbF}{\mathord}{bbbfont}{134}
 \DeclareMathSymbol{\bbbG}{\mathord}{bbbfont}{135}
 \DeclareMathSymbol{\bbbH}{\mathord}{bbbfont}{136}
 \DeclareMathSymbol{\bbbI}{\mathord}{bbbfont}{137}
 \DeclareMathSymbol{\bbbJ}{\mathord}{bbbfont}{138}
 \DeclareMathSymbol{\bbbK}{\mathord}{bbbfont}{139}
 \DeclareMathSymbol{\bbbL}{\mathord}{bbbfont}{140}
 \DeclareMathSymbol{\bbbM}{\mathord}{bbbfont}{141}
 \DeclareMathSymbol{\bbbN}{\mathord}{bbbfont}{142}
 \DeclareMathSymbol{\bbbO}{\mathord}{bbbfont}{143}
 \DeclareMathSymbol{\bbbP}{\mathord}{bbbfont}{144}
 \DeclareMathSymbol{\bbbQ}{\mathord}{bbbfont}{145}
 \DeclareMathSymbol{\bbbR}{\mathord}{bbbfont}{146}
 \DeclareMathSymbol{\bbbS}{\mathord}{bbbfont}{147}
 \DeclareMathSymbol{\bbbT}{\mathord}{bbbfont}{148}
 \DeclareMathSymbol{\bbbU}{\mathord}{bbbfont}{149}
 \DeclareMathSymbol{\bbbV}{\mathord}{bbbfont}{150}
 \DeclareMathSymbol{\bbbW}{\mathord}{bbbfont}{151}
 \DeclareMathSymbol{\bbbX}{\mathord}{bbbfont}{152}
 \DeclareMathSymbol{\bbbY}{\mathord}{bbbfont}{153}
 \DeclareMathSymbol{\bbbZ}{\mathord}{bbbfont}{154}
 
 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
 
 \newdimen\isa@parindent\newdimen\isa@parskip
 
 \newenvironment{isabellebody}{%
 \isamarkuptrue\par%
 \isa@parindent\parindent\parindent0pt%
 \isa@parskip\parskip\parskip0pt%
 \isaspacing\isastyle}{\par}
 
 \newenvironment{isabellebodytt}{%
 \isamarkuptrue\par%
 \isa@parindent\parindent\parindent0pt%
 \isa@parskip\parskip\parskip0pt%
 \isaspacing\isastylett}{\par}
 
 \newenvironment{isabelle}
 {\begin{trivlist}\begin{isabellebody}\item\relax}
 {\end{isabellebody}\end{trivlist}}
 
 \newenvironment{isabellett}
 {\begin{trivlist}\begin{isabellebodytt}\item\relax}
 {\end{isabellebodytt}\end{trivlist}}
 
 \newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
 \newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
 
 \newcommand{\isaindent}[1]{\hphantom{#1}}
 \newcommand{\isanewline}{\mbox{}\par\mbox{}}
 \newcommand{\isasep}{}
 \newcommand{\isadigit}[1]{#1}
 
 \newcommand{\isachardefaults}{%
 \def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
 \chardef\isacharbang=`\!%
 \chardef\isachardoublequote=`\"%
 \chardef\isachardoublequoteopen=`\"%
 \chardef\isachardoublequoteclose=`\"%
 \chardef\isacharhash=`\#%
 \chardef\isachardollar=`\$%
 \chardef\isacharpercent=`\%%
 \chardef\isacharampersand=`\&%
 \chardef\isacharprime=`\'%
 \chardef\isacharparenleft=`\(%
 \chardef\isacharparenright=`\)%
 \chardef\isacharasterisk=`\*%
 \chardef\isacharplus=`\+%
 \chardef\isacharcomma=`\,%
 \chardef\isacharminus=`\-%
 \chardef\isachardot=`\.%
 \chardef\isacharslash=`\/%
 \chardef\isacharcolon=`\:%
 \chardef\isacharsemicolon=`\;%
 \chardef\isacharless=`\<%
 \chardef\isacharequal=`\=%
 \chardef\isachargreater=`\>%
 \chardef\isacharquery=`\?%
 \chardef\isacharat=`\@%
 \chardef\isacharbrackleft=`\[%
 \chardef\isacharbackslash=`\\%
 \chardef\isacharbrackright=`\]%
 \chardef\isacharcircum=`\^%
 \chardef\isacharunderscore=`\_%
 \def\isacharunderscorekeyword{\_}%
 \chardef\isacharbackquote=`\`%
 \chardef\isacharbackquoteopen=`\`%
 \chardef\isacharbackquoteclose=`\`%
 \chardef\isacharbraceleft=`\{%
 \chardef\isacharbar=`\|%
 \chardef\isacharbraceright=`\}%
 \chardef\isachartilde=`\~%
 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
 \def\isacartoucheopen{\isatext{\guilsinglleft}}%
 \def\isacartoucheclose{\isatext{\guilsinglright}}%
 }
 
 
 % keyword and section markup
 
 \newcommand{\isakeyword}[1]
 {\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
 \newcommand{\isacommand}[1]{\isakeyword{#1}}
 
 \newcommand{\isakeywordcontrol}[1]
 {\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
 
 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
 \newcommand{\isamarkupsection}[1]{\section{#1}}
 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
 \newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
 \newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
 
 \newif\ifisamarkup
 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
 \newcommand{\isaendpar}{\par\medskip}
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
+% index entries
+
+\newcommand{\isaindexdef}[1]{\textbf{#1}}
+\newcommand{\isaindexref}[1]{#1}
+
+
 % styles
 
 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
 
 \newcommand{\isabellestyledefault}{%
 \def\isastyle{\small\normalfont\ttfamily\slshape}%
 \def\isastylett{\small\normalfont\ttfamily}%
 \def\isastyleminor{\small\normalfont\ttfamily\slshape}%
 \def\isastyleminortt{\small\normalfont\ttfamily}%
 \def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
 \isachardefaults%
 }
 \isabellestyledefault
 
 \newcommand{\isabellestylett}{%
 \def\isastyle{\small\normalfont\ttfamily}%
 \def\isastylett{\small\normalfont\ttfamily}%
 \def\isastyleminor{\small\normalfont\ttfamily}%
 \def\isastyleminortt{\small\normalfont\ttfamily}%
 \def\isastylescript{\footnotesize\normalfont\ttfamily}%
 \isachardefaults%
 }
 
 \newcommand{\isabellestyleit}{%
 \def\isastyle{\small\normalfont\itshape}%
 \def\isastylett{\small\normalfont\ttfamily}%
 \def\isastyleminor{\normalfont\itshape}%
 \def\isastyleminortt{\normalfont\ttfamily}%
 \def\isastylescript{\footnotesize\normalfont\itshape}%
 \isachardefaults%
 \def\isacharunderscorekeyword{\mbox{-}}%
 \def\isacharbang{\isamath{!}}%
 \def\isachardoublequote{}%
 \def\isachardoublequoteopen{}%
 \def\isachardoublequoteclose{}%
 \def\isacharhash{\isamath{\#}}%
 \def\isachardollar{\isamath{\$}}%
 \def\isacharpercent{\isamath{\%}}%
 \def\isacharampersand{\isamath{\&}}%
 \def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
 \def\isacharparenleft{\isamath{(}}%
 \def\isacharparenright{\isamath{)}}%
 \def\isacharasterisk{\isamath{*}}%
 \def\isacharplus{\isamath{+}}%
 \def\isacharcomma{\isamath{\mathord,}}%
 \def\isacharminus{\isamath{-}}%
 \def\isachardot{\isamath{\mathord.}}%
 \def\isacharslash{\isamath{/}}%
 \def\isacharcolon{\isamath{\mathord:}}%
 \def\isacharsemicolon{\isamath{\mathord;}}%
 \def\isacharless{\isamath{<}}%
 \def\isacharequal{\isamath{=}}%
 \def\isachargreater{\isamath{>}}%
 \def\isacharat{\isamath{@}}%
 \def\isacharbrackleft{\isamath{[}}%
 \def\isacharbackslash{\isamath{\backslash}}%
 \def\isacharbrackright{\isamath{]}}%
 \def\isacharunderscore{\mbox{-}}%
 \def\isacharbraceleft{\isamath{\{}}%
 \def\isacharbar{\isamath{\mid}}%
 \def\isacharbraceright{\isamath{\}}}%
 \def\isachartilde{\isamath{{}\sp{\sim}}}%
 \def\isacharbackquoteopen{\isatext{\guilsinglleft}}%
 \def\isacharbackquoteclose{\isatext{\guilsinglright}}%
 }
 
 \newcommand{\isabellestyleliteral}{%
 \isabellestyleit%
 \def\isacharunderscore{\_}%
 \def\isacharunderscorekeyword{\_}%
 \chardef\isacharbackquoteopen=`\`%
 \chardef\isacharbackquoteclose=`\`%
 }
 
 \newcommand{\isabellestyleliteralunderscore}{%
 \isabellestyleliteral%
 \def\isacharunderscore{\textunderscore}%
 \def\isacharunderscorekeyword{\textunderscore}%
 }
 
 \newcommand{\isabellestylesl}{%
 \isabellestyleit%
 \def\isastyle{\small\normalfont\slshape}%
 \def\isastylett{\small\normalfont\ttfamily}%
 \def\isastyleminor{\normalfont\slshape}%
 \def\isastyleminortt{\normalfont\ttfamily}%
 \def\isastylescript{\footnotesize\normalfont\slshape}%
 }
 
 
 % cancel text
 
 \usepackage[normalem]{ulem}
 \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
 
 
 % tagged regions
 
 %plain TeX version of comment package -- much faster!
 \let\isafmtname\fmtname\def\fmtname{plain}
 \usepackage{comment}
 \let\fmtname\isafmtname
 
 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
 
 \newcommand{\isakeeptag}[1]%
 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
 \newcommand{\isadroptag}[1]%
 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
 \newcommand{\isafoldtag}[1]%
 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
 
 \isakeeptag{document}
 \isakeeptag{theory}
 \isakeeptag{proof}
 \isakeeptag{ML}
 \isakeeptag{visible}
 \isadroptag{invisible}
 \isakeeptag{important}
 \isakeeptag{unimportant}
 
 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
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,350 +1,374 @@
 (*  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) =
   Thy_Output.pretty_term ctxt (style t);
 
 fun pretty_thms_style ctxt (style: style, ths) =
   map (fn th => Thy_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 Thy_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 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' = 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 = Thy_Output.antiquotation_pretty_source_embedded;
 
 fun basic_entities name scan pretty =
   Document_Antiquotation.setup name scan
     (fn {context = ctxt, source = src, argument = xs} =>
       Thy_Output.pretty_items_source ctxt {embedded = false} src (map (pretty ctxt) xs));
 
 in
 
 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} =>
       Thy_Output.pretty_items_source ctxt {embedded = false} src (pretty_thms_style ctxt arg)));
 
 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)))))
 
 in
 
 val _ =
   Theory.setup
    (markdown_error \<^binding>\<open>item\<close> #>
     markdown_error \<^binding>\<open>enum\<close> #>
     markdown_error \<^binding>\<open>descr\<close>);
 
 end;
 
 
 (* control spacing *)
 
 val _ =
   Theory.setup
    (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"));
 
 
 (* nested document text *)
 
 local
 
 fun nested_antiquotation name s1 s2 =
   Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
     (fn ctxt => fn txt =>
       (Context_Position.reports ctxt (Thy_Output.document_reports txt);
         Latex.enclose_block s1 s2 (Thy_Output.output_document ctxt {markdown = false} txt)));
 
 in
 
 val _ =
   Theory.setup
    (nested_antiquotation \<^binding>\<open>footnote\<close> "\\footnote{" "}" #>
     nested_antiquotation \<^binding>\<open>emph\<close> "\\emph{" "}" #>
     nested_antiquotation \<^binding>\<open>bold\<close> "\\textbf{" "}");
 
 end;
 
 
+(* index entries *)
+
+local
+
+val index_like = Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "is" |-- Args.name --| Parse.$$$ ")");
+val index_args = Parse.enum1 "!" (Args.embedded_input -- Scan.optional index_like "");
+
+fun output_text ctxt = Latex.block o Thy_Output.output_document ctxt {markdown = false};
+
+fun index binding def =
+  Thy_Output.antiquotation_raw binding (Scan.lift index_args)
+    (fn ctxt => fn args =>
+     (Context_Position.reports ctxt (maps (Thy_Output.document_reports o #1) args);
+      Latex.index_entry
+        {items = map (fn (txt, like) => {text = output_text ctxt txt, like = like}) args,
+         def = def}));
+
+in
+
+val _ = Theory.setup (index \<^binding>\<open>index_ref\<close> false #> index \<^binding>\<open>index_def\<close> true);
+
+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 =
   Thy_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
         |> Thy_Output.output_source ctxt
         |> Thy_Output.isabelle ctxt
       end);
 
 val theory_text_antiquotation =
   Thy_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 (Thy_Output.output_token ctxt)
         |> Thy_Output.isabelle ctxt
       end);
 
 in
 
 val _ =
   Theory.setup
    (text_antiquotation \<^binding>\<open>text\<close> #>
     text_antiquotation \<^binding>\<open>cartouche\<close> #>
     theory_text_antiquotation);
 
 end;
 
 
 (* goal state *)
 
 local
 
 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)))));
 
 in
 
 val _ = Theory.setup
  (goal_state \<^binding>\<open>goals\<close> true #>
   goal_state \<^binding>\<open>subgoals\<close> false);
 
 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
         Thy_Output.pretty_source ctxt {embedded = false}
           [hd src, prop_tok] (Thy_Output.pretty_term ctxt prop)
       end));
 
 
 (* verbatim text *)
 
 val _ = Theory.setup
   (Thy_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
   (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>bash_function\<close>
     (Scan.lift Args.embedded_position) Isabelle_System.check_bash_function);
 
 
 (* system options *)
 
 val _ = Theory.setup
   (Thy_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 =
   Thy_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;
 
 in
 
 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 []));
 
 end;
 
 
 (* URLs *)
 
 val escape_url =
   translate_string (fn c => if c = "%" orelse c = "#" orelse c = "^" then "\\" ^ c else c);
 
 val _ = Theory.setup
   (Thy_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 =
   Thy_Output.antiquotation_raw name (Scan.lift Args.name_position)
     (fn ctxt => fn (name, pos) =>
       let val _ = check ctxt (name, pos)
       in Latex.enclose_block bg en [Latex.string (Output.output name)] end);
 
 in
 
 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{" "}");
 
 end;
 
 end;
diff --git a/src/Pure/Thy/latex.ML b/src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML
+++ b/src/Pure/Thy/latex.ML
@@ -1,268 +1,298 @@
 (*  Title:      Pure/Thy/latex.ML
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
-LaTeX presentation elements -- based on outer lexical syntax.
+LaTeX output of theory sources.
 *)
 
 signature LATEX =
 sig
   type text
   val string: string -> text
   val text: string * Position.T -> text
   val block: text list -> text
   val enclose_body: string -> string -> text list -> text list
   val enclose_block: string -> string -> text list -> text
   val output_text: text list -> string
   val output_positions: Position.T -> text list -> string
   val output_name: string -> string
   val output_ascii: string -> string
   val output_ascii_breakable: string -> string -> string
   val output_symbols: Symbol.symbol list -> string
   val output_syms: string -> string
   val symbols: Symbol_Pos.T list -> text
   val symbols_output: Symbol_Pos.T list -> text
   val begin_delim: string -> string
   val end_delim: string -> string
   val begin_tag: string -> string
   val end_tag: string -> string
   val environment_block: string -> text list -> text
   val environment: string -> string -> string
   val isabelle_body: string -> text list -> text list
   val theory_entry: string -> string
+  val index_escape: string -> string
+  type index_item = {text: text, like: string}
+  val index_item: index_item -> text
+  type index_entry = {items: index_item list, def: bool}
+  val index_entry: index_entry -> text
   val latexN: string
   val latex_output: string -> string * int
   val latex_markup: string * Properties.T -> Markup.output
   val latex_indent: string -> int -> string
 end;
 
 structure Latex: LATEX =
 struct
 
 (* text with positions *)
 
 abstype text = Text of string * Position.T | Block of text list
 with
 
 fun string s = Text (s, Position.none);
 val text = Text;
 val block = Block;
 
+fun map_text f (Text (s, pos)) = Text (f s, pos)
+  | map_text f (Block texts) = Block ((map o map_text) f texts);
+
 fun output_text texts =
   let
     fun output (Text (s, _)) = Buffer.add s
       | output (Block body) = fold output body;
   in Buffer.empty |> fold output texts |> Buffer.content end;
 
 fun output_positions file_pos texts =
   let
     fun position (a, b) = enclose "%:%" "%:%" (a ^ "=" ^ b);
     fun add_position p positions =
       let val s = position (apply2 Value.print_int p)
       in positions |> s <> hd positions ? cons s end;
 
     fun output (Text (s, pos)) (positions, line) =
           let
             val positions' =
               (case Position.line_of pos of
                 NONE => positions
               | SOME l => add_position (line, l) positions);
             val line' = fold_string (fn c => fn n => if c = "\n" then n + 1 else n) s line;
           in (positions', line') end
       | output (Block body) res = fold output body res;
   in
     (case Position.file_of file_pos of
       NONE => ""
     | SOME file =>
         ([position (Markup.fileN, file), "\\endinput"], 1)
         |> fold output texts |> #1 |> rev |> cat_lines)
   end;
 
 end;
 
 fun enclose_body bg en body =
   (if bg = "" then [] else [string bg]) @ body @
   (if en = "" then [] else [string en]);
 
 fun enclose_block bg en = block o enclose_body bg en;
 
 
 (* output name for LaTeX macros *)
 
 val output_name =
   translate_string
     (fn "_" => "UNDERSCORE"
       | "'" => "PRIME"
       | "0" => "ZERO"
       | "1" => "ONE"
       | "2" => "TWO"
       | "3" => "THREE"
       | "4" => "FOUR"
       | "5" => "FIVE"
       | "6" => "SIX"
       | "7" => "SEVEN"
       | "8" => "EIGHT"
       | "9" => "NINE"
       | s => s);
 
 fun enclose_name bg en = enclose bg en o output_name;
 
 
 (* output verbatim ASCII *)
 
 val output_ascii =
   translate_string
     (fn " " => "\\ "
       | "\t" => "\\ "
       | "\n" => "\\isanewline\n"
       | s =>
           s
           |> exists_string (fn s' => s = s') "\"#$%&',-<>\\^_`{}~" ? enclose "{\\char`\\" "}"
           |> suffix "{\\kern0pt}");
 
 fun output_ascii_breakable sep =
   space_explode sep
   #> map output_ascii
   #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
 
 
 (* output symbols *)
 
 local
 
 val char_table =
   Symtab.make
    [("\007", "{\\isacharbell}"),
     ("!", "{\\isacharbang}"),
     ("\"", "{\\isachardoublequote}"),
     ("#", "{\\isacharhash}"),
     ("$", "{\\isachardollar}"),
     ("%", "{\\isacharpercent}"),
     ("&", "{\\isacharampersand}"),
     ("'", "{\\isacharprime}"),
     ("(", "{\\isacharparenleft}"),
     (")", "{\\isacharparenright}"),
     ("*", "{\\isacharasterisk}"),
     ("+", "{\\isacharplus}"),
     (",", "{\\isacharcomma}"),
     ("-", "{\\isacharminus}"),
     (".", "{\\isachardot}"),
     ("/", "{\\isacharslash}"),
     (":", "{\\isacharcolon}"),
     (";", "{\\isacharsemicolon}"),
     ("<", "{\\isacharless}"),
     ("=", "{\\isacharequal}"),
     (">", "{\\isachargreater}"),
     ("?", "{\\isacharquery}"),
     ("@", "{\\isacharat}"),
     ("[", "{\\isacharbrackleft}"),
     ("\\", "{\\isacharbackslash}"),
     ("]", "{\\isacharbrackright}"),
     ("^", "{\\isacharcircum}"),
     ("_", "{\\isacharunderscore}"),
     ("`", "{\\isacharbackquote}"),
     ("{", "{\\isacharbraceleft}"),
     ("|", "{\\isacharbar}"),
     ("}", "{\\isacharbraceright}"),
     ("~", "{\\isachartilde}")];
 
 fun output_chr " " = "\\ "
   | output_chr "\t" = "\\ "
   | output_chr "\n" = "\\isanewline\n"
   | output_chr c =
       (case Symtab.lookup char_table c of
         SOME s => s ^ "{\\kern0pt}"
       | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
 
 fun output_sym sym =
   (case Symbol.decode sym of
     Symbol.Char s => output_chr s
   | Symbol.UTF8 s => s
   | Symbol.Sym s => enclose_name "{\\isasym" "}" s
   | Symbol.Control s => enclose_name "\\isactrl" " " s
   | Symbol.Malformed s => error (Symbol.malformed_msg s)
   | Symbol.EOF => error "Bad EOF symbol");
 
 open Basic_Symbol_Pos;
 
 val scan_latex_length =
   Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s)
     >> (Symbol.length o map Symbol_Pos.symbol) ||
   $$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
 
 val scan_latex =
   $$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: "
     >> (implode o map Symbol_Pos.symbol) ||
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
 
 fun read scan syms =
   Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
 
 in
 
 fun length_symbols syms =
   fold Integer.add (these (read scan_latex_length syms)) 0;
 
 fun output_symbols syms =
   if member (op =) syms Symbol.latex then
     (case read scan_latex syms of
       SOME ss => implode ss
     | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
   else implode (map output_sym syms);
 
 val output_syms = output_symbols o Symbol.explode;
 
 end;
 
 fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
 fun symbols_output syms =
   text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
 
 
 (* tags *)
 
 val begin_delim = enclose_name "%\n\\isadelim" "\n";
 val end_delim = enclose_name "%\n\\endisadelim" "\n";
 val begin_tag = enclose_name "%\n\\isatag" "\n";
 fun end_tag tg = enclose_name "%\n\\endisatag" "\n" tg ^ enclose "{\\isafold" "}%\n" tg;
 
 
 (* theory presentation *)
 
 fun environment_delim name =
  ("%\n\\begin{" ^ output_name name ^ "}%\n",
   "%\n\\end{" ^ output_name name ^ "}");
 
 fun environment_block name = environment_delim name |-> enclose_body #> block;
 fun environment name = environment_delim name |-> enclose;
 
 fun isabelle_body name =
   enclose_body
    ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
    "%\n\\end{isabellebody}%\n";
 
 fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
 
 
+(* index entries *)
+
+type index_item = {text: text, like: string};
+type index_entry = {items: index_item list, def: bool};
+
+val index_escape =
+  translate_string (fn s =>
+    s |> exists_string (fn s' => s = s') "\"\\{}!@|" ? prefix "\"");
+
+fun index_item (item: index_item) =
+  let
+    val like_text =
+      if #like item = "" then []
+      else [string (index_escape (#like item) ^ "@")];
+  in block (like_text @ [map_text index_escape (#text item)]) end;
+
+fun index_entry (entry: index_entry) =
+  (separate (string "!") (map index_item (#items entry)) @
+    [string ("|" ^ index_escape (if #def entry then "isaindexdef" else "isaindexref"))])
+  |> enclose_block "\\index{" "}";
+
+
 (* print mode *)
 
 val latexN = "latex";
 
 fun latex_output str =
   let val syms = Symbol.explode str
   in (output_symbols syms, length_symbols syms) end;
 
 fun latex_markup (s, _: Properties.T) =
   if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
   then ("\\isacommand{", "}")
   else if s = Markup.keyword2N
   then ("\\isakeyword{", "}")
   else Markup.no_output;
 
 fun latex_indent "" _ = ""
   | latex_indent s _ = enclose "\\isaindent{" "}" s;
 
 val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
 val _ = Markup.add_mode latexN latex_markup;
 val _ = Pretty.add_mode latexN latex_indent;
 
 end;