# HG changeset patch
# User wenzelm
# Date 1197720512 -3600
# Node ID 615aecd485ad425242350470510bddf50c3129a3
# Parent  1546ffd849869f3d204af9a294b7598f6bb2aa0f
added separate_chars;

diff -r 1546ffd84986 -r 615aecd485ad src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Dec 15 13:08:31 2007 +0100
+++ b/src/Pure/General/symbol.ML	Sat Dec 15 13:08:32 2007 +0100
@@ -20,6 +20,7 @@
   val is_sync: symbol -> bool
   val malformed: symbol
   val end_malformed: symbol
+  val separate_chars: string -> string
   val is_regular: symbol -> bool
   val is_ascii: symbol -> bool
   val is_ascii_letter: symbol -> bool
@@ -112,7 +113,9 @@
 
 val malformed = "[[";
 val end_malformed = "]]";
-fun malformed_msg s = "Malformed symbolic character: " ^ quote (Output.escape_malformed s);
+
+val separate_chars = explode #> space_implode space;
+fun malformed_msg s = "Malformed symbolic character: " ^ quote (separate_chars s);
 
 fun is_regular s =
   not_eof s andalso s <> sync andalso s <> malformed andalso s <> end_malformed;