--- 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;
--- 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);