# HG changeset patch
# User wenzelm
# Date 1165775849 -3600
# Node ID 6e08004d0476ba455e3bfb340adf0b8273b8c229
# Parent  093ca3efb13249cdb9dd98033b82280deed8f2a3
renamed str_of_XXX to print_XXX;

diff -r 093ca3efb132 -r 6e08004d0476 src/Pure/General/ml_syntax.ML
--- a/src/Pure/General/ml_syntax.ML	Sun Dec 10 19:37:28 2006 +0100
+++ b/src/Pure/General/ml_syntax.ML	Sun Dec 10 19:37:29 2006 +0100
@@ -11,10 +11,11 @@
   val reserved: Name.context
   val is_reserved: string -> bool
   val is_identifier: string -> bool
-  val str_of_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
-  val str_of_list: ('a -> string) -> 'a list -> string
-  val str_of_option: ('a -> string) -> 'a option -> string
-  val str_of_char: string -> string
+  val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
+  val print_list: ('a -> string) -> 'a list -> string
+  val print_option: ('a -> string) -> 'a option -> string
+  val print_char: string -> string
+  val print_string: string -> string
 end;
 
 structure ML_Syntax: ML_SYNTAX =
@@ -42,14 +43,14 @@
 
 (* unformatted output *)
 
-fun str_of_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
+fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
 
-fun str_of_list f = enclose "[" "]" o commas o map f;
+fun print_list f = enclose "[" "]" o commas o map f;
 
-fun str_of_option f NONE = "NONE"
-  | str_of_option f (SOME x) = "SOME (" ^ f x ^ ")";
+fun print_option f NONE = "NONE"
+  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
 
-fun str_of_char s =
+fun print_char s =
   if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
   else if s = "\"" then "\\\""
   else if s = "\\" then "\\\\"
@@ -60,6 +61,6 @@
       else "\\" ^ string_of_int c
     end;
 
-val str_of_string = quote o translate_string str_of_char;
+val print_string = quote o translate_string print_char;
 
 end;