equal
deleted
inserted
replaced
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 = |