# HG changeset patch
# User wenzelm
# Date 1354268574 -3600
# Node ID 674893679352eb29b687437fb42e5800482883f0
# Parent  735bea8d89c9d738659711b7eb0ba128047eb5c9
prefer Symbol.decode_strict in batch mode, to avoid files with spurious Unicode symbols that clash with Isabelle symbol interpretation;

diff -r 735bea8d89c9 -r 674893679352 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Nov 29 23:12:50 2012 +0100
+++ b/src/Pure/General/symbol.scala	Fri Nov 30 10:42:54 2012 +0100
@@ -380,6 +380,18 @@
   def decode(text: String): String = symbols.decode(text)
   def encode(text: String): String = symbols.encode(text)
 
+  def decode_strict(text: String): String =
+  {
+    val decoded = decode(text)
+    if (encode(decoded) == text) decoded
+    else {
+      val bad = new mutable.ListBuffer[Symbol]
+      for (s <- iterator(text) if encode(decode(s)) != s && !bad.contains(s))
+        bad += s
+      error("Bad Unicode symbols in text: " + commas_quote(bad))
+    }
+  }
+
   def fonts: Map[Symbol, String] = symbols.fonts
   def font_names: List[String] = symbols.font_names
   def font_index: Map[String, Int] = symbols.font_index
diff -r 735bea8d89c9 -r 674893679352 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Thu Nov 29 23:12:50 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Fri Nov 30 10:42:54 2012 +0100
@@ -47,7 +47,10 @@
   {
     val path = Path.explode(name.node)
     if (!path.is_file) error("No such file: " + path.toString)
-    f(File.read(path))
+
+    val text = File.read(path)
+    Symbol.decode_strict(text)
+    f(text)
   }