# HG changeset patch
# User wenzelm
# Date 1124192554 -7200
# Node ID 50210558395102b4a23df62ec268ef51808c1d26
# Parent  7272b45099c7b2fdb8737833ad4d32964c5d355d
tuned Symbol.spaces;

diff -r 7272b45099c7 -r 502105583951 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Aug 16 13:42:33 2005 +0200
+++ b/src/Pure/General/symbol.ML	Tue Aug 16 13:42:34 2005 +0200
@@ -82,7 +82,15 @@
 type symbol = string;
 
 val space = " ";
-fun spaces k = Library.replicate_string k space;
+
+local
+  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i space);
+in
+  fun spaces k =
+    if k < 64 then Vector.sub (small_spaces, k)
+    else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
+      Vector.sub (small_spaces, k mod 64);
+end;
 
 fun is_char s = size s = 1;
 
@@ -170,7 +178,7 @@
 (* decode_raw *)
 
 fun is_raw s =
-  String.isPrefix "\\<^raw" s andalso String.substring (s, size s - 1, 1) = ">";
+  String.isPrefix "\\<^raw" s andalso String.isSuffix ">" s;
 
 fun decode_raw s =
   if not (is_raw s) then error (malformed_symbol s)