src/Pure/PIDE/command.scala
changeset 72774 51c0f79d6eed
parent 72772 a9ef39041114
child 72775 0a94eb91190d
equal deleted inserted replaced
72773:93b50b9e3494 72774:51c0f79d6eed
   417         val reader = Scan.char_reader(Token.implode(span.content))
   417         val reader = Scan.char_reader(Token.implode(span.content))
   418         val header = resources.check_thy(node_name, reader)
   418         val header = resources.check_thy(node_name, reader)
   419         val imports_pos = header.imports_pos
   419         val imports_pos = header.imports_pos
   420         val raw_imports =
   420         val raw_imports =
   421           try {
   421           try {
   422             val read_imports = Thy_Header.read(reader, Token.Pos.none).imports
   422             val read_imports = Thy_Header.read(reader).imports
   423             if (imports_pos.length == read_imports.length) read_imports else error("")
   423             if (imports_pos.length == read_imports.length) read_imports else error("")
   424           }
   424           }
   425           catch { case _: Throwable => List.fill(imports_pos.length)("") }
   425           catch { case _: Throwable => List.fill(imports_pos.length)("") }
   426 
   426 
   427         val errors =
   427         val errors =