src/Pure/ML/ml_syntax.ML
changeset 58978 e42da880c61e
parent 56184 a2bd40830593
child 62528 c8c532b22947
--- a/src/Pure/ML/ml_syntax.ML	Tue Nov 11 15:55:31 2014 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Tue Nov 11 18:16:25 2014 +0100
@@ -20,6 +20,7 @@
   val print_strings: string list -> string
   val print_properties: Properties.T -> string
   val print_position: Position.T -> string
+  val print_range: Position.range -> string
   val make_binding: string * Position.T -> string
   val print_indexname: indexname -> string
   val print_class: class -> string
@@ -77,8 +78,15 @@
 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);
-fun make_binding (name, pos) = "Binding.make " ^ print_pair print_string print_position (name, pos);
+
+fun print_position pos =
+  "Position.of_properties " ^ print_properties (Position.properties_of pos);
+
+fun print_range range =
+  "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);
+
+fun make_binding (name, pos) =
+  "Binding.make " ^ print_pair print_string print_position (name, pos);
 
 val print_indexname = print_pair print_string print_int;