replaced const_syntax by notation, which operates on terms;
authorwenzelm
Tue Nov 07 11:46:48 2006 +0100 (2006-11-07)
changeset 212062af4c7b3f7ef
parent 21205 dfe338ec9f9c
child 21207 cef082634be9
replaced const_syntax by notation, which operates on terms;
src/Pure/Isar/local_theory.ML
src/Pure/Isar/specification.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Tue Nov 07 11:46:47 2006 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Nov 07 11:46:48 2006 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4      local_theory -> (term * (bstring * thm)) * local_theory
     1.5    val note: (bstring * Attrib.src list) * thm list ->
     1.6      local_theory -> (bstring * thm list) * Proof.context
     1.7 -  val const_syntax: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
     1.8 +  val notation: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     1.9    val abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> local_theory -> local_theory
    1.10    val init: string option -> operations -> Proof.context -> local_theory
    1.11    val reinit: local_theory -> local_theory
    1.12 @@ -153,12 +153,11 @@
    1.13  
    1.14  fun note (a, ths) lthy = lthy |> notes [(a, [(ths, [])])] |>> hd;
    1.15  
    1.16 -fun const_syntax mode args =
    1.17 -  term_syntax
    1.18 -    (Context.mapping (Sign.add_const_syntax mode args) (ProofContext.add_const_syntax mode args));
    1.19 +fun notation mode args = term_syntax
    1.20 +  (Context.mapping (Sign.add_notation mode args) (ProofContext.add_notation mode args));
    1.21  
    1.22 -fun abbrevs mode args =
    1.23 -  term_syntax (Context.mapping (Sign.add_abbrevs mode args) (ProofContext.add_abbrevs mode args));
    1.24 +fun abbrevs mode args = term_syntax
    1.25 +  (Context.mapping (Sign.add_abbrevs mode args) (ProofContext.add_abbrevs mode args));
    1.26  
    1.27  
    1.28  (* init -- exit *)
     2.1 --- a/src/Pure/Isar/specification.ML	Tue Nov 07 11:46:47 2006 +0100
     2.2 +++ b/src/Pure/Isar/specification.ML	Tue Nov 07 11:46:48 2006 +0100
     2.3 @@ -34,8 +34,8 @@
     2.4      local_theory -> local_theory
     2.5    val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
     2.6      local_theory -> local_theory
     2.7 -  val const_syntax: Syntax.mode -> (xstring * mixfix) list -> local_theory -> local_theory
     2.8 -  val const_syntax_i: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
     2.9 +  val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    2.10 +  val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    2.11    val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    2.12      -> local_theory -> (bstring * thm list) list * local_theory
    2.13    val theorems_i: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
    2.14 @@ -174,12 +174,11 @@
    2.15  
    2.16  (* const syntax *)
    2.17  
    2.18 -fun gen_syntax intern_const mode raw_args lthy =
    2.19 -  let val args = raw_args |> map (apfst (intern_const (ProofContext.consts_of lthy)))
    2.20 -  in lthy |> LocalTheory.const_syntax mode args end;
    2.21 +fun gen_notation prep_const mode args lthy =
    2.22 +  lthy |> LocalTheory.notation mode (map (apfst (prep_const lthy)) args);
    2.23  
    2.24 -val const_syntax = gen_syntax Consts.intern;
    2.25 -val const_syntax_i = gen_syntax (K I);
    2.26 +val notation = gen_notation ProofContext.read_const;
    2.27 +val notation_i = gen_notation (K I);
    2.28  
    2.29  
    2.30  (* fact statements *)
    2.31 @@ -220,7 +219,7 @@
    2.32    let
    2.33      val _ = LocalTheory.assert lthy0;
    2.34      val thy = ProofContext.theory_of lthy0;
    2.35 -    
    2.36 +
    2.37      val (loc, ctxt, lthy) =
    2.38        (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
    2.39          (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)
     3.1 --- a/src/Pure/sign.ML	Tue Nov 07 11:46:47 2006 +0100
     3.2 +++ b/src/Pure/sign.ML	Tue Nov 07 11:46:48 2006 +0100
     3.3 @@ -191,7 +191,7 @@
     3.4    val read_term: theory -> string -> term
     3.5    val read_prop: theory -> string -> term
     3.6    val add_consts_authentic: (bstring * typ * mixfix) list -> theory -> theory
     3.7 -  val add_const_syntax: Syntax.mode -> (string * mixfix) list -> theory -> theory
     3.8 +  val add_notation: Syntax.mode -> (term * mixfix) list -> theory -> theory
     3.9    val add_abbrevs: Syntax.mode -> ((bstring * mixfix) * term) list -> theory -> theory
    3.10    include SIGN_THEORY
    3.11  end
    3.12 @@ -713,8 +713,11 @@
    3.13  val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
    3.14  val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
    3.15  
    3.16 -fun add_const_syntax mode args thy =
    3.17 -  thy |> add_modesyntax_i mode (map (Consts.syntax (consts_of thy)) args);
    3.18 +fun const_syntax thy (Const (c, _), mx) = SOME (Consts.syntax (consts_of thy) (c, mx))
    3.19 +  | const_syntax _ _ = NONE;
    3.20 +
    3.21 +fun add_notation mode args thy =
    3.22 +  thy |> add_modesyntax_i mode (map_filter (const_syntax thy) args);
    3.23  
    3.24  
    3.25  (* add constants *)