# HG changeset patch # User wenzelm # Date 1621683325 -7200 # Node ID eccc4a13216d1f6a73ca56c5935822257b02a650 # Parent 14841c6e4d5fe2a23cce8bb17e3876336b32b998 clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax; diff -r 14841c6e4d5f -r eccc4a13216d src/Doc/Implementation/Local_Theory.thy --- 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 \ \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"} \\ diff -r 14841c6e4d5f -r eccc4a13216d src/Doc/Implementation/Logic.thy --- 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 \ \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 \ \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>\term\ 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> \t\~\<^ML_text>\aconv\~\u\ checks \\\-equivalence of two terms. This is the basic equality relation on type \<^ML_type>\term\; raw datatype equality @@ -1022,14 +1022,14 @@ text %mlref \ \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> \rule\<^sub>1 RSN (i, rule\<^sub>2)\ resolves the conclusion of \rule\<^sub>1\ with the @@ -1197,8 +1197,8 @@ \end{mldecls} \<^descr> Type \<^ML_type>\proof\ 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 (!?) diff -r 14841c6e4d5f -r eccc4a13216d src/Doc/Implementation/ML.thy --- 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 \ \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} \ @@ -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 \ \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} \ diff -r 14841c6e4d5f -r eccc4a13216d src/Doc/Implementation/Prelim.thy --- 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 \ \begin{mldecls} - @{index_ML_type indexname: "string * int"} \\ + @{index_ML_type indexname = "string * int"} \\ \end{mldecls} \<^descr> Type \<^ML_type>\indexname\ represents indexed names. This is an diff -r 14841c6e4d5f -r eccc4a13216d src/Doc/Implementation/Tactic.thy --- 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 \ \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>\compose_tac\~\ctxt (flag, rule, m) i\ refines subgoal \i\ using @@ -502,15 +502,15 @@ text %mlref \ \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} diff -r 14841c6e4d5f -r eccc4a13216d src/Doc/Isar_Ref/Generic.thy --- 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 \ \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 \ \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} diff -r 14841c6e4d5f -r eccc4a13216d src/Doc/antiquote_setup.ML --- 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>\index_ML\ "" ml_val #> - index_ml \<^binding>\index_ML_op\ "infix" ml_op #> - index_ml \<^binding>\index_ML_type\ "type" ml_type #> - index_ml \<^binding>\index_ML_exception\ "exception" ml_exception #> - index_ml \<^binding>\index_ML_structure\ "structure" ml_structure #> - index_ml \<^binding>\index_ML_functor\ "functor" ml_functor); + (antiquotation_ml' parse_ml test_val "" \<^binding>\index_ML\ #> + antiquotation_ml' parse_ml test_op "infix" \<^binding>\index_ML_infix\ #> + antiquotation_ml' parse_type test_type "type" \<^binding>\index_ML_type\ #> + antiquotation_ml' parse_exn text_exn "exception" \<^binding>\index_ML_exception\ #> + antiquotation_ml' parse_struct test_struct "structure" \<^binding>\index_ML_structure\ #> + antiquotation_ml' parse_struct test_functor "functor" \<^binding>\index_ML_functor\); end; diff -r 14841c6e4d5f -r eccc4a13216d src/Pure/Thy/latex.ML --- 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"; diff -r 14841c6e4d5f -r eccc4a13216d src/Pure/library.ML --- 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;