src/Pure/Syntax/syn_ext.ML
changeset 2913 ce271fa4d8e2
parent 2694 b98365c6e869
child 4050 543df9687d7b
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Apr 04 16:33:28 1997 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Apr 04 19:07:54 1997 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4        logtypes: string list,
     1.5        xprods: xprod list,
     1.6        consts: string list,
     1.7 +      prmodes: string list,
     1.8        parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
     1.9        parse_rules: (Ast.ast * Ast.ast) list,
    1.10        parse_translation: (string * (term list -> term)) list,
    1.11 @@ -286,13 +287,14 @@
    1.12      logtypes: string list,
    1.13      xprods: xprod list,
    1.14      consts: string list,
    1.15 +    prmodes: string list,
    1.16      parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.17      parse_rules: (Ast.ast * Ast.ast) list,
    1.18      parse_translation: (string * (term list -> term)) list,
    1.19      print_translation: (string * (typ -> term list -> term)) list,
    1.20      print_rules: (Ast.ast * Ast.ast) list,
    1.21      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.22 -    token_translation: (string * string * (string -> string * int)) list};
    1.23 +    token_translation: (string * string * (string -> string * int)) list}
    1.24  
    1.25  
    1.26  (* syn_ext *)
    1.27 @@ -311,6 +313,7 @@
    1.28        logtypes = logtypes',
    1.29        xprods = xprods,
    1.30        consts = filter is_xid (consts union mfix_consts),
    1.31 +      prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
    1.32        parse_ast_translation = parse_ast_translation,
    1.33        parse_rules = parse_rules,
    1.34        parse_translation = parse_translation,