# HG changeset patch
# User wenzelm
# Date 1344712236 -7200
# Node ID c4bd5bb3ae69a56f10d5a8dbe0234a2541cbb455
# Parent  0e1bab274672e440ad78e23db46bb39f2027615c
further clarification of malformed symbols;

diff -r 0e1bab274672 -r c4bd5bb3ae69 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sat Aug 11 20:54:06 2012 +0200
+++ b/src/Pure/General/symbol.ML	Sat Aug 11 21:10:36 2012 +0200
@@ -115,7 +115,10 @@
 
 fun is_regular s = not_eof s andalso s <> sync;
 
-fun is_malformed s = String.isPrefix "\\<" s andalso not (String.isSuffix ">" s);
+fun is_malformed s =
+  String.isPrefix "\\<" s andalso not (String.isSuffix ">" s)
+  orelse s = "\\<>" orelse s = "\\<^>";
+
 fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
 
 
@@ -436,9 +439,8 @@
   Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
   scan_encoded_newline ||
   ($$ "\\" ^^ $$ "<" ^^
-    (($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ Scan.optional ($$ ">") "")) ||
-  Scan.this_string "\\<^" ||
-  Scan.this_string "\\<" ||
+    (($$ "^" ^^ Scan.optional (scan_raw || scan_id) "" || Scan.optional scan_id "") ^^
+      Scan.optional ($$ ">") "")) ||
   Scan.one not_eof;
 
 in
diff -r 0e1bab274672 -r c4bd5bb3ae69 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sat Aug 11 20:54:06 2012 +0200
+++ b/src/Pure/General/symbol.scala	Sat Aug 11 21:10:36 2012 +0200
@@ -56,7 +56,7 @@
         val c1 = s(0)
         val c2 = s(1)
         !(c1 == '\r' && c2 == '\n' || Character.isSurrogatePair(c1, c2))
-      case _ => !s.endsWith(">")
+      case _ => !s.endsWith(">") || s == "\\<>" || s == "\\<^>"
     }
 
   def is_physical_newline(s: Symbol): Boolean =