support for index entries;

--- a/lib/texinputs/isabelle.sty	Thu May 20 13:56:45 2021 +0200
+++ b/lib/texinputs/isabelle.sty	Thu May 20 18:16:13 2021 +0200
@@ -173,6 +173,12 @@
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
+% index entries
+
+\newcommand{\isaindexdef}[1]{\textbf{#1}}
+\newcommand{\isaindexref}[1]{#1}
+
+
 % styles
 
 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}

--- a/src/Pure/Thy/document_antiquotations.ML	Thu May 20 13:56:45 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu May 20 18:16:13 2021 +0200
@@ -148,6 +148,30 @@
 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

--- a/src/Pure/Thy/latex.ML	Thu May 20 13:56:45 2021 +0200
+++ b/src/Pure/Thy/latex.ML	Thu May 20 18:16:13 2021 +0200
@@ -1,7 +1,7 @@
 (*  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 =
@@ -29,6 +29,11 @@
   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
@@ -47,6 +52,9 @@
 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
@@ -243,6 +251,28 @@
 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";