# HG changeset patch # User wenzelm # Date 1729634208 -7200 # Node ID 41a39fa0cae0d8e6723868a9dd7f86cbf8198a5d # Parent 6922f189cb439d030e0b4ba555c05ae82cb8dc91# Parent a8502d492dde72f1ce7f5ae724ae4c2ee4c3a61d merged diff -r 6922f189cb43 -r 41a39fa0cae0 src/HOL/Eisbach/match_method.ML --- a/src/HOL/Eisbach/match_method.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/HOL/Eisbach/match_method.ML Tue Oct 22 23:56:48 2024 +0200 @@ -121,18 +121,27 @@ then Syntax.parse_prop ctxt3 term else Syntax.parse_term ctxt3 term; - fun drop_judgment_dummy t = + val judgment_name = Object_Logic.judgment_name ctxt; + + fun dest_judgment_dummy t = (case t of - Const (judgment, _) $ - (Const (\<^syntax_const>\_type_constraint_\, T) $ - Const (\<^const_name>\Pure.dummy_pattern\, _)) => - if judgment = Object_Logic.judgment_name ctxt then - Const (\<^syntax_const>\_type_constraint_\, T) $ - Const (\<^const_name>\Pure.dummy_pattern\, propT) - else t - | t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2 - | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b) - | _ => t); + Const (c, _) $ + (Const (\<^syntax_const>\_type_constraint_\, T) $ \<^Const_>\Pure.dummy_pattern _\) => + if c = judgment_name then SOME T else NONE + | Const (\<^syntax_const>\_type_constraint_\, _) $ Const (c, _) $ + (Const (\<^syntax_const>\_type_constraint_\, T) $ \<^Const_>\Pure.dummy_pattern _\) => + if c = judgment_name then SOME T else NONE + | _ => NONE); + + fun drop_judgment_dummy t = + (case dest_judgment_dummy t of + SOME T => + Const (\<^syntax_const>\_type_constraint_\, T) $ \<^Const>\Pure.dummy_pattern \<^Type>\prop\\ + | NONE => + (case t of + t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2 + | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b) + | _ => t)); val pats = map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts diff -r 6922f189cb43 -r 41a39fa0cae0 src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Tue Oct 22 23:56:48 2024 +0200 @@ -1,7 +1,9 @@ (* Title: HOL/HOLCF/Tools/cont_consts.ML - Author: Tobias Mayr, David von Oheimb, and Markus Wenzel + Author: Tobias Mayr + Author: David von Oheimb + Author: Makarius -HOLCF version of consts: handle continuous function types in mixfix +HOLCF version of 'consts' command: handle continuous function types in mixfix syntax. *) @@ -14,83 +16,51 @@ structure Cont_Consts: CONT_CONSTS = struct - -(* misc utils *) - -fun change_arrow 0 T = T - | change_arrow n (Type (_, [S, T])) = \<^Type>\fun S \change_arrow (n - 1) T\\ - | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], []) - -fun trans_rules name2 name1 n mx = - let - val vnames = Name.invent Name.context "a" n - val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1) - in - [Syntax.Parse_Print_Rule - (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames), - fold (fn a => fn t => - Ast.mk_appl (Ast.Constant \<^const_syntax>\Rep_cfun\) [t, Ast.Variable a]) - vnames (Ast.Constant name1))] @ - (case mx of - Infix _ => [extra_parse_rule] - | Infixl _ => [extra_parse_rule] - | Infixr _ => [extra_parse_rule] - | _ => []) - end - +fun count_cfun \<^Type>\cfun _ B\ = count_cfun B + 1 + | count_cfun _ = 0 -(* transforming infix/mixfix declarations of constants with type ...->... - a declaration of such a constant is transformed to a normal declaration with - an internal name, the same type, and nofix. Additionally, a purely syntactic - declaration with the original name, type ...=>..., and the original mixfix - is generated and connected to the other declaration via some translation. -*) -fun transform thy (c, T, mx) = - let - val thy_ctxt = Proof_Context.init_global thy - fun syntax b = Lexicon.mark_const (Sign.full_bname thy b) - val c1 = Binding.name_of c - val c2 = c1 ^ "_cont_syntax" - val n = Mixfix.mixfix_args thy_ctxt mx - in - ((c, T, NoSyn), - (Binding.name c2, change_arrow n T, mx), - trans_rules (syntax c2) (syntax c1) n mx) - end - -fun cfun_arity (Type (n, [_, T])) = if n = \<^type_name>\cfun\ then 1 + cfun_arity T else 0 - | cfun_arity _ = 0 - -fun is_contconst _ (_, _, NoSyn) = false - | is_contconst _ (_, _, Binder _) = false (* FIXME ? *) - | is_contconst thy (c, T, mx) = - let - val thy_ctxt = Proof_Context.init_global thy - val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg => - cat_error msg ("in mixfix annotation for " ^ Binding.print c) - in cfun_arity T >= n end - - -(* add_consts *) - -local +fun change_cfun 0 T = T + | change_cfun n \<^Type>\cfun A B\ = \<^Type>\fun A \change_cfun (n - 1) B\\ + | change_cfun _ T = raise TYPE ("cont_consts: change_cfun", [T], []) fun gen_add_consts prep_typ raw_decls thy = let - val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls - val (contconst_decls, normal_decls) = List.partition (is_contconst thy) decls - val transformed_decls = map (transform thy) contconst_decls + val thy_ctxt = Proof_Context.init_global thy + + fun is_cont_const (_, _, NoSyn) = false + | is_cont_const (_, _, Binder _) = false + | is_cont_const (b, T, mx) = + let + val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg => + cat_error msg ("in mixfix annotation for " ^ Binding.print b) + in count_cfun T >= n end + + fun transform (b, T, mx) = + let + val c = Sign.full_name thy b + val c1 = Lexicon.mark_syntax c + val c2 = Lexicon.mark_const c + val xs = Name.invent Name.context "xa" (Mixfix.mixfix_args thy_ctxt mx) + val trans_rules = + Syntax.Parse_Print_Rule + (Ast.mk_appl (Ast.Constant c1) (map Ast.Variable xs), + fold (fn x => fn t => + Ast.mk_appl (Ast.Constant \<^const_syntax>\Rep_cfun\) [t, Ast.Variable x]) + xs (Ast.Constant c2)) :: + (if Mixfix.is_infix mx then [Syntax.Parse_Rule (Ast.Constant c1, Ast.Constant c2)] else []) + in ((b, T, NoSyn), (c1, change_cfun (length xs) T, mx), trans_rules) end + + val decls = map (fn (b, T, mx) => (b, prep_typ thy T, mx)) raw_decls + val (cont_decls, normal_decls) = List.partition is_cont_const decls + val transformed_decls = map transform cont_decls in thy - |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls) + |> Sign.add_consts (normal_decls @ map #1 transformed_decls) + |> Sign.syntax_global true Syntax.mode_default (map #2 transformed_decls) |> Sign.add_trrules (maps #3 transformed_decls) end -in - val add_consts = gen_add_consts Sign.certify_typ val add_consts_cmd = gen_add_consts Syntax.read_typ_global end - -end diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Isar/attrib.ML Tue Oct 22 23:56:48 2024 +0200 @@ -612,6 +612,7 @@ register_config_bool Syntax.ambiguity_warning #> register_config_int Syntax.ambiguity_limit #> register_config_bool Syntax_Trans.eta_contract #> + register_config_bool Syntax_Phases.const_syntax_legacy #> register_config_bool Name_Space.names_long #> register_config_bool Name_Space.names_short #> register_config_bool Name_Space.names_unique #> diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Oct 22 23:56:48 2024 +0200 @@ -95,6 +95,7 @@ val read_term_schematic: Proof.context -> string -> term val read_term_abbrev: Proof.context -> string -> term val show_abbrevs: bool Config.T + val contract_abbrevs: Proof.context -> term -> term val expand_abbrevs: Proof.context -> term -> term val cert_term: Proof.context -> term -> term val cert_prop: Proof.context -> term -> term @@ -779,7 +780,7 @@ val reports = (fold o fold_atyps) (fn T => - if Term_Position.is_positionT T then I + if Term_Position.detect_positionT T then I else (case T of TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S @@ -791,7 +792,7 @@ fun replace_sortsT_same get_sort = Term.map_atyps_same (fn T => - if Term_Position.is_positionT T then raise Same.SAME + if Term_Position.detect_positionT T then raise Same.SAME else (case T of TFree (x, raw_S) => TFree (x, Same.function_eq (op =) (get_sort (x, ~1)) raw_S) diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Syntax/ast.ML --- a/src/Pure/Syntax/ast.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Syntax/ast.ML Tue Oct 22 23:56:48 2024 +0200 @@ -104,7 +104,7 @@ (* strip_positions *) fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) = - if member (op =) Term_Position.markers c andalso not (null (Term_Position.decode x)) + if member (op =) Term_Position.markers c andalso Term_Position.detect x then mk_appl (strip_positions u) (map strip_positions asts) else Appl (map strip_positions (t :: u :: v :: asts)) | strip_positions (Appl asts) = Appl (map strip_positions asts) @@ -163,15 +163,19 @@ exception NO_MATCH; -fun const_match _ (Constant a) b = a = b - | const_match _ (Variable a) b = a = b - | const_match true (Appl [Constant "_constrain", ast, _]) b = const_match false ast b - | const_match _ _ _ = false; +fun const_match0 (Constant a) b = a = b + | const_match0 (Variable a) b = a = b + | const_match0 _ _ = false; + +fun const_match true (Appl [Constant "_constrain", ast, _]) b = const_match0 ast b + | const_match false (Appl [Constant "_constrain", ast, Variable x]) b = + Term_Position.detect x andalso const_match0 ast b + | const_match _ a b = const_match0 a b; fun match1 p ast (Constant b) env = if const_match p ast b then env else raise NO_MATCH - | match1 p ast (Variable x) env = Symtab.update (x, ast) env + | match1 _ ast (Variable x) env = Symtab.update (x, ast) env | match1 p (Appl asts) (Appl pats) env = match2 p asts pats env - | match1 p _ _ _ = raise NO_MATCH + | match1 _ _ _ _ = raise NO_MATCH and match2 p (ast :: asts) (pat :: pats) env = match1 p ast pat env |> match2 p asts pats | match2 _ [] [] env = env | match2 _ _ _ _ = raise NO_MATCH; diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Syntax/lexicon.ML Tue Oct 22 23:56:48 2024 +0200 @@ -60,6 +60,9 @@ val read_int: string -> int option val read_num: string -> {radix: int, leading_zeros: int, value: int} val read_float: string -> {mant: int, exp: int} + val mark_syntax: string -> string + val mark_binder: string -> string + val mark_indexed: string -> string val mark_class: string -> string val unmark_class: string -> string val is_class: string -> bool val mark_type: string -> string val unmark_type: string -> string val is_type: string -> bool val mark_const: string -> string val unmark_const: string -> string val is_const: string -> bool @@ -474,10 +477,21 @@ end; -(* marked logical entities *) + +(** marked names **) fun marker s = (prefix s, unprefix s, String.isPrefix s); + +(* syntax consts *) + +val (mark_syntax, _, _) = marker "\<^syntax>"; +val (mark_binder, _, _) = marker "\<^binder>"; +val (mark_indexed, _, _) = marker "\<^indexed>"; + + +(* logical entities *) + val (mark_class, unmark_class, is_class) = marker "\<^class>"; val (mark_type, unmark_type, is_type) = marker "\<^type>"; val (mark_const, unmark_const, is_const) = marker "\<^const>"; diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Syntax/mixfix.ML Tue Oct 22 23:56:48 2024 +0200 @@ -1,26 +1,25 @@ (* Title: Pure/Syntax/mixfix.ML - Author: Tobias Nipkow and Markus Wenzel, TU Muenchen + Author: Tobias Nipkow, TU Muenchen + Author: Makarius Mixfix declarations, infixes, binders. *) -signature BASIC_MIXFIX = -sig - datatype mixfix = - NoSyn | - Mixfix of Input.source * int list * int * Position.range | - Infix of Input.source * int * Position.range | - Infixl of Input.source * int * Position.range | - Infixr of Input.source * int * Position.range | - Binder of Input.source * int * int * Position.range | - Structure of Position.range -end; +datatype mixfix = + NoSyn | + Mixfix of Input.source * int list * int * Position.range | + Infix of Input.source * int * Position.range | + Infixl of Input.source * int * Position.range | + Infixr of Input.source * int * Position.range | + Binder of Input.source * int * int * Position.range | + Structure of Position.range; signature MIXFIX = sig - include BASIC_MIXFIX + datatype mixfix = datatype mixfix val mixfix: string -> mixfix val is_empty: mixfix -> bool + val is_infix: mixfix -> bool val equal: mixfix * mixfix -> bool val range_of: mixfix -> Position.range val pos_of: mixfix -> Position.T @@ -30,7 +29,6 @@ val default_constraint: Proof.context -> mixfix -> typ val make_type: int -> typ val binder_name: string -> string - val is_binder_name: string -> bool val syn_ext_types: Proof.context -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext val syn_ext_consts: Proof.context -> string list -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext @@ -41,20 +39,18 @@ (** mixfix declarations **) -datatype mixfix = - NoSyn | - Mixfix of Input.source * int list * int * Position.range | - Infix of Input.source * int * Position.range | - Infixl of Input.source * int * Position.range | - Infixr of Input.source * int * Position.range | - Binder of Input.source * int * int * Position.range | - Structure of Position.range; +datatype mixfix = datatype mixfix; fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range); fun is_empty NoSyn = true | is_empty _ = false; +fun is_infix (Infix _) = true + | is_infix (Infixl _) = true + | is_infix (Infixr _) = true + | is_infix _ = false; + fun equal (NoSyn, NoSyn) = true | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) = Input.equal_content (sy, sy') andalso ps = ps' andalso p = p' @@ -171,9 +167,11 @@ (* binder notation *) val binder_stamp = stamp (); -val binder_suffix = "_binder" -val binder_name = suffix binder_suffix; -val is_binder_name = String.isSuffix binder_suffix; + +fun binder_name c = + (if Lexicon.is_const c then Lexicon.unmark_const c + else if Lexicon.is_fixed c then Lexicon.unmark_fixed c + else c) |> Lexicon.mark_binder; val binder_bg = Symbol_Pos.explode0 "("; val binder_en = Symbol_Pos.explode0 "_./ _)"; @@ -276,6 +274,3 @@ end; end; - -structure Basic_Mixfix: BASIC_MIXFIX = Mixfix; -open Basic_Mixfix; diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Tue Oct 22 23:56:48 2024 +0200 @@ -383,7 +383,7 @@ else let val indexed_const = - if const <> "" then const ^ "_indexed" + if const <> "" then Lexicon.mark_indexed const else err_in_mixfix "Missing constant name for indexed syntax"; val rangeT = Term.range_type typ handle Match => err_in_mixfix "Missing structure argument for indexed syntax"; diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Tue Oct 22 23:56:48 2024 +0200 @@ -15,6 +15,7 @@ Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result val parse_ast_pattern: Proof.context -> string * string -> Ast.ast val term_of_typ: Proof.context -> typ -> term + val const_syntax_legacy: bool Config.T val print_checks: Proof.context -> unit val typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> Context.generic -> Context.generic @@ -117,8 +118,7 @@ (* decode_typ *) -fun decode_pos (Free (s, _)) = - if not (null (Term_Position.decode s)) then SOME s else NONE +fun decode_pos (Free (x, _)) = if Term_Position.detect x then SOME x else NONE | decode_pos _ = NONE; fun decode_typ tm = @@ -153,6 +153,15 @@ (* parsetree_to_ast *) +val const_syntax_legacy = Config.declare_bool ("const_syntax_legacy", \<^here>) (K false); + +fun parsetree_literals (Parser.Markup (_, ts)) = maps parsetree_literals ts + | parsetree_literals (Parser.Node _) = [] + | parsetree_literals (Parser.Tip tok) = + if Lexicon.is_literal tok andalso + not (null (Lexicon.literal_markup (Lexicon.str_of_token tok))) + then [Lexicon.pos_of_token tok] else []; + fun parsetree_to_ast ctxt trf parsetree = let val reports = Unsynchronized.ref ([]: Position.report_text list); @@ -177,11 +186,6 @@ val ast_of_position = ast_of_pos o single o report_pos; fun ast_of_position' a = Ast.constrain (Ast.Constant a) o ast_of_position; - fun trans a args = - (case trf a of - NONE => Ast.mk_appl (Ast.Constant a) args - | SOME f => f ctxt args); - fun asts_of_token tok = if Lexicon.valued_token tok then [Ast.Variable (Lexicon.str_of_token tok)] @@ -223,7 +227,20 @@ let val args = maps asts_of pts in [Ast.Appl (Ast.Constant "_constrain" :: ast_of_position' "_idtdummy" tok :: args)] end | asts_of (Parser.Node ({const = a, ...}, pts)) = - (report_literals a pts; [trans a (maps asts_of pts)]) + let + val ps = maps parsetree_literals pts; + val args = maps asts_of pts; + fun head () = + if (Lexicon.is_fixed a orelse Lexicon.is_const a) + andalso not (Config.get ctxt const_syntax_legacy) + then Ast.constrain (Ast.Constant a) (ast_of_pos ps) + else Ast.Constant a; + val _ = List.app (fn pos => report pos markup_cache a) ps; + in + [case trf a of + SOME f => f ctxt args + | NONE => Ast.mk_appl (head ()) args] + end | asts_of (Parser.Tip tok) = asts_of_token tok and ast_of pt = @@ -304,15 +321,13 @@ | decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u | decode ps _ _ (Const (a, T)) = (case try Lexicon.unmark_fixed a of - SOME x => (report ps markup_free_cache x; Free (x, T)) + SOME x => Free (x, T) | NONE => - let - val c = - (case try Lexicon.unmark_const a of - SOME c => c - | NONE => #1 (decode_const ctxt (a, []))); - val _ = report ps markup_const_cache c; - in Const (c, T) end) + (case try Lexicon.unmark_const a of + SOME c => Const (c, T) + | NONE => + let val c = #1 (decode_const ctxt (a, [])) + in report ps markup_const_cache c; Const (c, T) end)) | decode ps _ _ (Free (a, T)) = ((Name.reject_internal (a, ps) handle ERROR msg => error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps))); @@ -546,7 +561,7 @@ fun term_of (Type (a, Ts)) = Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts) | term_of (TFree (x, S)) = - if not (null (Term_Position.decode x)) then Syntax.free x + if Term_Position.detect x then Syntax.free x else ofsort (Syntax.const "_tfree" $ Syntax.free x) S | term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S; in term_of ty end; diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Syntax/syntax_trans.ML --- a/src/Pure/Syntax/syntax_trans.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Syntax/syntax_trans.ML Tue Oct 22 23:56:48 2024 +0200 @@ -205,7 +205,7 @@ fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts) | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts) | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) = - if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts) + if Term_Position.detect_position ty then list_comb (c $ update_name_tr [t] $ ty, ts) else list_comb (c $ update_name_tr [t] $ (Lexicon.fun_type $ diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/Syntax/term_position.ML --- a/src/Pure/Syntax/term_position.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/Syntax/term_position.ML Tue Oct 22 23:56:48 2024 +0200 @@ -8,13 +8,14 @@ sig val pretty: Position.T list -> Pretty.T val encode: Position.T list -> string + val detect: string -> bool val decode: string -> Position.T list + val detect_position: term -> bool val decode_position: term -> (Position.T list * typ) option val decode_position1: term -> Position.T option + val detect_positionT: typ -> bool val decode_positionT: typ -> Position.T list val decode_positionS: sort -> Position.T list * sort - val is_position: term -> bool - val is_positionT: typ -> bool val markers: string list val strip_positions: term -> term end; @@ -37,22 +38,42 @@ else NONE | decode_pos _ = NONE; + +(* encode *) + +val encode_none = YXML.string_of (encode_pos Position.none); + fun encode ps = - YXML.string_of_body (map encode_pos (if null ps then [Position.none] else ps)); + (case remove (op =) Position.none ps of + [] => encode_none + | ps' => YXML.string_of_body (map encode_pos (distinct (op =) ps'))); + +val encode_prefix = YXML.XY ^ Markup.positionN; + + +(* decode *) + +val detect = String.isPrefix encode_prefix; fun decode str = - let - val xml = YXML.parse_body str handle Fail msg => error msg; - val ps = map decode_pos xml; - in - if not (null ps) andalso forall is_some ps then map the ps - else if forall is_none ps then [] - else error ("Bad encoded positions: " ^ quote str) - end; + if str = encode_none then [Position.none] + else if detect str then + let + val xml = YXML.parse_body str handle Fail msg => error msg; + val ps = map decode_pos xml; + in + if not (null ps) andalso forall is_some ps then map the ps + else if forall is_none ps then [] + else error ("Bad encoded positions: " ^ quote str) + end + else []; (* positions within parse trees *) +fun detect_position (Free (x, _)) = detect x + | detect_position _ = false; + fun decode_position (Free (x, _)) = (case decode x of [] => NONE @@ -65,20 +86,23 @@ | pos :: _ => SOME pos) | decode_position1 _ = NONE; +fun detect_positionT (TFree (x, _)) = detect x + | detect_positionT _ = false; + fun decode_positionT (TFree (x, _)) = decode x | decode_positionT _ = []; fun decode_positionS cs = - let val (ps, sort) = List.partition (not o null o decode) cs + let val (ps, sort) = List.partition detect cs in (maps decode ps, sort) end; -val is_position = is_some o decode_position; -val is_positionT = not o null o decode_positionT; + +(* strip_positions *) val markers = ["_constrain", "_constrainAbs", "_ofsort"]; fun strip_positions ((t as Const (c, _)) $ u $ v) = - if member (op =) markers c andalso is_position v + if member (op =) markers c andalso detect_position v then strip_positions u else t $ strip_positions u $ strip_positions v | strip_positions (t $ u) = strip_positions t $ strip_positions u diff -r 6922f189cb43 -r 41a39fa0cae0 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Oct 22 17:32:34 2024 +0200 +++ b/src/Pure/pure_thy.ML Tue Oct 22 23:56:48 2024 +0200 @@ -219,7 +219,7 @@ ("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(\indent=3 notation=abstraction\%_./ _)", [0, 3], 3)), (const "Pure.eq", typ "'a \ 'a \ prop", infix_ ("==", 2)), - (const "Pure.all_binder", typ "idts \ prop \ prop", + (Mixfix.binder_name "Pure.all", typ "idts \ prop \ prop", mixfix ("(\indent=3 notation=\binder !!\\!!_./ _)", [0, 0], 0)), (const "Pure.imp", typ "prop \ prop \ prop", infixr_ ("==>", 1)), ("_DDDOT", typ "aprop", Mixfix.mixfix "..."),