# 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))