# HG changeset patch # User wenzelm # Date 1606660399 -3600 # Node ID 51c0f79d6eed8e365ff1b789eae007a31c41c66b # Parent 93b50b9e3494589625952e0812f262ac8884ad93 tuned signature; diff -r 93b50b9e3494 -r 51c0f79d6eed src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sun Nov 29 15:23:18 2020 +0100 +++ b/src/Pure/PIDE/command.scala Sun Nov 29 15:33:19 2020 +0100 @@ -419,7 +419,7 @@ val imports_pos = header.imports_pos val raw_imports = try { - val read_imports = Thy_Header.read(reader, Token.Pos.none).imports + val read_imports = Thy_Header.read(reader).imports if (imports_pos.length == read_imports.length) read_imports else error("") } catch { case _: Throwable => List.fill(imports_pos.length)("") } diff -r 93b50b9e3494 -r 51c0f79d6eed src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sun Nov 29 15:23:18 2020 +0100 +++ b/src/Pure/PIDE/resources.scala Sun Nov 29 15:33:19 2020 +0100 @@ -221,7 +221,7 @@ { if (node_name.is_theory && reader.source.length > 0) { try { - val header = Thy_Header.read(reader, start, strict) + val header = Thy_Header.read(reader, start = start, strict = strict) val base_name = node_name.theory_base_name if (Long_Name.is_qualified(header.name)) { diff -r 93b50b9e3494 -r 51c0f79d6eed src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sun Nov 29 15:23:18 2020 +0100 +++ b/src/Pure/Thy/thy_header.scala Sun Nov 29 15:33:19 2020 +0100 @@ -213,7 +213,9 @@ } } - def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header = + def read(reader: Reader[Char], + start: Token.Pos = Token.Pos.none, + strict: Boolean = true): Thy_Header = { val (_, tokens0) = read_tokens(reader, true) val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))