--- a/src/Pure/ML/ml_syntax.ML Thu Mar 20 16:04:30 2008 +0100
+++ b/src/Pure/ML/ml_syntax.ML Thu Mar 20 16:04:32 2008 +0100
@@ -19,6 +19,8 @@
val print_char: string -> string
val print_string: string -> string
val print_strings: string list -> string
+ val print_properties: Markup.property list -> string
+ val print_position: Position.T -> string
val print_indexname: indexname -> string
val print_class: class -> string
val print_sort: sort -> string
@@ -69,6 +71,9 @@
val print_string = quote o translate_string print_char;
val print_strings = print_list print_string;
+val print_properties = print_list (print_pair print_string print_string);
+fun print_position pos = "Position.of_properties " ^ print_properties (Position.properties_of pos);
+
val print_indexname = print_pair print_string print_int;
val print_class = print_string;