more ambitious default for index "is like";

--- a/src/Pure/Thy/document_antiquotation.ML	Thu May 20 18:32:59 2021 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Thu May 20 21:21:37 2021 +0200
@@ -33,6 +33,8 @@
   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
 end;
@@ -187,15 +189,17 @@
 
 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 {range = (pos, _), body, ...} =>
-      let val keywords = Thy_Header.get_keywords' ctxt;
-      in eval ctxt pos (Token.read_antiq keywords parse_antiq (body, pos)) end);
+  | Antiquote.Antiq antiq => eval ctxt (#1 (#range antiq)) (read_antiq ctxt antiq));
 
 end;
 

--- a/src/Pure/Thy/document_antiquotations.ML	Thu May 20 18:32:59 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu May 20 21:21:37 2021 +0200
@@ -146,18 +146,61 @@
 
 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.optional index_like "");
+val index_args = Parse.enum1 "!" (Args.embedded_input -- Scan.option 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}));
+      let
+        val _ = Context_Position.reports ctxt (maps (Thy_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);
+            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);