src/Pure/Syntax/syntax.ML
changeset 14648 0e67b385a6df
parent 14598 7009f59711e3
child 14687 e089757b952a
     1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Apr 22 10:59:19 2004 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Apr 22 10:59:41 2004 +0200
     1.3 @@ -24,6 +24,14 @@
     1.4    include SYN_TRANS1
     1.5    include MIXFIX1
     1.6    include PRINTER0
     1.7 +  val extend_trtab: ('a * stamp) Symtab.table -> (string * 'a) list -> string
     1.8 +    -> ('a * stamp) Symtab.table
     1.9 +  val merge_trtabs: ('a * stamp) Symtab.table -> ('a * stamp) Symtab.table -> string
    1.10 +    -> ('a * stamp) Symtab.table
    1.11 +  val merge_tr'tabs: ('a * stamp) list Symtab.table -> ('a * stamp) list Symtab.table
    1.12 +    -> ('a * stamp) list Symtab.table
    1.13 +  val extend_tr'tab: ('a * stamp) list Symtab.table -> (string * 'a) list
    1.14 +    -> ('a * stamp) list Symtab.table
    1.15    datatype 'a trrule =
    1.16      ParseRule of 'a * 'a |
    1.17      PrintRule of 'a * 'a |
    1.18 @@ -36,11 +44,10 @@
    1.19    val extend_trfuns:
    1.20      (string * (ast list -> ast)) list *
    1.21      (string * (term list -> term)) list *
    1.22 -    (string * (term list -> term)) list *
    1.23 +    (string * (bool -> typ -> term list -> term)) list *
    1.24      (string * (ast list -> ast)) list -> syntax -> syntax
    1.25 -  val extend_trfunsT: (string * (bool -> typ -> term list -> term)) list -> syntax -> syntax
    1.26    val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
    1.27 -  val extend_trrules: (string * string) trrule list -> syntax -> syntax
    1.28 +  val extend_trrules: syntax -> (string * string) trrule list -> syntax -> syntax
    1.29    val extend_trrules_i: ast trrule list -> syntax -> syntax
    1.30    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
    1.31    val merge_syntaxes: syntax -> syntax -> syntax
    1.32 @@ -485,12 +492,10 @@
    1.33  
    1.34  val extend_trfuns = ext_syntax SynExt.syn_ext_trfuns ("", true);
    1.35  
    1.36 -val extend_trfunsT = ext_syntax SynExt.syn_ext_trfunsT ("", true);
    1.37 -
    1.38  val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns ("", true);
    1.39  
    1.40 -fun extend_trrules rules syn =
    1.41 -  ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules (read_pattern syn) rules) syn;
    1.42 +fun extend_trrules syn rules =
    1.43 +  ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules (read_pattern syn) rules);
    1.44  
    1.45  fun extend_trrules_i rules = ext_syntax SynExt.syn_ext_rules ("", true) (prep_rules I rules);
    1.46