src/Pure/Syntax/syntax.ML
changeset 4887 bbc13af86c16
parent 4703 a50ab39756db
child 5692 2e873c5f0e2c
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat May 02 13:27:06 1998 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat May 02 13:27:42 1998 +0200
     1.3 @@ -47,6 +47,7 @@
     1.4    val print_gram: syntax -> unit
     1.5    val print_trans: syntax -> unit
     1.6    val print_syntax: syntax -> unit
     1.7 +  val trfun_names: syntax -> string list * string list * string list * string list
     1.8    val test_read: syntax -> string -> string -> unit
     1.9    val read: syntax -> typ -> string -> term list
    1.10    val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
    1.11 @@ -71,7 +72,7 @@
    1.12  (*does not subsume typed print translations*)
    1.13  type 'a trtab = (('a list -> 'a) * stamp) Symtab.table;
    1.14  
    1.15 -val dest_trtab = Symtab.dest;
    1.16 +fun dest_trtab tab = map fst (Symtab.dest tab);
    1.17  
    1.18  fun lookup_trtab tab c =
    1.19    apsome fst (Symtab.lookup (tab, c));
    1.20 @@ -269,6 +270,7 @@
    1.21  val pure_syn = extend_syntax ("", true) type_syn pure_ext;
    1.22  
    1.23  
    1.24 +
    1.25  (** inspect syntax **)
    1.26  
    1.27  fun pretty_strs_qs name strs =
    1.28 @@ -294,7 +296,7 @@
    1.29  fun print_trans (Syntax tabs) =
    1.30    let
    1.31      fun pretty_trtab name tab =
    1.32 -      pretty_strs_qs name (map fst (dest_trtab tab));
    1.33 +      pretty_strs_qs name (dest_trtab tab);
    1.34  
    1.35      fun pretty_ruletab name tab =
    1.36        Pretty.big_list name (map pretty_rule (dest_ruletab tab));
    1.37 @@ -320,6 +322,13 @@
    1.38  fun print_syntax syn = (print_gram syn; print_trans syn);
    1.39  
    1.40  
    1.41 +(* trfun_names *)
    1.42 +
    1.43 +fun trfun_names (Syntax {parse_ast_trtab, parse_trtab, print_trtab, print_ruletab, ...}) =
    1.44 +  (dest_trtab parse_ast_trtab, dest_trtab parse_trtab,
    1.45 +    dest_trtab print_trtab, dest_trtab print_ruletab);
    1.46 +
    1.47 +
    1.48  
    1.49  (** read **)
    1.50