generalized notation interface (add or del);
authorwenzelm
Wed Oct 10 17:31:56 2007 +0200 (2007-10-10)
changeset 249495f00e3532418
parent 24948 c12c16a680a0
child 24950 106fc30769a9
generalized notation interface (add or del);
src/Pure/Isar/class.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/class.ML	Wed Oct 10 17:31:55 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Oct 10 17:31:56 2007 +0200
     1.3 @@ -800,7 +800,7 @@
     1.4      val ty' = fastype_of rhs';
     1.5    in
     1.6      thy
     1.7 -    |> Sign.add_notation prmode [(Const (c', ty'), syn)]
     1.8 +    |> Sign.notation true prmode [(Const (c', ty'), syn)]
     1.9      |> register_abbrev class (c', ty')
    1.10      |> pair c'
    1.11    end;
     2.1 --- a/src/Pure/Isar/local_theory.ML	Wed Oct 10 17:31:55 2007 +0200
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Oct 10 17:31:56 2007 +0200
     2.3 @@ -36,7 +36,7 @@
     2.4    val declaration: declaration -> local_theory -> local_theory
     2.5    val note: string -> (bstring * Attrib.src list) * thm list ->
     2.6      local_theory -> (bstring * thm list) * local_theory
     2.7 -  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     2.8 +  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     2.9    val target_morphism: local_theory -> morphism
    2.10    val target_naming: local_theory -> NameSpace.naming
    2.11    val target_name: local_theory -> bstring -> string
    2.12 @@ -167,9 +167,9 @@
    2.13    ProofContext.export_morphism lthy (target_of lthy) $>
    2.14    Morphism.thm_morphism Goal.norm_result;
    2.15  
    2.16 -fun notation mode raw_args lthy =
    2.17 +fun notation add mode raw_args lthy =
    2.18    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    2.19 -  in term_syntax (ProofContext.target_notation mode args) lthy end;
    2.20 +  in term_syntax (ProofContext.target_notation add mode args) lthy end;
    2.21  
    2.22  val target_name = NameSpace.full o target_naming;
    2.23  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Wed Oct 10 17:31:55 2007 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Oct 10 17:31:56 2007 +0200
     3.3 @@ -139,9 +139,8 @@
     3.4    val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
     3.5    val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
     3.6    val get_case: Proof.context -> string -> string option list -> RuleCases.T
     3.7 -  val add_notation: Syntax.mode -> (term * mixfix) list ->
     3.8 -    Proof.context -> Proof.context
     3.9 -  val target_notation: Syntax.mode -> (term * mixfix) list -> morphism ->
    3.10 +  val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
    3.11 +  val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
    3.12      Context.generic -> Context.generic
    3.13    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
    3.14    val add_abbrev: string -> Markup.property list ->
    3.15 @@ -991,11 +990,6 @@
    3.16  
    3.17  (* authentic constants *)
    3.18  
    3.19 -fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
    3.20 -  | const_syntax ctxt (Const (c, _), mx) =
    3.21 -      Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
    3.22 -  | const_syntax _ _ = NONE;
    3.23 -
    3.24  fun context_const_ast_tr ctxt [Syntax.Variable c] =
    3.25        let
    3.26          val consts = consts_of ctxt;
    3.27 @@ -1013,13 +1007,24 @@
    3.28  
    3.29  (* notation *)
    3.30  
    3.31 -fun add_notation mode args ctxt =
    3.32 -  ctxt |> map_syntax
    3.33 -    (LocalSyntax.add_modesyntax (theory_of ctxt) mode (map_filter (const_syntax ctxt) args));
    3.34 +local
    3.35 +
    3.36 +fun const_syntax ctxt (Free (x, T), mx) = SOME (true, (x, T, mx))
    3.37 +  | const_syntax ctxt (Const (c, _), mx) =
    3.38 +      Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
    3.39 +  | const_syntax _ _ = NONE;
    3.40 +
    3.41 +in
    3.42  
    3.43 -fun target_notation mode args phi =
    3.44 +fun notation add mode args ctxt =
    3.45 +  ctxt |> map_syntax
    3.46 +    (LocalSyntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
    3.47 +
    3.48 +fun target_notation add mode args phi =
    3.49    let val args' = filter (fn (t, _) => Term.equiv_types (t, Morphism.term phi t)) args;
    3.50 -  in Context.mapping (Sign.add_notation mode args') (add_notation mode args') end;
    3.51 +  in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
    3.52 +
    3.53 +end;
    3.54  
    3.55  
    3.56  (* local constants *)
     4.1 --- a/src/Pure/Isar/specification.ML	Wed Oct 10 17:31:55 2007 +0200
     4.2 +++ b/src/Pure/Isar/specification.ML	Wed Oct 10 17:31:56 2007 +0200
     4.3 @@ -42,8 +42,8 @@
     4.4      local_theory -> local_theory
     4.5    val abbreviation_cmd: Syntax.mode -> (string * string option * mixfix) option * string ->
     4.6      local_theory -> local_theory
     4.7 -  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     4.8 -  val notation_cmd: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
     4.9 +  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    4.10 +  val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    4.11    val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
    4.12      -> local_theory -> (bstring * thm list) list * local_theory
    4.13    val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    4.14 @@ -221,8 +221,8 @@
    4.15  
    4.16  (* notation *)
    4.17  
    4.18 -fun gen_notation prep_const mode args lthy =
    4.19 -  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
    4.20 +fun gen_notation prep_const add mode args lthy =
    4.21 +  lthy |> LocalTheory.notation add mode (map (apfst (prep_const lthy)) args);
    4.22  
    4.23  val notation = gen_notation (K I);
    4.24  val notation_cmd = gen_notation ProofContext.read_const;
     5.1 --- a/src/Pure/Isar/theory_target.ML	Wed Oct 10 17:31:55 2007 +0200
     5.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Oct 10 17:31:56 2007 +0200
     5.3 @@ -175,7 +175,7 @@
     5.4        (Sign.add_abbrev Syntax.internalM [] arg') (ProofContext.add_abbrev Syntax.internalM [] arg')
     5.5      #-> (fn (lhs, _) =>
     5.6        Term.equiv_types (rhs, rhs') ?
     5.7 -        Morphism.form (ProofContext.target_notation prmode [(lhs, mx)])))
     5.8 +        Morphism.form (ProofContext.target_notation true prmode [(lhs, mx)])))
     5.9    end;
    5.10  
    5.11  fun internal_abbrev loc prmode ((c, mx), t) lthy = lthy
    5.12 @@ -279,10 +279,11 @@
    5.13      lthy
    5.14      |> LocalTheory.theory_result
    5.15          (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
    5.16 -    |-> (fn (lhs as Const (full_c, _), rhs) => LocalTheory.theory (Sign.add_notation prmode [(lhs, mx3)])
    5.17 -    #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
    5.18 -    #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)
    5.19 -    #> local_abbrev (c, rhs))
    5.20 +    |-> (fn (lhs as Const (full_c, _), rhs) =>
    5.21 +          LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)])
    5.22 +          #> is_loc ? internal_abbrev loc prmode ((c, mx2), Term.list_comb (Const (full_c, U), xs))
    5.23 +          #> add_abbrev_in_class some_class ((c, Term.list_comb (Const (full_c, U), xs)), mx1)
    5.24 +          #> local_abbrev (c, rhs))
    5.25    end;
    5.26  
    5.27  
     6.1 --- a/src/Pure/sign.ML	Wed Oct 10 17:31:55 2007 +0200
     6.2 +++ b/src/Pure/sign.ML	Wed Oct 10 17:31:56 2007 +0200
     6.3 @@ -158,7 +158,7 @@
     6.4    val read_prop: theory -> string -> term
     6.5    val add_consts_authentic: Markup.property list ->
     6.6      (bstring * typ * mixfix) list -> theory -> theory
     6.7 -  val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
     6.8 +  val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
     6.9    val add_abbrev: string -> Markup.property list ->
    6.10      bstring * term -> theory -> (term * term) * theory
    6.11    include SIGN_THEORY
    6.12 @@ -665,8 +665,8 @@
    6.13  fun const_syntax thy (Const (c, _), mx) = try (Consts.syntax (consts_of thy)) (c, mx)
    6.14    | const_syntax _ _ = NONE;
    6.15  
    6.16 -fun add_notation mode args thy =
    6.17 -  thy |> add_modesyntax_i mode (map_filter (const_syntax thy) args);
    6.18 +fun notation add mode args thy = thy
    6.19 +  |> (if add then add_modesyntax_i else del_modesyntax_i) mode (map_filter (const_syntax thy) args);
    6.20  
    6.21  
    6.22  (* add constants *)