# HG changeset patch
# User wenzelm
# Date 1308604884 -7200
# Node ID 33a24212a72d870fa7b3243987cc0beaa322917e
# Parent  51b8043a8cf5ee8c3b91c7b3554c61f2fc04fd49
more tolerant Symbol.decode;

diff -r 51b8043a8cf5 -r 33a24212a72d src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Jun 20 23:19:38 2011 +0200
+++ b/src/Pure/General/symbol.ML	Mon Jun 20 23:21:24 2011 +0200
@@ -43,7 +43,7 @@
   val encode_raw: string -> string
   datatype sym =
     Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string |
-    Malformed of string
+    Malformed of string | EOF
   val decode: symbol -> sym
   datatype kind = Letter | Digit | Quasi | Blank | Other
   val kind: symbol -> kind
@@ -222,10 +222,11 @@
 
 datatype sym =
   Char of string | UTF8 of string | Sym of string | Ctrl of string | Raw of string |
-  Malformed of string;
+  Malformed of string | EOF;
 
 fun decode s =
-  if is_char s then Char s
+  if s = "" then EOF
+  else if is_char s then Char s
   else if is_utf8 s then UTF8 s
   else if is_raw s then Raw (decode_raw s)
   else if is_malformed s then Malformed s
diff -r 51b8043a8cf5 -r 33a24212a72d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Jun 20 23:19:38 2011 +0200
+++ b/src/Pure/Thy/latex.ML	Mon Jun 20 23:21:24 2011 +0200
@@ -102,7 +102,8 @@
       if known_ctrl s then literal sym ^ "{}" ^ enclose "\\isactrl" " " s
       else output_chrs sym
   | Symbol.Raw s => s
-  | Symbol.Malformed s => error (Symbol.malformed_msg s));
+  | Symbol.Malformed s => error (Symbol.malformed_msg s)
+  | Symbol.EOF => error "Bad EOF symbol");
 
 in
 
diff -r 51b8043a8cf5 -r 33a24212a72d src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Mon Jun 20 23:19:38 2011 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Mon Jun 20 23:21:24 2011 +0200
@@ -88,11 +88,10 @@
   >> token Comment;
 
 fun is_sym s =
-  Symbol.not_eof s andalso
-    (case Symbol.decode s of
-      Symbol.Sym _ => true
-    | Symbol.Ctrl _ => true
-    | _ => false);
+  (case Symbol.decode s of
+    Symbol.Sym _ => true
+  | Symbol.Ctrl _ => true
+  | _ => false);
 
 fun tokenize syms =
   let