src/Pure/Syntax/syntax.ML
changeset 35412 b8dead547d9e
parent 35394 11f58c600707
child 35429 afa8cf9e63d8
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon Mar 01 09:47:44 2010 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Mar 01 17:07:36 2010 +0100
     1.3 @@ -59,7 +59,6 @@
     1.4      Proof.context -> syntax -> bool -> term -> Pretty.T
     1.5    val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
     1.6    val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T
     1.7 -  val update_type_gram: (string * int * mixfix) list -> syntax -> syntax
     1.8    val update_consts: string list -> syntax -> syntax
     1.9    val update_trfuns:
    1.10      (string * ((ast list -> ast) * stamp)) list *
    1.11 @@ -73,9 +72,8 @@
    1.12      (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
    1.13    val extend_tokentrfuns: (string * string * (Proof.context -> string -> Pretty.T)) list ->
    1.14      syntax -> syntax
    1.15 -  val update_const_gram: (string -> bool) ->
    1.16 -    mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.17 -  val remove_const_gram: (string -> bool) ->
    1.18 +  val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.19 +  val update_const_gram: bool -> (string -> bool) ->
    1.20      mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.21    val update_trrules: Proof.context -> (string -> bool) -> syntax ->
    1.22      (string * string) trrule list -> syntax -> syntax
    1.23 @@ -669,17 +667,16 @@
    1.24  
    1.25  fun ext_syntax f decls = update_syntax mode_default (f decls);
    1.26  
    1.27 -val update_type_gram       = ext_syntax Mixfix.syn_ext_types;
    1.28 -val update_consts          = ext_syntax SynExt.syn_ext_const_names;
    1.29 -val update_trfuns          = ext_syntax SynExt.syn_ext_trfuns;
    1.30 +val update_consts = ext_syntax SynExt.syn_ext_const_names;
    1.31 +val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
    1.32  val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
    1.33 -val extend_tokentrfuns     = ext_syntax SynExt.syn_ext_tokentrfuns;
    1.34 +val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
    1.35  
    1.36 -fun update_const_gram is_logtype prmode decls =
    1.37 -  update_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
    1.38 +fun update_type_gram add prmode decls =
    1.39 +  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
    1.40  
    1.41 -fun remove_const_gram is_logtype prmode decls =
    1.42 -  remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
    1.43 +fun update_const_gram add is_logtype prmode decls =
    1.44 +  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
    1.45  
    1.46  fun update_trrules ctxt is_logtype syn =
    1.47    ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;