# HG changeset patch # User wenzelm # Date 1726588315 -7200 # Node ID 5328d67ec64761388b6f7ad73a1fd350b841c15f # Parent d0d0d12cd4cc27f20d672af3383a857c41d15d4e more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory; diff -r d0d0d12cd4cc -r 5328d67ec647 src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Tue Sep 17 17:51:55 2024 +0200 @@ -47,10 +47,11 @@ *) 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 mx + val n = Mixfix.mixfix_args thy_ctxt mx in ((c, T, NoSyn), (Binding.name c2, change_arrow n T, mx), @@ -60,11 +61,12 @@ 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 (c, T, mx) = +fun is_contconst _ (_, _, NoSyn) = false + | is_contconst _ (_, _, Binder _) = false (* FIXME ? *) + | is_contconst thy (c, T, mx) = let - val n = Mixfix.mixfix_args mx handle ERROR msg => + 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 @@ -76,7 +78,7 @@ 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 decls + val (contconst_decls, normal_decls) = List.partition (is_contconst thy) decls val transformed_decls = map (transform thy) contconst_decls in thy diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Isar/class.ML Tue Sep 17 17:51:55 2024 +0200 @@ -438,7 +438,7 @@ thy |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs') |> snd - |> with_syntax ? Sign.notation true prmode [(Const (c, fastype_of rhs), mx)] + |> with_syntax ? Sign.notation_global true prmode [(Const (c, fastype_of rhs), mx)] |> with_syntax ? register_operation class (c, rhs) (#1 prmode = Print_Mode.input) |> Sign.add_const_constraint (c, SOME (fastype_of rhs')) diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Isar/generic_target.ML Tue Sep 17 17:51:55 2024 +0200 @@ -412,7 +412,7 @@ Local_Theory.background_theory_result (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) => (* FIXME type_params!? *) - Sign.notation true prmode + Sign.notation_global true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs)) #-> (fn lhs => standard_const (op <>) prmode diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Isar/proof.ML Tue Sep 17 17:51:55 2024 +0200 @@ -604,7 +604,7 @@ let val ctxt' = ctxt |> is_none (Variable.default_type ctxt x) ? - Variable.declare_constraints (Free (x, Mixfix.default_constraint mx)); + Variable.declare_constraints (Free (x, Mixfix.default_constraint ctxt mx)); val t = Free (#1 (Proof_Context.inferred_param x ctxt')); in ((t, mx), ctxt') end | t => ((t, mx), ctxt)); diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Sep 17 17:51:55 2024 +0200 @@ -377,18 +377,25 @@ (* theory transfer *) -fun transfer_syntax thy ctxt = ctxt |> - map_syntax (Local_Syntax.rebuild thy) |> - map_tsig (fn tsig as (local_tsig, global_tsig) => - let val thy_tsig = Sign.tsig_of thy in - if Type.eq_tsig (thy_tsig, global_tsig) then tsig - else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) - end) |> - map_consts (fn consts as (local_consts, global_consts) => - let val thy_consts = Sign.consts_of thy in - if Consts.eq_consts (thy_consts, global_consts) then consts - else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) - end); +fun transfer_syntax thy ctxt = + let + val thy_ctxt = + Proof_Context.init_global thy + |> Context_Position.restore_visible ctxt; + in + ctxt |> + map_syntax (Local_Syntax.rebuild thy_ctxt) |> + map_tsig (fn tsig as (local_tsig, global_tsig) => + let val thy_tsig = Sign.tsig_of thy in + if Type.eq_tsig (thy_tsig, global_tsig) then tsig + else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig) (*historic merge order*) + end) |> + map_consts (fn consts as (local_consts, global_consts) => + let val thy_consts = Sign.consts_of thy in + if Consts.eq_consts (thy_consts, global_consts) then consts + else (Consts.merge (local_consts, thy_consts), thy_consts) (*historic merge order*) + end) + end; fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy; @@ -1081,7 +1088,7 @@ (* variables *) fun declare_var (x, opt_T, mx) ctxt = - let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx) + let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint ctxt mx) in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end; fun add_syntax vars ctxt = @@ -1137,7 +1144,7 @@ in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end; fun generic_syntax add mode args = - Context.mapping (Sign.syntax add mode args) (syntax add mode args); + Context.mapping (Sign.syntax_global add mode args) (syntax add mode args); (* notation *) @@ -1171,14 +1178,14 @@ val T' = Morphism.typ phi T; val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false); in if similar then SOME (T', mx) else NONE end); - in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end; + in Context.mapping (Sign.type_notation_global add mode args') (type_notation add mode args') end; fun generic_notation add mode args phi = let val args' = args |> map_filter (fn (t, mx) => let val t' = Morphism.term phi t in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end); - in Context.mapping (Sign.notation add mode args') (notation add mode args') end; + in Context.mapping (Sign.notation_global add mode args') (notation add mode args') end; end; diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Tue Sep 17 17:51:55 2024 +0200 @@ -46,7 +46,7 @@ |> Sign.add_nonterminals_global [Binding.make ("param", \<^here>), Binding.make ("params", \<^here>)] - |> Sign.syntax true Syntax.mode_default + |> Sign.syntax_global true Syntax.mode_default [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Syntax/local_syntax.ML --- a/src/Pure/Syntax/local_syntax.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Syntax/local_syntax.ML Tue Sep 17 17:51:55 2024 +0200 @@ -10,7 +10,7 @@ type T val syntax_of: T -> Syntax.syntax val init: theory -> T - val rebuild: theory -> T -> T + val rebuild: Proof.context -> T -> T datatype kind = Type | Const | Fixed val add_syntax: Proof.context -> (kind * (string * typ * mixfix)) list -> T -> {structs: string list, fixes: string list} option * T @@ -42,20 +42,21 @@ fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes}) = make_syntax (f (thy_syntax, local_syntax, mode, mixfixes)); -fun is_consistent thy (Syntax {thy_syntax, ...}) = - Syntax.eq_syntax (Sign.syntax_of thy, thy_syntax); +fun is_consistent ctxt (Syntax {thy_syntax, ...}) = + Syntax.eq_syntax (Sign.syntax_of (Proof_Context.theory_of ctxt), thy_syntax); fun syntax_of (Syntax {local_syntax, ...}) = local_syntax; (* build syntax *) -fun build_syntax thy mode mixfixes = +fun build_syntax ctxt mode mixfixes = let + val thy = Proof_Context.theory_of ctxt; val thy_syntax = Sign.syntax_of thy; - fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls + fun update_gram ((true, add, m), decls) = Syntax.update_type_gram ctxt add m decls | update_gram ((false, add, m), decls) = - Syntax.update_const_gram add (Sign.logical_types thy) m decls; + Syntax.update_const_gram ctxt add (Sign.logical_types thy) m decls; val local_syntax = thy_syntax |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); @@ -65,9 +66,9 @@ let val thy_syntax = Sign.syntax_of thy in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, []) end; -fun rebuild thy (syntax as Syntax {mode, mixfixes, ...}) = - if is_consistent thy syntax then syntax - else build_syntax thy mode mixfixes; +fun rebuild ctxt (syntax as Syntax {mode, mixfixes, ...}) = + if is_consistent ctxt syntax then syntax + else build_syntax ctxt mode mixfixes; (* mixfix declarations *) @@ -104,7 +105,7 @@ else subtract (op =) new_structs (#structs idents), fixes = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []}; - val syntax' = build_syntax (Proof_Context.theory_of ctxt) mode mixfixes'; + val syntax' = build_syntax ctxt mode mixfixes'; in (if idents = idents' then NONE else SOME idents', syntax') end); fun add_syntax ctxt = update_syntax ctxt true; diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Syntax/mixfix.ML Tue Sep 17 17:51:55 2024 +0200 @@ -26,12 +26,13 @@ val pos_of: mixfix -> Position.T val reset_pos: mixfix -> mixfix val pretty_mixfix: mixfix -> Pretty.T - val mixfix_args: mixfix -> int - val default_constraint: mixfix -> typ + val mixfix_args: Proof.context -> mixfix -> int + val default_constraint: Proof.context -> mixfix -> typ val make_type: int -> typ val binder_name: string -> string - val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext - val syn_ext_consts: string list -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext + 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 end; structure Mixfix: MIXFIX = @@ -117,19 +118,20 @@ (* syntax specifications *) -fun mixfix_args NoSyn = 0 - | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy - | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy - | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy - | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy - | mixfix_args (Binder _) = 1 - | mixfix_args (Structure _) = 0; +fun mixfix_args ctxt = + fn NoSyn => 0 + | Mixfix (sy, _, _, _) => Syntax_Ext.mixfix_args ctxt sy + | Infix (sy, _, _) => 2 + Syntax_Ext.mixfix_args ctxt sy + | Infixl (sy, _, _) => 2 + Syntax_Ext.mixfix_args ctxt sy + | Infixr (sy, _, _) => 2 + Syntax_Ext.mixfix_args ctxt sy + | Binder _ => 1 + | Structure _ => 0; (* default type constraint *) -fun default_constraint (Binder _) = (dummyT --> dummyT) --> dummyT - | default_constraint mx = replicate (mixfix_args mx) dummyT ---> dummyT; +fun default_constraint _ (Binder _) = (dummyT --> dummyT) --> dummyT + | default_constraint ctxt mx = replicate (mixfix_args ctxt mx) dummyT ---> dummyT; (* mixfix template *) @@ -154,7 +156,7 @@ val typeT = Type ("type", []); fun make_type n = replicate n typeT ---> typeT; -fun syn_ext_types type_decls = +fun syn_ext_types ctxt type_decls = let fun mk_infix sy ty t p1 p2 p3 pos = Syntax_Ext.Mfix @@ -172,7 +174,7 @@ | (t, _, _) => error ("Bad mixfix declaration for " ^ quote t ^ Position.here (pos_of mx))); fun check_args (_, ty, mx) (SOME (Syntax_Ext.Mfix (sy, _, _, _, _, _))) = - if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then () + if length (Term.binder_types ty) = Syntax_Ext.mfix_args ctxt sy then () else error ("Bad number of type constructor arguments in mixfix annotation" ^ Position.here (pos_of mx)) @@ -183,7 +185,7 @@ val mfix = map mfix_of type_decls; val _ = map2 check_args type_decls mfix; val consts = map (fn (t, _, _) => (t, [])) type_decls; - in Syntax_Ext.syn_ext [] (map_filter I mfix) consts ([], [], [], []) ([], []) end; + in Syntax_Ext.syn_ext ctxt [] (map_filter I mfix) consts ([], [], [], []) ([], []) end; (* syn_ext_consts *) @@ -195,7 +197,7 @@ let val sy' = Input.source_explode (Input.reset_pos sy); in Symbol_Pos.explode0 "'(" @ sy' @ Symbol_Pos.explode0 "')" end -fun syn_ext_consts logical_types const_decls = +fun syn_ext_consts ctxt logical_types const_decls = let fun mk_infix sy ty c p1 p2 p3 pos = [Syntax_Ext.Mfix (mk_prefix sy, ty, c, [], 1000, Position.none), @@ -238,7 +240,9 @@ val consts = map (fn (c, b) => (c, [b])) binders @ map (fn (c, _, _) => (c, [])) const_decls; - in Syntax_Ext.syn_ext logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) end; + in + Syntax_Ext.syn_ext ctxt logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) + end; end; diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue Sep 17 17:51:55 2024 +0200 @@ -104,17 +104,18 @@ Print_Rule of 'a * 'a | Parse_Print_Rule of 'a * 'a val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule - val update_trfuns: + val update_trfuns: Proof.context -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax - val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax - val update_const_gram: bool -> string list -> + val update_type_gram: Proof.context -> bool -> mode -> (string * typ * mixfix) list -> + syntax -> syntax + val update_const_gram: Proof.context -> bool -> string list -> mode -> (string * typ * mixfix) list -> syntax -> syntax - val update_consts: (string * string list) list -> syntax -> syntax - val update_trrules: Ast.ast trrule list -> syntax -> syntax - val remove_trrules: Ast.ast trrule list -> syntax -> syntax + val update_consts: Proof.context -> (string * string list) list -> syntax -> syntax + val update_trrules: Proof.context -> Ast.ast trrule list -> syntax -> syntax + val remove_trrules: Proof.context -> Ast.ast trrule list -> syntax -> syntax val const: string -> term val free: string -> term val var: indexname -> term @@ -707,18 +708,19 @@ (** modify syntax **) -val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns; +fun update_trfuns ctxt = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns ctxt; -fun update_type_gram add prmode decls = - (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls); +fun update_type_gram ctxt add prmode decls = + (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types ctxt decls); -fun update_const_gram add logical_types prmode decls = - (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls); +fun update_const_gram ctxt add logical_types prmode decls = + (if add then update_syntax else remove_syntax) prmode + (Mixfix.syn_ext_consts ctxt logical_types decls); -val update_consts = update_syntax mode_default o Syntax_Ext.syn_ext_consts; +val update_consts = update_syntax mode_default oo Syntax_Ext.syn_ext_consts; -val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; -val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules; +fun update_trrules ctxt = update_syntax mode_default o Syntax_Ext.syn_ext_rules ctxt o check_rules; +fun remove_trrules ctxt = remove_syntax mode_default o Syntax_Ext.syn_ext_rules ctxt o check_rules; open Lexicon.Syntax; diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Tue Sep 17 17:51:55 2024 +0200 @@ -29,18 +29,18 @@ print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list, print_rules: (Ast.ast * Ast.ast) list, print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list} - val mfix_args: Symbol_Pos.T list -> int - val mixfix_args: Input.source -> int + val mfix_args: Proof.context -> Symbol_Pos.T list -> int + val mixfix_args: Proof.context -> Input.source -> int val escape: string -> string - val syn_ext: string list -> mfix list -> + val syn_ext: Proof.context -> string list -> mfix list -> (string * string list) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext_consts: (string * string list) list -> syn_ext - val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext - val syn_ext_trfuns: + val syn_ext_consts: Proof.context -> (string * string list) list -> syn_ext + val syn_ext_rules: Proof.context -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext + val syn_ext_trfuns: Proof.context -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * @@ -263,18 +263,21 @@ in -fun read_mfix ss = +fun read_mfix ctxt ss = let val xsymbs = (case Scan.error (Scan.finite Symbol_Pos.stopper scan_symbs) ss of (res, []) => map_filter I res | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos)); - val _ = Position.reports (maps reports_of xsymbs); - val _ = Position.reports_text (maps reports_text_of xsymbs); + val _ = Context_Position.reports ctxt (maps reports_of xsymbs); + val _ = Context_Position.reports_text ctxt (maps reports_text_of xsymbs); in xsymbs end; -val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none)); -val mixfix_args = mfix_args o Input.source_explode; +fun mfix_args ctxt = + let val ctxt' = Context_Position.set_visible false ctxt + in length o filter (is_argument o #1) o read_mfix ctxt' o map (apsnd (K Position.none)) end; + +fun mixfix_args ctxt = mfix_args ctxt o Input.source_explode; val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; @@ -283,13 +286,13 @@ (* mfix_to_xprod *) -fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) = +fun mfix_to_xprod ctxt logical_types (Mfix (sy, typ, const, pris, pri, pos)) = let val nonterm_for_lhs = the_default "logic" o try dest_Type_name; val nonterm_for_rhs = the_default "any" o try dest_Type_name; val _ = Position.report pos Markup.language_mixfix; - val symbs0 = read_mfix sy; + val symbs0 = read_mfix ctxt sy; fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos); @@ -396,12 +399,12 @@ (* syn_ext *) -fun syn_ext logical_types mfixes consts trfuns (parse_rules, print_rules) = +fun syn_ext ctxt logical_types mfixes consts trfuns (parse_rules, print_rules) = let val (parse_ast_translation, parse_translation, print_translation, print_ast_translation) = trfuns; - val xprod_results = map (mfix_to_xprod logical_types) mfixes; + val xprod_results = map (mfix_to_xprod ctxt logical_types) mfixes; val xprods = map #1 xprod_results; val consts' = map_filter #2 xprod_results; val parse_rules' = rev (map_filter #3 xprod_results); @@ -419,9 +422,9 @@ end; -fun syn_ext_consts consts = syn_ext [] [] consts ([], [], [], []) ([], []); -fun syn_ext_rules rules = syn_ext [] [] [] ([], [], [], []) rules; -fun syn_ext_trfuns trfuns = syn_ext [] [] [] trfuns ([], []); +fun syn_ext_consts ctxt consts = syn_ext ctxt [] [] consts ([], [], [], []) ([], []); +fun syn_ext_rules ctxt rules = syn_ext ctxt [] [] [] ([], [], [], []) rules; +fun syn_ext_trfuns ctxt trfuns = syn_ext ctxt [] [] [] trfuns ([], []); fun stamp_trfun s (c, f) = (c, (f, s)); fun mk_trfun tr = stamp_trfun (stamp ()) tr; diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/pure_thy.ML Tue Sep 17 17:51:55 2024 +0200 @@ -55,8 +55,8 @@ val old_appl_syntax_setup = Old_Appl_Syntax.put true #> - Sign.syntax false Syntax.mode_default applC_syntax #> - Sign.syntax true Syntax.mode_default appl_syntax; + Sign.syntax_global false Syntax.mode_default applC_syntax #> + Sign.syntax_global true Syntax.mode_default appl_syntax; (* main content *) @@ -87,8 +87,8 @@ "tvar_position", "id_position", "longid_position", "var_position", "str_position", "string_position", "cartouche_position", "type_name", "class_name"])) - #> Sign.syntax true Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) - #> Sign.syntax true Syntax.mode_default + #> Sign.syntax_global true Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) + #> Sign.syntax_global true Syntax.mode_default [("", typ "prop' \ prop", Mixfix.mixfix "_"), ("", typ "logic \ any", Mixfix.mixfix "_"), ("", typ "prop' \ any", Mixfix.mixfix "_"), @@ -184,8 +184,8 @@ ("_sort_constraint", typ "type \ prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"), (const "Pure.term", typ "logic \ prop", Mixfix.mixfix "TERM _"), (const "Pure.conjunction", typ "prop \ prop \ prop", infixr_ ("&&&", 2))] - #> Sign.syntax true Syntax.mode_default applC_syntax - #> Sign.syntax true (Print_Mode.ASCII, true) + #> Sign.syntax_global true Syntax.mode_default applC_syntax + #> Sign.syntax_global true (Print_Mode.ASCII, true) [(tycon "fun", typ "type \ type \ type", mixfix ("(_/ => _)", [1, 0], 0)), ("_bracket", typ "types \ type \ type", mixfix ("([_]/ => _)", [0, 0], 0)), ("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3%_./ _)", [0, 3], 3)), @@ -195,7 +195,7 @@ ("_DDDOT", typ "aprop", Mixfix.mixfix "..."), ("_bigimpl", typ "asms \ prop \ prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), ("_DDDOT", typ "logic", Mixfix.mixfix "...")] - #> Sign.syntax true ("", false) + #> Sign.syntax_global true ("", false) [(const "Pure.prop", typ "prop \ prop", mixfix ("_", [0], 0))] #> Sign.add_consts [(qualify (Binding.make ("eq", \<^here>)), typ "'a \ 'a \ prop", infix_ ("\", 2)), diff -r d0d0d12cd4cc -r 5328d67ec647 src/Pure/sign.ML --- a/src/Pure/sign.ML Tue Sep 17 17:05:37 2024 +0200 +++ b/src/Pure/sign.ML Tue Sep 17 17:51:55 2024 +0200 @@ -76,10 +76,12 @@ val add_nonterminals: Proof.context -> binding list -> theory -> theory val add_nonterminals_global: binding list -> theory -> theory val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory - val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory + val syntax: Proof.context -> bool -> Syntax.mode -> (string * typ * mixfix) list -> + theory -> theory + val syntax_global: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory val syntax_deps: (string * string list) list -> theory -> theory - val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory - val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory + val type_notation_global: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory + val notation_global: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory val add_consts: (binding * typ * mixfix) list -> theory -> theory @@ -157,6 +159,8 @@ fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts)); fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts)); +fun update_syn_global f args thy = map_syn (f (Proof_Context.init_global thy) args) thy; + (* linear change discipline *) @@ -357,7 +361,7 @@ fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) => let val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx); - val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn; + val syn' = Syntax.update_type_gram ctxt true Syntax.mode_default [type_syntax] syn; val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig; in (syn', tsig', consts) end); @@ -382,29 +386,34 @@ (* modify syntax *) -fun syntax add mode args thy = +fun syntax ctxt add mode args thy = let fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy T, mx) handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c); - in thy |> map_syn (Syntax.update_const_gram add (logical_types thy) mode (map prep args)) end; + in thy |> map_syn (Syntax.update_const_gram ctxt add (logical_types thy) mode (map prep args)) end; + +fun syntax_global add mode args thy = + syntax (Proof_Context.init_global thy) add mode args thy; -val syntax_deps = map_syn o Syntax.update_consts; +val syntax_deps = update_syn_global Syntax.update_consts; -fun type_notation add mode args = +fun type_notation_global add mode args thy = let + val thy_ctxt = Proof_Context.init_global thy; fun type_syntax (Type (c, args), mx) = SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx) | type_syntax _ = NONE; - in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end; + in map_syn (Syntax.update_type_gram thy_ctxt add mode (map_filter type_syntax args)) thy end; -fun notation add mode args thy = +fun notation_global add mode args thy = let + val thy_ctxt = Proof_Context.init_global thy; fun const_syntax (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of thy)) c of SOME T => SOME (Lexicon.mark_const c, T, mx) | NONE => NONE) | const_syntax _ = NONE; - in syntax add mode (map_filter const_syntax args) thy end; + in syntax thy_ctxt add mode (map_filter const_syntax args) thy end; (* add constants *) @@ -425,7 +434,7 @@ in thy |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args) - |> syntax true Syntax.mode_default (map #2 args) + |> syntax ctxt true Syntax.mode_default (map #2 args) |> pair (map #3 args) end; @@ -493,20 +502,20 @@ in -fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], [])); -fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], [])); +fun parse_ast_translation atrs = update_syn_global Syntax.update_trfuns (mk atrs, [], [], []); +fun parse_translation trs = update_syn_global Syntax.update_trfuns ([], mk trs, [], []); fun print_translation tr's = - map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), [])); -fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, [])); -fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's)); + update_syn_global Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), []); +fun typed_print_translation tr's = update_syn_global Syntax.update_trfuns ([], [], mk tr's, []); +fun print_ast_translation atr's = update_syn_global Syntax.update_trfuns ([], [], [], mk atr's); end; (* translation rules *) -val add_trrules = map_syn o Syntax.update_trrules; -val del_trrules = map_syn o Syntax.remove_trrules; +val add_trrules = update_syn_global Syntax.update_trrules; +val del_trrules = update_syn_global Syntax.remove_trrules; (* naming *)