# HG changeset patch
# User wenzelm
# Date 1459879505 -7200
# Node ID 741560a5283b9968e9f3d83ba54dea37a9aa4b0f
# Parent  507c90523113bff25a6a7d30d89e8e0b498e82f4
avoid malformed Isabelle symbols during bootstrap;

diff -r 507c90523113 -r 741560a5283b src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Apr 05 20:03:24 2016 +0200
+++ b/src/Pure/General/symbol.ML	Tue Apr 05 20:05:05 2016 +0200
@@ -119,7 +119,7 @@
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
 
 fun raw_symbolic s =
-  String.isPrefix "\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\<^" s);
+  String.isPrefix "\092<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\092<^" s);
 
 fun is_symbolic s =
   s <> open_ andalso s <> close andalso raw_symbolic s;
@@ -131,7 +131,7 @@
   else is_utf8 s orelse raw_symbolic s;
 
 fun is_control s =
-  String.isPrefix "\<^" s andalso String.isSuffix ">" s;
+  String.isPrefix "\092<^" s andalso String.isSuffix ">" s;
 
 
 (* input source control *)
@@ -142,8 +142,8 @@
 val stopper = Scan.stopper (K eof) is_eof;
 
 fun is_malformed s =
-  String.isPrefix "\<" s andalso not (String.isSuffix ">" s)
-  orelse s = "\<>" orelse s = "\<^>";
+  String.isPrefix "\092<" s andalso not (String.isSuffix ">" s)
+  orelse s = "\092<>" orelse s = "\092<^>";
 
 fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
 
@@ -201,9 +201,9 @@
 fun encode_raw "" = ""
   | encode_raw str =
       let
-        val raw0 = enclose "\<^raw:" ">";
+        val raw0 = enclose "\092<^raw:" ">";
         val raw1 = raw0 o implode;
-        val raw2 = enclose "\<^raw" ">" o string_of_int o ord;
+        val raw2 = enclose "\092<^raw" ">" o string_of_int o ord;
 
         fun encode cs = enc (take_prefix raw_chr cs)
         and enc ([], []) = []
@@ -233,11 +233,11 @@
 (* decode_raw *)
 
 fun is_raw s =
-  String.isPrefix "\<^raw" s andalso String.isSuffix ">" s;
+  String.isPrefix "\092<^raw" s andalso String.isSuffix ">" s;
 
 fun decode_raw s =
   if not (is_raw s) then error (malformed_msg s)
-  else if String.isPrefix "\<^raw:" s then String.substring (s, 7, size s - 8)
+  else if String.isPrefix "\092<^raw:" s then String.substring (s, 7, size s - 8)
   else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
 
 
@@ -563,8 +563,8 @@
 
 fun sym_len s =
   if not (is_printable s) then (0: int)
-  else if String.isPrefix "\<long" s then 2
-  else if String.isPrefix "\<Long" s then 2
+  else if String.isPrefix "\092<long" s then 2
+  else if String.isPrefix "\092<Long" s then 2
   else 1;
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
diff -r 507c90523113 -r 741560a5283b src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/ML/ml_compiler0.ML	Tue Apr 05 20:03:24 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Tue Apr 05 20:05:05 2016 +0200
@@ -69,7 +69,7 @@
       | input line (#"@" :: #"{" :: #"m" :: #"a" :: #"k" :: #"e" :: #"_" ::
             #"s" :: #"t" :: #"r" :: #"i" :: #"n" :: #"g" :: #"}" :: cs) res =
           input line cs (ML_Pretty.make_string_fn "" :: res)
-      | input line (#"\\" :: #"<" :: cs) res = input line cs ("\\\\<" :: res)
+      | input line (#"\\" :: #"<" :: cs) res = input line cs ("\092\092<" :: res)
       | input line (#"\n" :: cs) res = input (line + 1) cs ("\n" :: res)
       | input line (c :: cs) res = input line cs (str c :: res)
       | input _ [] res = rev res;