# HG changeset patch
# User wenzelm
# Date 1278790696 -7200
# Node ID b55f848f34fcfd2211ffcc37fef2d08adaede7ef
# Parent  decac8d1c8e71e1e036b02a897e76332824550a7# Parent  5d2b3e8273718144ca21ab5477e2ec94887f55b7
merged

diff -r decac8d1c8e7 -r b55f848f34fc src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Jul 09 16:44:05 2010 +0100
+++ b/src/Pure/General/symbol.ML	Sat Jul 10 21:38:16 2010 +0200
@@ -432,6 +432,10 @@
 
 fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192;
 
+fun implode_pseudo_utf8 (cs as ["\192", c]) =
+      if ord c < 160 then chr (ord c - 128) else implode cs
+  | implode_pseudo_utf8 cs = implode cs;
+
 val scan_encoded_newline =
   $$ "\^M" -- $$ "\n" >> K "\n" ||
   $$ "\^M" >> K "\n" ||
@@ -443,7 +447,7 @@
 
 val scan =
   Scan.one is_plain ||
-  Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode ||
+  Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 ||
   scan_encoded_newline ||
   ($$ "\\" ^^ $$ "<" ^^
     !! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))