clarified modules;

--- a/src/Pure/Thy/document_antiquotation.ML	Fri May 21 12:29:29 2021 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Fri May 21 13:07:53 2021 +0200
@@ -33,10 +33,9 @@
   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 =
@@ -204,6 +203,40 @@
 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

--- a/src/Pure/Thy/document_antiquotations.ML	Fri May 21 12:29:29 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Fri May 21 13:07:53 2021 +0200
@@ -146,37 +146,6 @@
 
 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);
 
@@ -193,7 +162,7 @@
             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 ^ ")" ^