--- a/src/Pure/PIDE/command.scala Sat Jan 07 20:01:05 2017 +0100
+++ b/src/Pure/PIDE/command.scala Sat Jan 07 20:37:48 2017 +0100
@@ -349,8 +349,8 @@
span.name match {
// inlined errors
case Thy_Header.THEORY =>
- val header =
- resources.check_thy_reader("", node_name, Scan.char_reader(Token.implode(span.content)))
+ val reader = Scan.char_reader(Token.implode(span.content))
+ val header = resources.check_thy_reader("", node_name, reader)
val errors =
for ((imp, pos) <- header.imports if !can_import(imp)) yield {
val msg =