--- a/src/Pure/PIDE/command.scala Sat Jan 07 17:32:11 2017 +0100
+++ b/src/Pure/PIDE/command.scala Sat Jan 07 19:36:40 2017 +0100
@@ -351,8 +351,8 @@
// inlined errors
case Thy_Header.THEORY =>
val header =
- resources.check_thy_reader("", node_name,
- new CharSequenceReader(Token.implode(span.content)), Token.Pos.command)
+ resources.check_thy_reader(
+ "", node_name, new CharSequenceReader(Token.implode(span.content)))
val errors =
for ((imp, pos) <- header.imports if !can_import(imp)) yield {
val msg =