clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;
--- a/src/Doc/Implementation/Local_Theory.thy Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy Sat May 22 13:35:25 2021 +0200
@@ -90,7 +90,7 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_type local_theory: Proof.context} \\
+ @{index_ML_type local_theory = Proof.context} \\
@{index_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex]
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
local_theory -> (term * (string * thm)) * local_theory"} \\
--- a/src/Doc/Implementation/Logic.thy Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy Sat May 22 13:35:25 2021 +0200
@@ -102,9 +102,9 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_type class: string} \\
- @{index_ML_type sort: "class list"} \\
- @{index_ML_type arity: "string * sort list * sort"} \\
+ @{index_ML_type class = string} \\
+ @{index_ML_type sort = "class list"} \\
+ @{index_ML_type arity = "string * sort list * sort"} \\
@{index_ML_type typ} \\
@{index_ML Term.map_atyps: "(typ -> typ) -> typ -> typ"} \\
@{index_ML Term.fold_atyps: "(typ -> 'a -> 'a) -> typ -> 'a -> 'a"} \\
@@ -314,7 +314,7 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML_type term} \\
- @{index_ML_op "aconv": "term * term -> bool"} \\
+ @{index_ML_infix "aconv": "term * term -> bool"} \\
@{index_ML Term.map_types: "(typ -> typ) -> term -> term"} \\
@{index_ML Term.fold_types: "(typ -> 'a -> 'a) -> term -> 'a -> 'a"} \\
@{index_ML Term.map_aterms: "(term -> term) -> term -> term"} \\
@@ -336,7 +336,7 @@
\<^descr> Type \<^ML_type>\<open>term\<close> represents de-Bruijn terms, with comments in
abstractions, and explicitly named free variables and constants; this is a
datatype with constructors @{index_ML Bound}, @{index_ML Free}, @{index_ML
- Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_op "$"}.
+ Var}, @{index_ML Const}, @{index_ML Abs}, @{index_ML_infix "$"}.
\<^descr> \<open>t\<close>~\<^ML_text>\<open>aconv\<close>~\<open>u\<close> checks \<open>\<alpha>\<close>-equivalence of two terms. This is the
basic equality relation on type \<^ML_type>\<open>term\<close>; raw datatype equality
@@ -1022,14 +1022,14 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_op "RSN": "thm * (int * thm) -> thm"} \\
- @{index_ML_op "RS": "thm * thm -> thm"} \\
+ @{index_ML_infix "RSN": "thm * (int * thm) -> thm"} \\
+ @{index_ML_infix "RS": "thm * thm -> thm"} \\
- @{index_ML_op "RLN": "thm list * (int * thm list) -> thm list"} \\
- @{index_ML_op "RL": "thm list * thm list -> thm list"} \\
+ @{index_ML_infix "RLN": "thm list * (int * thm list) -> thm list"} \\
+ @{index_ML_infix "RL": "thm list * thm list -> thm list"} \\
- @{index_ML_op "MRS": "thm list * thm -> thm"} \\
- @{index_ML_op "OF": "thm * thm list -> thm"} \\
+ @{index_ML_infix "MRS": "thm list * thm -> thm"} \\
+ @{index_ML_infix "OF": "thm * thm list -> thm"} \\
\end{mldecls}
\<^descr> \<open>rule\<^sub>1 RSN (i, rule\<^sub>2)\<close> resolves the conclusion of \<open>rule\<^sub>1\<close> with the
@@ -1197,8 +1197,8 @@
\end{mldecls}
\<^descr> Type \<^ML_type>\<open>proof\<close> represents proof terms; this is a datatype with
- constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_op "%"},
- @{index_ML_op "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
+ constructors @{index_ML Abst}, @{index_ML AbsP}, @{index_ML_infix "%"},
+ @{index_ML_infix "%%"}, @{index_ML PBound}, @{index_ML MinProof}, @{index_ML
Hyp}, @{index_ML PAxm}, @{index_ML Oracle}, @{index_ML PThm} as explained
above. %FIXME PClass (!?)
--- a/src/Doc/Implementation/ML.thy Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/ML.thy Sat May 22 13:35:25 2021 +0200
@@ -818,10 +818,10 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\
- @{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
- @{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
- @{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
+ @{index_ML_infix "|>" : "'a * ('a -> 'b) -> 'b"} \\
+ @{index_ML_infix "|->" : "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
+ @{index_ML_infix "#>" : "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
+ @{index_ML_infix "#->" : "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
\end{mldecls}
\<close>
@@ -1142,8 +1142,8 @@
\begin{mldecls}
@{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
@{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
- @{index_ML_exception ERROR: string} \\
- @{index_ML_exception Fail: string} \\
+ @{index_ML_exception ERROR of string} \\
+ @{index_ML_exception Fail of string} \\
@{index_ML Exn.is_interrupt: "exn -> bool"} \\
@{index_ML Exn.reraise: "exn -> 'a"} \\
@{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
@@ -1284,7 +1284,7 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_type "Symbol.symbol": string} \\
+ @{index_ML_type Symbol.symbol = string} \\
@{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
@{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
@{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\
@@ -1596,7 +1596,7 @@
@{index_ML_type "'a Unsynchronized.ref"} \\
@{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
@{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
- @{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\
+ @{index_ML_infix ":=" : "'a Unsynchronized.ref * 'a -> unit"} \\
\end{mldecls}
\<close>
--- a/src/Doc/Implementation/Prelim.thy Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Prelim.thy Sat May 22 13:35:25 2021 +0200
@@ -720,7 +720,7 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_type indexname: "string * int"} \\
+ @{index_ML_type indexname = "string * int"} \\
\end{mldecls}
\<^descr> Type \<^ML_type>\<open>indexname\<close> represents indexed names. This is an
--- a/src/Doc/Implementation/Tactic.thy Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Implementation/Tactic.thy Sat May 22 13:35:25 2021 +0200
@@ -156,7 +156,7 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_type tactic: "thm -> thm Seq.seq"} \\
+ @{index_ML_type tactic = "thm -> thm Seq.seq"} \\
@{index_ML no_tac: tactic} \\
@{index_ML all_tac: tactic} \\
@{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
@@ -452,7 +452,7 @@
\begin{mldecls}
@{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
@{index_ML Drule.compose: "thm * int * thm -> thm"} \\
- @{index_ML_op COMP: "thm * thm -> thm"} \\
+ @{index_ML_infix COMP: "thm * thm -> thm"} \\
\end{mldecls}
\<^descr> \<^ML>\<open>compose_tac\<close>~\<open>ctxt (flag, rule, m) i\<close> refines subgoal \<open>i\<close> using
@@ -502,15 +502,15 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML_op "THEN": "tactic * tactic -> tactic"} \\
- @{index_ML_op "ORELSE": "tactic * tactic -> tactic"} \\
- @{index_ML_op "APPEND": "tactic * tactic -> tactic"} \\
+ @{index_ML_infix "THEN": "tactic * tactic -> tactic"} \\
+ @{index_ML_infix "ORELSE": "tactic * tactic -> tactic"} \\
+ @{index_ML_infix "APPEND": "tactic * tactic -> tactic"} \\
@{index_ML "EVERY": "tactic list -> tactic"} \\
@{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
- @{index_ML_op "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
- @{index_ML_op "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
- @{index_ML_op "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML_infix "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML_infix "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+ @{index_ML_infix "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
@{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
@{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
\end{mldecls}
--- a/src/Doc/Isar_Ref/Generic.thy Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Sat May 22 13:35:25 2021 +0200
@@ -909,10 +909,10 @@
@{index_ML_type solver} \\
@{index_ML Simplifier.mk_solver: "string ->
(Proof.context -> int -> tactic) -> solver"} \\
- @{index_ML_op setSolver: "Proof.context * solver -> Proof.context"} \\
- @{index_ML_op addSolver: "Proof.context * solver -> Proof.context"} \\
- @{index_ML_op setSSolver: "Proof.context * solver -> Proof.context"} \\
- @{index_ML_op addSSolver: "Proof.context * solver -> Proof.context"} \\
+ @{index_ML_infix setSolver: "Proof.context * solver -> Proof.context"} \\
+ @{index_ML_infix addSolver: "Proof.context * solver -> Proof.context"} \\
+ @{index_ML_infix setSSolver: "Proof.context * solver -> Proof.context"} \\
+ @{index_ML_infix addSSolver: "Proof.context * solver -> Proof.context"} \\
\end{mldecls}
A solver is a tactic that attempts to solve a subgoal after simplification.
@@ -992,12 +992,12 @@
text \<open>
\begin{mldecls}
- @{index_ML_op setloop: "Proof.context *
+ @{index_ML_infix setloop: "Proof.context *
(Proof.context -> int -> tactic) -> Proof.context"} \\
- @{index_ML_op addloop: "Proof.context *
+ @{index_ML_infix addloop: "Proof.context *
(string * (Proof.context -> int -> tactic))
-> Proof.context"} \\
- @{index_ML_op delloop: "Proof.context * string -> Proof.context"} \\
+ @{index_ML_infix delloop: "Proof.context * string -> Proof.context"} \\
@{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
@{index_ML Splitter.add_split: "thm -> Proof.context -> Proof.context"} \\
@{index_ML Splitter.add_split_bang: "
@@ -1624,21 +1624,21 @@
text \<open>
\begin{mldecls}
- @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
- @{index_ML_op addSWrapper: "Proof.context *
+ @{index_ML_type wrapper = "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
+ @{index_ML_infix addSWrapper: "Proof.context *
(string * (Proof.context -> wrapper)) -> Proof.context"} \\
- @{index_ML_op addSbefore: "Proof.context *
+ @{index_ML_infix addSbefore: "Proof.context *
(string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
- @{index_ML_op addSafter: "Proof.context *
+ @{index_ML_infix addSafter: "Proof.context *
(string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
- @{index_ML_op delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
- @{index_ML_op addWrapper: "Proof.context *
+ @{index_ML_infix delSWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
+ @{index_ML_infix addWrapper: "Proof.context *
(string * (Proof.context -> wrapper)) -> Proof.context"} \\
- @{index_ML_op addbefore: "Proof.context *
+ @{index_ML_infix addbefore: "Proof.context *
(string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
- @{index_ML_op addafter: "Proof.context *
+ @{index_ML_infix addafter: "Proof.context *
(string * (Proof.context -> int -> tactic)) -> Proof.context"} \\
- @{index_ML_op delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
+ @{index_ML_infix delWrapper: "Proof.context * string -> Proof.context"} \\[0.5ex]
@{index_ML addSss: "Proof.context -> Proof.context"} \\
@{index_ML addss: "Proof.context -> Proof.context"} \\
\end{mldecls}
--- a/src/Doc/antiquote_setup.ML Fri May 21 13:07:53 2021 +0200
+++ b/src/Doc/antiquote_setup.ML Sat May 22 13:35:25 2021 +0200
@@ -37,82 +37,86 @@
local
-fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
- | ml_val (toks1, toks2) =
- ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
+fun test_val (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read ");"
+ | test_val (ml1, ml2) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read ");";
-fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
- | ml_op (toks1, toks2) =
- ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
+fun test_op (ml1, ml2) = test_val (ML_Lex.read "op " @ ml1, ml2);
-fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
- | ml_type (toks1, toks2) =
- ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
- toks2 @ ML_Lex.read ") option];";
+fun test_type (ml1, []) = ML_Lex.read "val _ = NONE : (" @ ml1 @ ML_Lex.read ") option;"
+ | test_type (ml1, ml2) =
+ ML_Lex.read "val _ = [NONE : (" @ ml1 @ ML_Lex.read ") option, NONE : (" @
+ ml2 @ ML_Lex.read ") option];";
-fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
- | ml_exception (toks1, toks2) =
- ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";
+fun text_exn (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : exn);"
+ | text_exn (ml1, ml2) =
+ ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read " -> exn);";
-fun ml_structure (toks, _) =
- ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";
+fun test_struct (ml, _) =
+ ML_Lex.read "functor XXX() = struct structure XX = " @ ml @ ML_Lex.read " end;";
-fun ml_functor (Antiquote.Text tok :: _, _) =
+fun test_functor (Antiquote.Text tok :: _, _) =
ML_Lex.read "ML_Env.check_functor " @
ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
- | ml_functor _ = raise Fail "Bad ML functor specification";
+ | test_functor _ = raise Fail "Bad ML functor specification";
val is_name =
ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
-fun ml_name txt =
- (case filter is_name (ML_Lex.tokenize txt) of
- toks as [_] => ML_Lex.flatten toks
- | _ => error ("Single ML name expected in input: " ^ quote txt));
-
-fun prep_ml source =
- (#1 (Input.source_content source), ML_Lex.read_source source);
+fun is_ml_identifier ants =
+ forall Antiquote.is_text ants andalso
+ (case filter is_name (map (Antiquote.the_text "") ants) of
+ toks as [_] => Symbol_Pos.is_identifier (Long_Name.base_name (ML_Lex.flatten toks))
+ | _ => false);
-fun index_ml name kind ml = Document_Output.antiquotation_raw name
- (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
- (fn ctxt => fn (source1, opt_source2) =>
- let
- val (txt1, ants1) = prep_ml source1;
- val (txt2, ants2) =
- (case opt_source2 of
- SOME source => prep_ml source
- | NONE => ("", []));
+val parse_ml = Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty;
+val parse_type = Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty;
+val parse_exn = Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty;
+val parse_struct = Args.text_input >> rpair Input.empty;
+
+fun antiquotation_ml parse test kind show_kind binding index =
+ Document_Output.antiquotation_raw binding (Scan.lift parse)
+ (fn ctxt => fn (source1, source2) =>
+ let
+ val (ml1, ml2) = apply2 ML_Lex.read_source (source1, source2);
+ val pos = Input.pos_of source1;
+ val _ =
+ ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (test (ml1, ml2))
+ handle ERROR msg => error (msg ^ Position.here pos);
- val txt =
- if txt2 = "" then txt1
- else if kind = "type" then txt1 ^ " = " ^ txt2
- else if kind = "exception" then txt1 ^ " of " ^ txt2
- else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1))
- then txt1 ^ ": " ^ txt2
- else txt1 ^ " : " ^ txt2;
- val txt' = if kind = "" then txt else kind ^ " " ^ txt;
+ val (txt1, txt2) = apply2 (#1 o Input.source_content) (source1, source2);
+ val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":";
+ val txt =
+ if txt2 = "" then txt1
+ else if sep = ":" andalso is_ml_identifier ml1 then txt1 ^ ": " ^ txt2
+ else txt1 ^ " " ^ sep ^ " " ^ txt2;
+
+ val main_text =
+ Document_Output.verbatim ctxt
+ (if kind = "" orelse not show_kind then txt else kind ^ " " ^ txt);
- val pos = Input.pos_of source1;
- val _ =
- ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (ants1, ants2))
- handle ERROR msg => error (msg ^ Position.here pos);
- val kind' = if kind = "" then "ML" else "ML " ^ kind;
- in
- Latex.block
- [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"),
- Document_Output.verbatim ctxt txt']
- end);
+ val index_text =
+ index |> Option.map (fn def =>
+ let
+ 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;
+ in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
+ in Latex.block (the_list index_text @ [main_text]) end);
+
+fun antiquotation_ml' parse test kind binding =
+ antiquotation_ml parse test kind true binding (SOME true);
in
val _ =
Theory.setup
- (index_ml \<^binding>\<open>index_ML\<close> "" ml_val #>
- index_ml \<^binding>\<open>index_ML_op\<close> "infix" ml_op #>
- index_ml \<^binding>\<open>index_ML_type\<close> "type" ml_type #>
- index_ml \<^binding>\<open>index_ML_exception\<close> "exception" ml_exception #>
- index_ml \<^binding>\<open>index_ML_structure\<close> "structure" ml_structure #>
- index_ml \<^binding>\<open>index_ML_functor\<close> "functor" ml_functor);
+ (antiquotation_ml' parse_ml test_val "" \<^binding>\<open>index_ML\<close> #>
+ antiquotation_ml' parse_ml test_op "infix" \<^binding>\<open>index_ML_infix\<close> #>
+ antiquotation_ml' parse_type test_type "type" \<^binding>\<open>index_ML_type\<close> #>
+ antiquotation_ml' parse_exn text_exn "exception" \<^binding>\<open>index_ML_exception\<close> #>
+ antiquotation_ml' parse_struct test_struct "structure" \<^binding>\<open>index_ML_structure\<close> #>
+ antiquotation_ml' parse_struct test_functor "functor" \<^binding>\<open>index_ML_functor\<close>);
end;
--- a/src/Pure/Thy/latex.ML Fri May 21 13:07:53 2021 +0200
+++ b/src/Pure/Thy/latex.ML Sat May 22 13:35:25 2021 +0200
@@ -34,6 +34,7 @@
val index_item: index_item -> text
type index_entry = {items: index_item list, def: bool}
val index_entry: index_entry -> text
+ val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
val latexN: string
val latex_output: string -> string * int
val latex_markup: string * Properties.T -> Markup.output
@@ -258,7 +259,8 @@
val index_escape =
translate_string (fn s =>
- s |> exists_string (fn s' => s = s') "\"\\{}!@|" ? prefix "\"");
+ if member_string "!\"@|" s then "\\char" ^ string_of_int (ord s)
+ else if member_string "\\{}#" s then "\"" ^ s else s);
fun index_item (item: index_item) =
let
@@ -273,6 +275,13 @@
|> enclose_block "\\index{" "}";
+fun index_binding NONE = I
+ | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
+
+fun index_variants setup binding =
+ fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
+
+
(* print mode *)
val latexN = "latex";
--- a/src/Pure/library.ML Fri May 21 13:07:53 2021 +0200
+++ b/src/Pure/library.ML Sat May 22 13:35:25 2021 +0200
@@ -132,6 +132,7 @@
val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
val exists_string: (string -> bool) -> string -> bool
val forall_string: (string -> bool) -> string -> bool
+ val member_string: string -> string -> bool
val first_field: string -> string -> (string * string) option
val enclose: string -> string -> string -> string
val unenclose: string -> string
@@ -703,6 +704,8 @@
fun forall_string pred = not o exists_string (not o pred);
+fun member_string str s = exists_string (fn s' => s = s') str;
+
fun first_field sep str =
let
val n = size sep;