added print_properties, print_position (again);
authorwenzelm
Tue, 03 Mar 2009 21:48:40 +0100
changeset 30230a2094a8c1672
parent 30229 9861257b18e6
child 30231 b3f3ad327d4d
added print_properties, print_position (again);
src/Pure/ML/ml_syntax.ML
     1.1 --- a/src/Pure/ML/ml_syntax.ML	Tue Mar 03 19:30:43 2009 +0100
     1.2 +++ b/src/Pure/ML/ml_syntax.ML	Tue Mar 03 21:48:40 2009 +0100
     1.3 @@ -18,6 +18,8 @@
     1.4    val print_char: string -> string
     1.5    val print_string: string -> string
     1.6    val print_strings: string list -> string
     1.7 +  val print_properties: Properties.T -> string
     1.8 +  val print_position: Position.T -> string
     1.9    val print_indexname: indexname -> string
    1.10    val print_class: class -> string
    1.11    val print_sort: sort -> string
    1.12 @@ -68,6 +70,9 @@
    1.13  val print_string = quote o translate_string print_char;
    1.14  val print_strings = print_list print_string;
    1.15  
    1.16 +val print_properties = print_list (print_pair print_string print_string);
    1.17 +fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
    1.18 +
    1.19  val print_indexname = print_pair print_string print_int;
    1.20  
    1.21  val print_class = print_string;