# HG changeset patch
# User wenzelm
# Date 1621784128 -7200
# Node ID b49a03bb136c1dbb9c7dc990fd2dfec4db47e7cb
# Parent  e502b40717c76bc32702d7f6c50c6ea2c3abd2f3
tuned signature;

diff -r e502b40717c7 -r b49a03bb136c src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Sun May 23 17:08:34 2021 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Sun May 23 17:35:28 2021 +0200
@@ -35,7 +35,7 @@
   val integer: string -> int
   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
+  val approx_content: Proof.context -> string -> string
 end;
 
 structure Document_Antiquotation: DOCUMENT_ANTIQUOTATION =
@@ -227,12 +227,13 @@
 
 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;
+fun approx_content ctxt =
+  Symbol_Pos.explode0
+  #> trim (Symbol.is_blank o Symbol_Pos.symbol)
+  #> Antiquote.parse_comments Position.none
+  #> maps (strip_antiq ctxt)
+  #> map strip_symbol
+  #> implode;
 
 end;
 
diff -r e502b40717c7 -r b49a03bb136c src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Sun May 23 17:08:34 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Sun May 23 17:35:28 2021 +0200
@@ -162,7 +162,7 @@
             val like =
               (case opt_like of
                 SOME s => s
-              | NONE => Document_Antiquotation.approx_content ctxt txt);
+              | NONE => Document_Antiquotation.approx_content ctxt (Input.string_of txt));
             val _ =
               if is_none opt_like andalso Context_Position.is_visible ctxt then
                 writeln ("(" ^ Markup.markup Markup.keyword2 "is" ^ " " ^ quote like ^ ")" ^
@@ -368,7 +368,7 @@
               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;
+              val like = Document_Antiquotation.approx_content ctxt' txt1;
             in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
       in Latex.block (the_list index_text @ [main_text]) end);