clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
authorwenzelm
Sat, 22 May 2021 13:35:25 +0200
changeset 74019 eccc4a13216d
parent 74018 14841c6e4d5f
child 74020 35d8132633c6
clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
src/Doc/Implementation/Local_Theory.thy
src/Doc/Implementation/Logic.thy
src/Doc/Implementation/ML.thy
src/Doc/Implementation/Prelim.thy
src/Doc/Implementation/Tactic.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/antiquote_setup.ML
src/Pure/Thy/latex.ML
src/Pure/library.ML
--- a/src/Doc/Implementation/Local_Theory.thy	Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Sat May 22 13:35:25 2021 +0200
@@ -90,7 +90,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type local_theory: Proof.context} \\
+  @{index_ML_type local_theory = Proof.context} \\
   @{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex]
   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
--- a/src/Doc/Implementation/Logic.thy	Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sat May 22 13:35:25 2021 +0200
@@ -102,9 +102,9 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type class: string} \\
-  @{index_ML_type sort: "class list"} \\
-  @{index_ML_type arity: "string * sort list * sort"} \\
+  @{index_ML_type class = string} \\
+  @{index_ML_type sort = "class list"} \\
+  @{index_ML_type arity = "string * sort list * sort"} \\
   @{index_ML_type typ} \\
   @{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\
   @{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
@@ -314,7 +314,7 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type term} \\
-  @{index_ML_op "aconv": "term * term -> bool"} \\
+  @{index_ML_infix "aconv": "term * term -> bool"} \\
   @{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
   @{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
   @{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
@@ -336,7 +336,7 @@
   \<^descr> Type \<^ML_type>\<open>term\<close> represents de-Bruijn terms, with comments in
   abstractions, and explicitly named free variables and constants; this is a
   datatype with constructors @{index_ML Bound}, @{index_ML Free}, @{index_ML
-  Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_op "$"}.
+  Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_infix "$"}.
 
   \<^descr> \<open>t\<close>~\<^ML_text>\<open>aconv\<close>~\<open>u\<close> checks \<open>\<alpha>\<close>-equivalence of two terms. This is the
   basic equality relation on type \<^ML_type>\<open>term\<close>; raw datatype equality
@@ -1022,14 +1022,14 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\
-  @{index_ML_op "RS": "thm * thm -> thm"} \\
+  @{index_ML_infix "RSN": "thm * (int * thm) -> thm"} \\
+  @{index_ML_infix "RS": "thm * thm -> thm"} \\
 
-  @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\
-  @{index_ML_op "RL": "thm list * thm list -> thm list"} \\
+  @{index_ML_infix "RLN": "thm list * (int * thm list) -> thm list"} \\
+  @{index_ML_infix "RL": "thm list * thm list -> thm list"} \\
 
-  @{index_ML_op "MRS": "thm list * thm -> thm"} \\
-  @{index_ML_op "OF": "thm * thm list -> thm"} \\
+  @{index_ML_infix "MRS": "thm list * thm -> thm"} \\
+  @{index_ML_infix "OF": "thm * thm list -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<open>rule\<^sub>1 RSN (i, rule\<^sub>2)\<close> resolves the conclusion of \<open>rule\<^sub>1\<close> with the
@@ -1197,8 +1197,8 @@
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>proof\<close> represents proof terms; this is a datatype with
-  constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"},
-  @{index_ML_op "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
+  constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_infix "%"},
+  @{index_ML_infix "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
   Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML PThm} as explained
   above. %FIXME PClass (!?)
 
--- a/src/Doc/Implementation/ML.thy	Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/ML.thy	Sat May 22 13:35:25 2021 +0200
@@ -818,10 +818,10 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\
-  @{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
-  @{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
-  @{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
+  @{index_ML_infix "|>" : "'a * ('a -> 'b) -> 'b"} \\
+  @{index_ML_infix "|->" : "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
+  @{index_ML_infix "#>" : "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
+  @{index_ML_infix "#->" : "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
   \end{mldecls}
 \<close>
 
@@ -1142,8 +1142,8 @@
   \begin{mldecls}
   @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
   @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
-  @{index_ML_exception ERROR: string} \\
-  @{index_ML_exception Fail: string} \\
+  @{index_ML_exception ERROR of string} \\
+  @{index_ML_exception Fail of string} \\
   @{index_ML Exn.is_interrupt: "exn -> bool"} \\
   @{index_ML Exn.reraise: "exn -> 'a"} \\
   @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
@@ -1284,7 +1284,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type "Symbol.symbol": string} \\
+  @{index_ML_type Symbol.symbol = string} \\
   @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
@@ -1596,7 +1596,7 @@
   @{index_ML_type "'a Unsynchronized.ref"} \\
   @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
   @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
-  @{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\
+  @{index_ML_infix ":=" : "'a Unsynchronized.ref * 'a -> unit"} \\
   \end{mldecls}
 \<close>
 
--- a/src/Doc/Implementation/Prelim.thy	Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Sat May 22 13:35:25 2021 +0200
@@ -720,7 +720,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type indexname: "string * int"} \\
+  @{index_ML_type indexname = "string * int"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>indexname\<close> represents indexed names. This is an
--- a/src/Doc/Implementation/Tactic.thy	Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Tactic.thy	Sat May 22 13:35:25 2021 +0200
@@ -156,7 +156,7 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
+  @{index_ML_type tactic = "thm -> thm Seq.seq"} \\
   @{index_ML no_tac: tactic} \\
   @{index_ML all_tac: tactic} \\
   @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
@@ -452,7 +452,7 @@
   \begin{mldecls}
   @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
   @{index_ML Drule.compose: "thm * int * thm -> thm"} \\
-  @{index_ML_op COMP: "thm * thm -> thm"} \\
+  @{index_ML_infix COMP: "thm * thm -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>compose_tac\<close>~\<open>ctxt (flag, rule, m) i\<close> refines subgoal \<open>i\<close> using
@@ -502,15 +502,15 @@
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_op "THEN": "tactic * tactic -> tactic"} \\
-  @{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\
-  @{index_ML_op "APPEND": "tactic * tactic -> tactic"} \\
+  @{index_ML_infix "THEN": "tactic * tactic -> tactic"} \\
+  @{index_ML_infix "ORELSE": "tactic * tactic -> tactic"} \\
+  @{index_ML_infix "APPEND": "tactic * tactic -> tactic"} \\
   @{index_ML "EVERY": "tactic list -> tactic"} \\
   @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
 
-  @{index_ML_op "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
-  @{index_ML_op "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
-  @{index_ML_op "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{index_ML_infix "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{index_ML_infix "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{index_ML_infix "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
   @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
   @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
   \end{mldecls}
--- a/src/Doc/Isar_Ref/Generic.thy	Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Sat May 22 13:35:25 2021 +0200
@@ -909,10 +909,10 @@
   @{index_ML_type solver} \\
   @{index_ML Simplifier.mk_solver: "string ->
   (Proof.context -> int -> tactic) -> solver"} \\
-  @{index_ML_op setSolver: "Proof.context * solver -> Proof.context"} \\
-  @{index_ML_op addSolver: "Proof.context * solver -> Proof.context"} \\
-  @{index_ML_op setSSolver: "Proof.context * solver -> Proof.context"} \\
-  @{index_ML_op addSSolver: "Proof.context * solver -> Proof.context"} \\
+  @{index_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\
+  @{index_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\
+  @{index_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\
+  @{index_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\
   \end{mldecls}
 
   A solver is a tactic that attempts to solve a subgoal after simplification.
@@ -992,12 +992,12 @@
 
 text \<open>
   \begin{mldecls}
-  @{index_ML_op setloop: "Proof.context *
+  @{index_ML_infix setloop: "Proof.context *
   (Proof.context -> int -> tactic) -> Proof.context"} \\
-  @{index_ML_op addloop: "Proof.context *
+  @{index_ML_infix addloop: "Proof.context *
   (string * (Proof.context -> int -> tactic))
   -> Proof.context"} \\
-  @{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\
+  @{index_ML_infix delloop: "Proof.context * string -> Proof.context"} \\
   @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
   @{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
   @{index_ML Splitter.add_split_bang: "
@@ -1624,21 +1624,21 @@
 
 text \<open>
   \begin{mldecls}
-    @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
-    @{index_ML_op addSWrapper: "Proof.context *
+    @{index_ML_type wrapper = "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
+    @{index_ML_infix addSWrapper: "Proof.context *
   (string * (Proof.context -> wrapper)) -> Proof.context"} \\
-    @{index_ML_op addSbefore: "Proof.context *
+    @{index_ML_infix addSbefore: "Proof.context *
   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
-    @{index_ML_op addSafter: "Proof.context *
+    @{index_ML_infix addSafter: "Proof.context *
   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
-    @{index_ML_op delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
-    @{index_ML_op addWrapper: "Proof.context *
+    @{index_ML_infix delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
+    @{index_ML_infix addWrapper: "Proof.context *
   (string * (Proof.context -> wrapper)) -> Proof.context"} \\
-    @{index_ML_op addbefore: "Proof.context *
+    @{index_ML_infix addbefore: "Proof.context *
   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
-    @{index_ML_op addafter: "Proof.context *
+    @{index_ML_infix addafter: "Proof.context *
   (string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
-    @{index_ML_op delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
+    @{index_ML_infix delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
     @{index_ML addSss: "Proof.context -> Proof.context"} \\
     @{index_ML addss: "Proof.context -> Proof.context"} \\
   \end{mldecls}
--- a/src/Doc/antiquote_setup.ML	Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/antiquote_setup.ML	Sat May 22 13:35:25 2021 +0200
@@ -37,82 +37,86 @@
 
 local
 
-fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
-  | ml_val (toks1, toks2) =
-      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
+fun test_val (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read ");"
+  | test_val (ml1, ml2) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read ");";
 
-fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
-  | ml_op (toks1, toks2) =
-      ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
+fun test_op (ml1, ml2) = test_val (ML_Lex.read "op " @ ml1, ml2);
 
-fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
-  | ml_type (toks1, toks2) =
-      ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
-        toks2 @ ML_Lex.read ") option];";
+fun test_type (ml1, []) = ML_Lex.read "val _ = NONE : (" @ ml1 @ ML_Lex.read ") option;"
+  | test_type (ml1, ml2) =
+      ML_Lex.read "val _ = [NONE : (" @ ml1 @ ML_Lex.read ") option, NONE : (" @
+      ml2 @ ML_Lex.read ") option];";
 
-fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
-  | ml_exception (toks1, toks2) =
-      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";
+fun text_exn (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : exn);"
+  | text_exn (ml1, ml2) =
+      ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read " -> exn);";
 
-fun ml_structure (toks, _) =
-  ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";
+fun test_struct (ml, _) =
+  ML_Lex.read "functor XXX() = struct structure XX = " @ ml @ ML_Lex.read " end;";
 
-fun ml_functor (Antiquote.Text tok :: _, _) =
+fun test_functor (Antiquote.Text tok :: _, _) =
       ML_Lex.read "ML_Env.check_functor " @
       ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
-  | ml_functor _ = raise Fail "Bad ML functor specification";
+  | test_functor _ = raise Fail "Bad ML functor specification";
 
 val is_name =
   ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
 
-fun ml_name txt =
-  (case filter is_name (ML_Lex.tokenize txt) of
-    toks as [_] => ML_Lex.flatten toks
-  | _ => error ("Single ML name expected in input: " ^ quote txt));
-
-fun prep_ml source =
-  (#1 (Input.source_content source), ML_Lex.read_source source);
+fun is_ml_identifier ants =
+  forall Antiquote.is_text ants andalso
+    (case filter is_name (map (Antiquote.the_text "") ants) of
+      toks as [_] => Symbol_Pos.is_identifier (Long_Name.base_name (ML_Lex.flatten toks))
+    | _ => false);
 
-fun index_ml name kind ml = Document_Output.antiquotation_raw name
-  (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
-  (fn ctxt => fn (source1, opt_source2) =>
-    let
-      val (txt1, ants1) = prep_ml source1;
-      val (txt2, ants2) =
-        (case opt_source2 of
-          SOME source => prep_ml source
-        | NONE => ("", []));
+val parse_ml = Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty;
+val parse_type = Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty;
+val parse_exn = Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty;
+val parse_struct = Args.text_input >> rpair Input.empty;
+
+fun antiquotation_ml parse test kind show_kind binding index =
+  Document_Output.antiquotation_raw binding (Scan.lift parse)
+    (fn ctxt => fn (source1, source2) =>
+      let
+        val (ml1, ml2) = apply2 ML_Lex.read_source (source1, source2);
+        val pos = Input.pos_of source1;
+        val _ =
+          ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (test (ml1, ml2))
+            handle ERROR msg => error (msg ^ Position.here pos);
 
-      val txt =
-        if txt2 = "" then txt1
-        else if kind = "type" then txt1 ^ " = " ^ txt2
-        else if kind = "exception" then txt1 ^ " of " ^ txt2
-        else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1))
-        then txt1 ^ ": " ^ txt2
-        else txt1 ^ " : " ^ txt2;
-      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
+        val (txt1, txt2) = apply2 (#1 o Input.source_content) (source1, source2);
+        val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":";
+        val txt =
+          if txt2 = "" then txt1
+          else if sep = ":" andalso is_ml_identifier ml1 then txt1 ^ ": " ^ txt2
+          else txt1 ^ " " ^ sep ^ " " ^ txt2;
+
+        val main_text =
+          Document_Output.verbatim ctxt
+            (if kind = "" orelse not show_kind then txt else kind ^ " " ^ txt);
 
-      val pos = Input.pos_of source1;
-      val _ =
-        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (ants1, ants2))
-          handle ERROR msg => error (msg ^ Position.here pos);
-      val kind' = if kind = "" then "ML" else "ML " ^ kind;
-    in
-      Latex.block
-       [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"),
-        Document_Output.verbatim ctxt txt']
-    end);
+        val index_text =
+          index |> Option.map (fn def =>
+            let
+              val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt;
+              val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")";
+              val txt' = Latex.block [Document_Output.verbatim ctxt' txt1, Latex.string kind'];
+              val like = Document_Antiquotation.approx_content ctxt source1;
+            in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
+      in Latex.block (the_list index_text @ [main_text]) end);
+
+fun antiquotation_ml' parse test kind binding =
+  antiquotation_ml parse test kind true binding (SOME true);
 
 in
 
 val _ =
   Theory.setup
-   (index_ml \<^binding>\<open>index_ML\<close> "" ml_val #>
-    index_ml \<^binding>\<open>index_ML_op\<close> "infix" ml_op #>
-    index_ml \<^binding>\<open>index_ML_type\<close> "type" ml_type #>
-    index_ml \<^binding>\<open>index_ML_exception\<close> "exception" ml_exception #>
-    index_ml \<^binding>\<open>index_ML_structure\<close> "structure" ml_structure #>
-    index_ml \<^binding>\<open>index_ML_functor\<close> "functor" ml_functor);
+   (antiquotation_ml' parse_ml test_val "" \<^binding>\<open>index_ML\<close> #>
+    antiquotation_ml' parse_ml test_op "infix" \<^binding>\<open>index_ML_infix\<close> #>
+    antiquotation_ml' parse_type test_type "type" \<^binding>\<open>index_ML_type\<close> #>
+    antiquotation_ml' parse_exn text_exn "exception" \<^binding>\<open>index_ML_exception\<close> #>
+    antiquotation_ml' parse_struct test_struct "structure" \<^binding>\<open>index_ML_structure\<close> #>
+    antiquotation_ml' parse_struct test_functor "functor" \<^binding>\<open>index_ML_functor\<close>);
 
 end;
 
--- a/src/Pure/Thy/latex.ML	Fri May 21 13:07:53 2021 +0200
+++ b/src/Pure/Thy/latex.ML	Sat May 22 13:35:25 2021 +0200
@@ -34,6 +34,7 @@
   val index_item: index_item -> text
   type index_entry = {items: index_item list, def: bool}
   val index_entry: index_entry -> text
+  val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
   val latexN: string
   val latex_output: string -> string * int
   val latex_markup: string * Properties.T -> Markup.output
@@ -258,7 +259,8 @@
 
 val index_escape =
   translate_string (fn s =>
-    s |> exists_string (fn s' => s = s') "\"\\{}!@|" ? prefix "\"");
+    if member_string "!\"@|" s then "\\char" ^ string_of_int (ord s)
+    else if member_string "\\{}#" s then "\"" ^ s else s);
 
 fun index_item (item: index_item) =
   let
@@ -273,6 +275,13 @@
   |> enclose_block "\\index{" "}";
 
 
+fun index_binding NONE = I
+  | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
+
+fun index_variants setup binding =
+  fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
+
+
 (* print mode *)
 
 val latexN = "latex";
--- a/src/Pure/library.ML	Fri May 21 13:07:53 2021 +0200
+++ b/src/Pure/library.ML	Sat May 22 13:35:25 2021 +0200
@@ -132,6 +132,7 @@
   val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
   val exists_string: (string -> bool) -> string -> bool
   val forall_string: (string -> bool) -> string -> bool
+  val member_string: string -> string -> bool
   val first_field: string -> string -> (string * string) option
   val enclose: string -> string -> string -> string
   val unenclose: string -> string
@@ -703,6 +704,8 @@
 
 fun forall_string pred = not o exists_string (not o pred);
 
+fun member_string str s = exists_string (fn s' => s = s') str;
+
 fun first_field sep str =
   let
     val n = size sep;