src/Pure/PIDE/command.scala
changeset 64825 e78b62c289bb
parent 64824 330ec9bc4b75
child 65335 7634d33c1a79
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Jan 07 20:01:05 2017 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Jan 07 20:37:48 2017 +0100
     1.3 @@ -349,8 +349,8 @@
     1.4      span.name match {
     1.5        // inlined errors
     1.6        case Thy_Header.THEORY =>
     1.7 -        val header =
     1.8 -          resources.check_thy_reader("", node_name, Scan.char_reader(Token.implode(span.content)))
     1.9 +        val reader = Scan.char_reader(Token.implode(span.content))
    1.10 +        val header = resources.check_thy_reader("", node_name, reader)
    1.11          val errors =
    1.12            for ((imp, pos) <- header.imports if !can_import(imp)) yield {
    1.13              val msg =