# HG changeset patch
# User wenzelm
# Date 1087475203 -7200
# Node ID 8092a0319927d689e01d0828f2895f9c8dc26765
# Parent  89cce4e95a22d9a4fe8daecfb06705b62a6c4581
isub/isup quasi letter (again); tuned;

diff -r 89cce4e95a22 -r 8092a0319927 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Jun 17 14:26:24 2004 +0200
+++ b/src/Pure/General/symbol.ML	Thu Jun 17 14:26:43 2004 +0200
@@ -336,8 +336,8 @@
     ("\\<Phi>", Letter),
     ("\\<Psi>", Letter),
     ("\\<Omega>", Letter),
-    ("\\<^isub>", Quasi),
-    ("\\<^isup>", Quasi),
+    ("\\<^isub>", Letter),
+    ("\\<^isup>", Letter),
     ("\\<spacespace>", Blank)];
 in
   fun kind s =
@@ -365,12 +365,13 @@
 
 fun scanner msg scan chs =
   let
-    fun err_msg cs = msg ^ ": " ^ beginning 10 cs;
-    val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan));
+    fun message (cs, None) = msg ^ ": " ^ quote (beginning 10 cs)
+      | message (cs, Some msg') = msg ^ ", " ^ msg' ^ ": " ^ quote (beginning 10 cs);
+    val fin_scan = Scan.error (Scan.finite stopper (!! message scan));
   in
     (case fin_scan chs of
       (result, []) => result
-    | (_, rest) => error (err_msg rest))
+    | (_, rest) => error (message (rest, None)))
   end;
 
 
@@ -394,7 +395,7 @@
 val scan =
   scan_encoded_newline ||
   (($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
-    !! (fn (cs, _) => malformed_symbol (beginning 10 ("\\" :: "<" :: cs)))
+    !! (fn (cs, _) => malformed_symbol (quote (beginning 10 ("\\" :: "<" :: cs))))
       (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
   Scan.one not_eof;