# HG changeset patch # User wenzelm # Date 1192030316 -7200 # Node ID 5f00e3532418cc216dcad1be061c51c247234fed # Parent c12c16a680a06453d73ee804da4c023dcbaf6c66 generalized notation interface (add or del); diff -r c12c16a680a0 -r 5f00e3532418 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Oct 10 17:31:55 2007 +0200 +++ b/src/Pure/Isar/class.ML Wed Oct 10 17:31:56 2007 +0200 @@ -800,7 +800,7 @@ val ty' = fastype_of rhs'; in thy - |> Sign.add_notation prmode [(Const (c', ty'), syn)] + |> Sign.notation true prmode [(Const (c', ty'), syn)] |> register_abbrev class (c', ty') |> pair c' end; diff -r c12c16a680a0 -r 5f00e3532418 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Wed Oct 10 17:31:55 2007 +0200 +++ b/src/Pure/Isar/local_theory.ML Wed Oct 10 17:31:56 2007 +0200 @@ -36,7 +36,7 @@ val declaration: declaration -> local_theory -> local_theory val note: string -> (bstring * Attrib.src list) * thm list -> local_theory -> (bstring * thm list) * local_theory - val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory + val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory val target_morphism: local_theory -> morphism val target_naming: local_theory -> NameSpace.naming val target_name: local_theory -> bstring -> string @@ -167,9 +167,9 @@ ProofContext.export_morphism lthy (target_of lthy) $> Morphism.thm_morphism Goal.norm_result; -fun notation mode raw_args lthy = +fun notation add mode raw_args lthy = let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args - in term_syntax (ProofContext.target_notation mode args) lthy end; + in term_syntax (ProofContext.target_notation add mode args) lthy end; val target_name = NameSpace.full o target_naming; diff -r c12c16a680a0 -r 5f00e3532418 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Oct 10 17:31:55 2007 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Oct 10 17:31:56 2007 +0200 @@ -139,9 +139,8 @@ val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context val get_case: Proof.context -> string -> string option list -> RuleCases.T - val add_notation: Syntax.mode -> (term * mixfix) list -> - Proof.context -> Proof.context - val target_notation: Syntax.mode -> (term * mixfix) list -> morphism -> + val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context + val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism -> Context.generic -> Context.generic val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> Markup.property list -> @@ -991,11 +990,6 @@ (* authentic constants *) -fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx)) - | const_syntax ctxt (Const (c, _), mx) = - Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx)) - | const_syntax _ _ = NONE; - fun context_const_ast_tr ctxt [Syntax.Variable c] = let val consts = consts_of ctxt; @@ -1013,13 +1007,24 @@ (* notation *) -fun add_notation mode args ctxt = - ctxt |> map_syntax - (LocalSyntax.add_modesyntax (theory_of ctxt) mode (map_filter (const_syntax ctxt) args)); +local + +fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx)) + | const_syntax ctxt (Const (c, _), mx) = + Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx)) + | const_syntax _ _ = NONE; + +in -fun target_notation mode args phi = +fun notation add mode args ctxt = + ctxt |> map_syntax + (LocalSyntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args)); + +fun target_notation add mode args phi = let val args' = filter (fn (t, _) => Term.equiv_types (t, Morphism.term phi t)) args; - in Context.mapping (Sign.add_notation mode args') (add_notation mode args') end; + in Context.mapping (Sign.notation add mode args') (notation add mode args') end; + +end; (* local constants *) diff -r c12c16a680a0 -r 5f00e3532418 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Wed Oct 10 17:31:55 2007 +0200 +++ b/src/Pure/Isar/specification.ML Wed Oct 10 17:31:56 2007 +0200 @@ -42,8 +42,8 @@ local_theory -> local_theory val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string -> local_theory -> local_theory - val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory - val notation_cmd: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory + val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory + val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> local_theory -> (bstring * thm list) list * local_theory val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list @@ -221,8 +221,8 @@ (* notation *) -fun gen_notation prep_const mode args lthy = - lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args); +fun gen_notation prep_const add mode args lthy = + lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args); val notation = gen_notation (K I); val notation_cmd = gen_notation ProofContext.read_const; diff -r c12c16a680a0 -r 5f00e3532418 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Wed Oct 10 17:31:55 2007 +0200 +++ b/src/Pure/Isar/theory_target.ML Wed Oct 10 17:31:56 2007 +0200 @@ -175,7 +175,7 @@ (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg') #-> (fn (lhs, _) => Term.equiv_types (rhs, rhs') ? - Morphism.form (ProofContext.target_notation prmode [(lhs, mx)]))) + Morphism.form (ProofContext.target_notation true prmode [(lhs, mx)]))) end; fun internal_abbrev loc prmode ((c, mx), t) lthy = lthy @@ -279,10 +279,11 @@ lthy |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u')) - |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)]) - #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs)) - #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1) - #> local_abbrev (c, rhs)) + |-> (fn (lhs as Const (full_c, _), rhs) => + LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)]) + #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs)) + #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1) + #> local_abbrev (c, rhs)) end; diff -r c12c16a680a0 -r 5f00e3532418 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Oct 10 17:31:55 2007 +0200 +++ b/src/Pure/sign.ML Wed Oct 10 17:31:56 2007 +0200 @@ -158,7 +158,7 @@ val read_prop: theory -> string -> term val add_consts_authentic: Markup.property list -> (bstring * typ * mixfix) list -> theory -> theory - val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory + val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory val add_abbrev: string -> Markup.property list -> bstring * term -> theory -> (term * term) * theory include SIGN_THEORY @@ -665,8 +665,8 @@ fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx) | const_syntax _ _ = NONE; -fun add_notation mode args thy = - thy |> add_modesyntax_i mode (map_filter (const_syntax thy) args); +fun notation add mode args thy = thy + |> (if add then add_modesyntax_i else del_modesyntax_i) mode (map_filter (const_syntax thy) args); (* add constants *)