src/Tools/jEdit/src-base/isabelle_encoding.scala

--- a/src/Tools/jEdit/src-base/isabelle_encoding.scala	Sat Dec 30 14:15:44 2017 +0100
+++ b/src/Tools/jEdit/src-base/isabelle_encoding.scala	Sat Dec 30 20:04:05 2017 +0100
@@ -11,7 +11,7 @@
 
 import org.gjt.sp.jedit.io.Encoding
 
-import java.nio.charset.{Charset, CodingErrorAction}
+import java.nio.charset.{Charset, CodingErrorAction, CharacterCodingException}
 import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
   CharArrayReader, ByteArrayOutputStream}
 
@@ -22,20 +22,25 @@
 {
   private val BUFSIZE = 32768
 
-  private def text_reader(in: InputStream, codec: Codec): Reader =
+  private def text_reader(in: InputStream, codec: Codec, strict: Boolean): Reader =
   {
-    val source = new BufferedSource(in)(codec)
-    new CharArrayReader(Symbol.decode(source.mkString).toArray)
+    val source = (new BufferedSource(in)(codec)).mkString
+
+    if (strict && Codepoint.iterator(source).exists(Symbol.is_code))
+      throw new CharacterCodingException()
+
+    new CharArrayReader(Symbol.decode(source).toArray)
   }
 
-  override def getTextReader(in: InputStream): Reader = text_reader(in, UTF8.codec())
+  override def getTextReader(in: InputStream): Reader =
+    text_reader(in, UTF8.codec(), true)
 
   override def getPermissiveTextReader(in: InputStream): Reader =
   {
     val codec = UTF8.codec()
     codec.onMalformedInput(CodingErrorAction.REPLACE)
     codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
-    text_reader(in, codec)
+    text_reader(in, codec, false)
   }
 
   override def getTextWriter(out: OutputStream): Writer =