src/Pure/Syntax/syntax.ML
changeset 25387 d9ab1e3a8acb
parent 25122 f37d7dd25c88
child 25394 db25c98f32e1
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Nov 10 23:04:02 2007 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Nov 10 23:04:03 2007 +0100
     1.3 @@ -42,8 +42,6 @@
     1.4    val mode_default: mode
     1.5    val mode_input: mode
     1.6    val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax
     1.7 -  val extend_const_gram: (string -> bool) ->
     1.8 -    mode -> (string * typ * mixfix) list -> syntax -> syntax
     1.9    val extend_consts: string list -> syntax -> syntax
    1.10    val extend_trfuns:
    1.11      (string * ((ast list -> ast) * stamp)) list *
    1.12 @@ -56,8 +54,12 @@
    1.13      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    1.14      (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
    1.15    val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax
    1.16 +  val extend_const_gram: (string -> bool) ->
    1.17 +    mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.18    val remove_const_gram: (string -> bool) ->
    1.19      mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.20 +  val update_const_gram: (string -> bool) ->
    1.21 +    mode -> (string * typ * mixfix) list -> syntax -> syntax
    1.22    val extend_trrules: Proof.context -> (string -> bool) -> syntax ->
    1.23      (string * string) trrule list -> syntax -> syntax
    1.24    val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
    1.25 @@ -315,12 +317,13 @@
    1.26        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
    1.27        print_ast_trtab, tokentrtab, prtabs} = tabs;
    1.28      val input' = if inout then subtract (op =) xprods input else input;
    1.29 +    val changed = input <> input';
    1.30      fun if_inout xs = if inout then xs else [];
    1.31    in
    1.32      Syntax
    1.33      ({input = input',
    1.34 -      lexicon = if inout then Scan.make_lexicon (SynExt.delims_of input') else lexicon,
    1.35 -      gram = if inout then Parser.make_gram input' else gram,
    1.36 +      lexicon = if changed then Scan.make_lexicon (SynExt.delims_of input') else lexicon,
    1.37 +      gram = if changed then Parser.make_gram input' else gram,
    1.38        consts = consts,
    1.39        prmodes = prmodes,
    1.40        parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,
    1.41 @@ -616,19 +619,24 @@
    1.42  
    1.43  (** modify syntax **)
    1.44  
    1.45 -fun ext_syntax' f is_logtype prmode decls = extend_syntax prmode (f is_logtype decls);
    1.46 -fun ext_syntax f = ext_syntax' (K f) (K false) mode_default;
    1.47 +fun ext_syntax f decls = extend_syntax mode_default (f decls);
    1.48  
    1.49  val extend_type_gram       = ext_syntax Mixfix.syn_ext_types;
    1.50 -val extend_const_gram      = ext_syntax' Mixfix.syn_ext_consts;
    1.51  val extend_consts          = ext_syntax SynExt.syn_ext_const_names;
    1.52  val extend_trfuns          = ext_syntax SynExt.syn_ext_trfuns;
    1.53  val extend_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
    1.54  val extend_tokentrfuns     = ext_syntax SynExt.syn_ext_tokentrfuns;
    1.55  
    1.56 +fun extend_const_gram is_logtype prmode decls =
    1.57 +  extend_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
    1.58 +
    1.59  fun remove_const_gram is_logtype prmode decls =
    1.60    remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
    1.61  
    1.62 +fun update_const_gram is_logtype prmode decls =
    1.63 +  let val syn_ext = Mixfix.syn_ext_consts is_logtype decls
    1.64 +  in remove_syntax prmode syn_ext #> extend_syntax prmode syn_ext end;
    1.65 +
    1.66  fun extend_trrules ctxt is_logtype syn =
    1.67    ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
    1.68