# HG changeset patch # User wenzelm # Date 1621538497 -7200 # Node ID f9c8da2539449766d561814e2ec192f495575b7b # Parent a3cdcd7dd1670401bfd08e655290673a0acb871b more ambitious default for index "is like"; diff -r a3cdcd7dd167 -r f9c8da253944 src/Pure/Thy/document_antiquotation.ML --- 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; diff -r a3cdcd7dd167 -r f9c8da253944 src/Pure/Thy/document_antiquotations.ML --- 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>\index_ref\ false #> index \<^binding>\index_def\ true);