--- a/src/Pure/General/symbol.scala Wed Oct 25 14:39:22 2017 +0200
+++ b/src/Pure/General/symbol.scala Wed Oct 25 14:54:28 2017 +0200
@@ -60,6 +60,8 @@
else char_symbols(c.toInt)
}
+ def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
+
/* symbol matching */
--- a/src/Pure/Isar/keyword.scala Wed Oct 25 14:39:22 2017 +0200
+++ b/src/Pure/Isar/keyword.scala Wed Oct 25 14:54:28 2017 +0200
@@ -166,7 +166,11 @@
(minor + name, major)
else (minor, major + name)
val load_commands1 =
- if (kind == THY_LOAD) load_commands + (name -> exts)
+ if (kind == THY_LOAD) {
+ if (!Symbol.iterator(name).forall(Symbol.is_ascii(_)))
+ error("Bad theory load command " + quote(name))
+ load_commands + (name -> exts)
+ }
else load_commands
new Keywords(minor1, major1, kinds1, load_commands1)
}