# HG changeset patch
# User oheimb
# Date 941015735 -7200
# Node ID cc1930ad1a88ab31bc14d797c5da052ea5b55337
# Parent  e31a3c0c2c1e0398d9a718a5ee9647869fe456b6
symbols in (error) messages now consistently with single backslash

diff -r e31a3c0c2c1e -r cc1930ad1a88 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Oct 27 11:13:25 1999 +0200
+++ b/src/Pure/Syntax/parser.ML	Wed Oct 27 11:15:35 1999 +0200
@@ -792,7 +792,7 @@
       if null toks then Pretty.str "Inner syntax error: unexpected end of input"
       else
         Pretty.block (Pretty.str "Inner syntax error at: \"" ::
-          Pretty.breaks (map (Pretty.str o Symbol.output o str_of_token)
+          Pretty.breaks (map (Pretty.str o str_of_token)
 		 (rev (tl (rev toks)))) @
           [Pretty.str "\""]);
     val expected =
diff -r e31a3c0c2c1e -r cc1930ad1a88 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Oct 27 11:13:25 1999 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Oct 27 11:15:35 1999 +0200
@@ -353,12 +353,11 @@
     val chars = Symbol.explode str;
     val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
 
-    fun show_pt pt =
-      warning (Symbol.output (Pretty.string_of 
-		(Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt))));
+    fun show_pt pt = warning (Pretty.string_of 
+			(Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
   in
     if length pts > ! ambiguity_level then
-      (warning ("Ambiguous input " ^ quote (Symbol.output str));
+      (warning ("Ambiguous input " ^ quote str);
        warning "produces the following parse trees:";
        seq show_pt pts)
     else ();