# HG changeset patch
# User wenzelm
# Date 1606662712 -3600
# Node ID 83e581c9a5f1f8be3c2a468bc65052c6633c36b7
# Parent  164cb0806d0ab2d143da04a1ec1eb1555bcae4d6
tuned signature;

diff -r 164cb0806d0a -r 83e581c9a5f1 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Nov 29 15:58:43 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 29 16:11:52 2020 +0100
@@ -419,10 +419,10 @@
         val imports_pos = header.imports_pos
         val raw_imports =
           try {
-            val read_imports = Thy_Header.read(node_name, reader).imports
+            val read_imports = Thy_Header.read(node_name, reader).imports.map(_._1)
             if (imports_pos.length == read_imports.length) read_imports else error("")
           }
-          catch { case _: Throwable => List.fill(imports_pos.length)("") }
+          catch { case _: Throwable => List.fill(header.imports.length)("") }
 
         val errors =
           for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
diff -r 164cb0806d0a -r 83e581c9a5f1 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Nov 29 15:58:43 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Nov 29 16:11:52 2020 +0100
@@ -220,15 +220,14 @@
     if (node_name.is_theory && reader.source.length > 0) {
       try {
         val header = Thy_Header.read(node_name, reader, command = command, strict = strict)
-
-        val imports_pos =
-          header.imports_pos.map({ case (s, pos) =>
+        val imports =
+          header.imports.map({ case (s, pos) =>
             val name = import_name(node_name, s)
             if (Sessions.exclude_theory(name.theory_base_name))
               error("Bad theory name " + quote(name.theory_base_name) + Position.here(pos))
             (name, pos)
           })
-        Document.Node.Header(imports_pos, header.keywords, header.abbrevs)
+        Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }
diff -r 164cb0806d0a -r 83e581c9a5f1 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:58:43 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 29 16:11:52 2020 +0100
@@ -162,7 +162,7 @@
           { case None => Nil case Some(_ ~ xs) => xs }) ~
         (opt($$$(ABBREVS) ~! abbrevs) ^^
           { case None => Nil case Some(_ ~ xs) => xs }) ~
-        $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a, b, c, d).map(Symbol.decode) }
+        $$$(BEGIN) ^^ { case a ~ b ~ c ~ d ~ _ => Thy_Header(a._1, a._2, b, c, d).map(Symbol.decode) }
 
       val heading =
         (command(CHAPTER) |
@@ -230,18 +230,15 @@
 }
 
 sealed case class Thy_Header(
-  name_pos: (String, Position.T),
-  imports_pos: List[(String, Position.T)],
+  name: String,
+  pos: Position.T,
+  imports: List[(String, Position.T)],
   keywords: Thy_Header.Keywords,
   abbrevs: Thy_Header.Abbrevs)
 {
-  def name: String = name_pos._1
-  def pos: Position.T = name_pos._2
-  def imports: List[String] = imports_pos.map(_._1)
-
   def map(f: String => String): Thy_Header =
-    Thy_Header((f(name), pos),
-      imports_pos.map({ case (a, b) => (f(a), b) }),
+    Thy_Header(f(name), pos,
+      imports.map({ case (a, b) => (f(a), b) }),
       keywords.map({ case (a, spec) => (f(a), spec.map(f)) }),
       abbrevs.map({ case (a, b) => (f(a), f(b)) }))