added token_translation interface;
authorwenzelm
Fri Feb 28 16:40:08 1997 +0100 (1997-02-28)
changeset 2694b98365c6e869
parent 2693 8300bba275e3
child 2695 871b69a4b78f
added token_translation interface;
src/Pure/Syntax/syn_ext.ML
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Feb 28 16:39:30 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Feb 28 16:40:08 1997 +0100
     1.3 @@ -40,15 +40,18 @@
     1.4        parse_translation: (string * (term list -> term)) list,
     1.5        print_translation: (string * (typ -> term list -> term)) list,
     1.6        print_rules: (Ast.ast * Ast.ast) list,
     1.7 -      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list}
     1.8 +      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
     1.9 +      token_translation: (string * string * (string -> string * int)) list}
    1.10    val mk_syn_ext: bool -> string list -> mfix list ->
    1.11      string list -> (string * (Ast.ast list -> Ast.ast)) list *
    1.12      (string * (term list -> term)) list *
    1.13      (string * (typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.14 +    -> (string * string * (string -> string * int)) list
    1.15      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.16    val syn_ext: string list -> mfix list -> string list ->
    1.17      (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    1.18      (string * (typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.19 +    -> (string * string * (string -> string * int)) list
    1.20      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.21    val syn_ext_logtypes: string list -> syn_ext
    1.22    val syn_ext_const_names: string list -> string list -> syn_ext
    1.23 @@ -59,6 +62,8 @@
    1.24      (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.25      -> syn_ext
    1.26    val syn_ext_trfunsT: string list -> (string * (typ -> term list -> term)) list -> syn_ext
    1.27 +  val syn_ext_tokentrfuns: string list
    1.28 +    -> (string * string * (string -> string * int)) list -> syn_ext
    1.29    val pure_ext: syn_ext
    1.30    end;
    1.31  
    1.32 @@ -67,6 +72,7 @@
    1.33  
    1.34  open Lexicon Ast;
    1.35  
    1.36 +
    1.37  (** misc definitions **)
    1.38  
    1.39  (* syntactic categories *)
    1.40 @@ -285,12 +291,13 @@
    1.41      parse_translation: (string * (term list -> term)) list,
    1.42      print_translation: (string * (typ -> term list -> term)) list,
    1.43      print_rules: (Ast.ast * Ast.ast) list,
    1.44 -    print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list};
    1.45 +    print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.46 +    token_translation: (string * string * (string -> string * int)) list};
    1.47  
    1.48  
    1.49  (* syn_ext *)
    1.50  
    1.51 -fun mk_syn_ext convert logtypes mfixes consts trfuns rules =
    1.52 +fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns rules =
    1.53    let
    1.54      val (parse_ast_translation, parse_translation, print_translation,
    1.55        print_ast_translation) = trfuns;
    1.56 @@ -309,28 +316,32 @@
    1.57        parse_translation = parse_translation,
    1.58        print_translation = print_translation,
    1.59        print_rules = print_rules,
    1.60 -      print_ast_translation = print_ast_translation}
    1.61 +      print_ast_translation = print_ast_translation,
    1.62 +      token_translation = tokentrfuns}
    1.63    end;
    1.64  
    1.65  
    1.66  val syn_ext = mk_syn_ext true;
    1.67  
    1.68  fun syn_ext_logtypes logtypes =
    1.69 -  syn_ext logtypes [] [] ([], [], [], []) ([], []);
    1.70 +  syn_ext logtypes [] [] ([], [], [], []) [] ([], []);
    1.71  
    1.72  fun syn_ext_const_names logtypes cs =
    1.73 -  syn_ext logtypes [] cs ([], [], [], []) ([], []);
    1.74 +  syn_ext logtypes [] cs ([], [], [], []) [] ([], []);
    1.75  
    1.76  fun syn_ext_rules logtypes rules =
    1.77 -  syn_ext logtypes [] [] ([], [], [], []) rules;
    1.78 +  syn_ext logtypes [] [] ([], [], [], []) [] rules;
    1.79  
    1.80  fun fix_tr' f _ args = f args;
    1.81  
    1.82  fun syn_ext_trfuns logtypes (atrs, trs, tr's, atr's) =
    1.83 -  syn_ext logtypes [] [] (atrs, trs, map (apsnd fix_tr') tr's, atr's) ([], []);
    1.84 +  syn_ext logtypes [] [] (atrs, trs, map (apsnd fix_tr') tr's, atr's) [] ([], []);
    1.85  
    1.86  fun syn_ext_trfunsT logtypes tr's =
    1.87 -  syn_ext logtypes [] [] ([], [], tr's, []) ([], []);
    1.88 +  syn_ext logtypes [] [] ([], [], tr's, []) [] ([], []);
    1.89 +
    1.90 +fun syn_ext_tokentrfuns logtypes tokentrfuns =
    1.91 +  syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []);
    1.92  
    1.93  
    1.94  (* pure_ext *)
    1.95 @@ -345,6 +356,7 @@
    1.96     Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
    1.97    []
    1.98    ([], [], [], [])
    1.99 +  []
   1.100    ([], []);
   1.101  
   1.102  end;
     2.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Feb 28 16:39:30 1997 +0100
     2.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Feb 28 16:40:08 1997 +0100
     2.3 @@ -338,7 +338,8 @@
     2.4    \ val parse_translation = [];\n\
     2.5    \ val print_translation = [];\n\
     2.6    \ val typed_print_translation = [];\n\
     2.7 -  \ val print_ast_translation = [];";
     2.8 +  \ val print_ast_translation = [];\n\
     2.9 +  \ val token_translation = [];";
    2.10  
    2.11  val trfun_args =
    2.12    "(parse_ast_translation, parse_translation, \
    2.13 @@ -482,6 +483,7 @@
    2.14          \|> add_trfuns\n"
    2.15          ^ trfun_args ^ "\n\
    2.16          \|> add_trfunsT typed_print_translation \n\
    2.17 +        \|> add_tokentrfuns token_translation \n\
    2.18          \\n"
    2.19          ^ extxt ^ "\n\
    2.20          \\n\