# HG changeset patch
# User wenzelm
# Date 1236113320 -3600
# Node ID a2094a8c1672960686197eb0e87fafee3a931080
# Parent  9861257b18e6319ebc402d23417d8a9c604565a4
added print_properties, print_position (again);

diff -r 9861257b18e6 -r a2094a8c1672 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Tue Mar 03 19:30:43 2009 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Tue Mar 03 21:48:40 2009 +0100
@@ -18,6 +18,8 @@
   val print_char: string -> string
   val print_string: string -> string
   val print_strings: string list -> string
+  val print_properties: Properties.T -> string
+  val print_position: Position.T -> string
   val print_indexname: indexname -> string
   val print_class: class -> string
   val print_sort: sort -> string
@@ -68,6 +70,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;