src/Pure/sign.ML
changeset 35412 b8dead547d9e
parent 35395 ba804f4c82c6
child 35429 afa8cf9e63d8
     1.1 --- a/src/Pure/sign.ML	Mon Mar 01 09:47:44 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Mar 01 17:07:36 2010 +0100
     1.3 @@ -89,6 +89,7 @@
     1.4    val add_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
     1.5    val del_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
     1.6    val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
     1.7 +  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
     1.8    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
     1.9    val declare_const: (binding * typ) * mixfix -> theory -> term * theory
    1.10    val add_consts: (binding * string * mixfix) list -> theory -> theory
    1.11 @@ -439,7 +440,9 @@
    1.12  
    1.13  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.14    let
    1.15 -    val syn' = Syntax.update_type_gram (map (fn (a, n, mx) => (Name.of_binding a, n, mx)) types) syn;
    1.16 +    val syn' =
    1.17 +      Syntax.update_type_gram true Syntax.mode_default
    1.18 +        (map (fn (a, n, mx) => (Name.of_binding a, Syntax.make_type n, mx)) types) syn;
    1.19      val decls = map (fn (a, n, _) => (a, n)) types;
    1.20      val tsig' = fold (Type.add_type naming) decls tsig;
    1.21    in (naming, syn', tsig', consts) end);
    1.22 @@ -460,7 +463,9 @@
    1.23    thy |> map_sign (fn (naming, syn, tsig, consts) =>
    1.24      let
    1.25        val ctxt = ProofContext.init thy;
    1.26 -      val syn' = Syntax.update_type_gram [(Name.of_binding b, length vs, mx)] syn;
    1.27 +      val syn' =
    1.28 +        Syntax.update_type_gram true Syntax.mode_default
    1.29 +          [(Name.of_binding b, Syntax.make_type (length vs), mx)] syn;
    1.30        val abbr = (b, vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
    1.31          handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
    1.32        val tsig' = Type.add_abbrev naming abbr tsig;
    1.33 @@ -479,24 +484,30 @@
    1.34        handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
    1.35    in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
    1.36  
    1.37 -fun gen_add_syntax x = gen_syntax Syntax.update_const_gram x;
    1.38 +fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
    1.39  
    1.40  val add_modesyntax = gen_add_syntax Syntax.parse_typ;
    1.41  val add_modesyntax_i = gen_add_syntax (K I);
    1.42  val add_syntax = add_modesyntax Syntax.mode_default;
    1.43  val add_syntax_i = add_modesyntax_i Syntax.mode_default;
    1.44 -val del_modesyntax = gen_syntax Syntax.remove_const_gram Syntax.parse_typ;
    1.45 -val del_modesyntax_i = gen_syntax Syntax.remove_const_gram (K I);
    1.46 +val del_modesyntax = gen_syntax (Syntax.update_const_gram false) Syntax.parse_typ;
    1.47 +val del_modesyntax_i = gen_syntax (Syntax.update_const_gram false) (K I);
    1.48 +
    1.49 +fun type_notation add mode args =
    1.50 +  let
    1.51 +    fun type_syntax (Type (c, args), mx) =  (* FIXME authentic syntax *)
    1.52 +          SOME (Long_Name.base_name c, Syntax.make_type (length args), mx)
    1.53 +      | type_syntax _ = NONE;
    1.54 +  in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
    1.55  
    1.56  fun notation add mode args thy =
    1.57    let
    1.58 -    val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
    1.59      fun const_syntax (Const (c, _), mx) =
    1.60            (case try (Consts.type_scheme (consts_of thy)) c of
    1.61              SOME T => SOME (Syntax.mark_const c, T, mx)
    1.62            | NONE => NONE)
    1.63        | const_syntax _ = NONE;
    1.64 -  in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
    1.65 +  in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
    1.66  
    1.67  
    1.68  (* add constants *)