# HG changeset patch
# User wenzelm
# Date 1606660896 -3600
# Node ID 0a94eb91190d2db4b63f4f0d11f47fa329c771b3
# Parent  51c0f79d6eed8e365ff1b789eae007a31c41c66b
clarified modules;

diff -r 51c0f79d6eed -r 0a94eb91190d src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Nov 29 15:33:19 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 29 15:41:36 2020 +0100
@@ -419,7 +419,7 @@
         val imports_pos = header.imports_pos
         val raw_imports =
           try {
-            val read_imports = Thy_Header.read(reader).imports
+            val read_imports = Thy_Header.read(node_name, reader).imports
             if (imports_pos.length == read_imports.length) read_imports else error("")
           }
           catch { case _: Throwable => List.fill(imports_pos.length)("") }
diff -r 51c0f79d6eed -r 0a94eb91190d src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Nov 29 15:33:19 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Nov 29 15:41:36 2020 +0100
@@ -60,8 +60,6 @@
   def is_hidden(name: Document.Node.Name): Boolean =
     !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
 
-  def thy_path(path: Path): Path = path.ext("thy")
-
 
   /* file-system operations */
 
@@ -147,7 +145,7 @@
 
   def find_theory_node(theory: String): Option[Document.Node.Name] =
   {
-    val thy_file = thy_path(Path.basic(Long_Name.base_name(theory)))
+    val thy_file = Thy_Header.thy_path(Path.basic(Long_Name.base_name(theory)))
     val session = session_base.theory_qualifier(theory)
     val dirs =
       sessions_structure.get(session) match {
@@ -161,7 +159,7 @@
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
-    def theory_node = make_theory_node(dir, thy_path(Path.explode(s)), theory)
+    def theory_node = make_theory_node(dir, Thy_Header.thy_path(Path.explode(s)), theory)
 
     if (!Thy_Header.is_base_name(s)) theory_node
     else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
@@ -221,18 +219,7 @@
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
-        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)) {
-          error("Bad theory name " + quote(header.name) + " with qualification" +
-            Position.here(header.pos))
-        }
-        if (base_name != header.name) {
-          error("Bad theory name " + quote(header.name) +
-            " for file " + thy_path(Path.basic(base_name)) + Position.here(header.pos) +
-            Completion.report_theories(header.pos, List(base_name)))
-        }
+        val header = Thy_Header.read(node_name, reader, start = start, strict = strict)
 
         val imports_pos =
           header.imports_pos.map({ case (s, pos) =>
diff -r 51c0f79d6eed -r 0a94eb91190d src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:33:19 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:41:36 2020 +0100
@@ -122,6 +122,8 @@
     for { Thy_File_Name(name) <- files } yield name
   }
 
+  def thy_path(path: Path): Path = path.ext("thy")
+
 
   /* parser */
 
@@ -213,7 +215,7 @@
       }
   }
 
-  def read(reader: Reader[Char],
+  def read(node_name: Document.Node.Name, reader: Reader[Char],
     start: Token.Pos = Token.Pos.none,
     strict: Boolean = true): Thy_Header =
   {
@@ -223,7 +225,7 @@
     val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
     val pos = (start /: drop_tokens)(_.advance(_))
 
-    Parser.parse_header(tokens, pos).check_keywords
+    Parser.parse_header(tokens, pos).check(node_name)
   }
 }
 
@@ -243,8 +245,18 @@
       keywords.map({ case (a, spec) => (f(a), spec.map(f)) }),
       abbrevs.map({ case (a, b) => (f(a), f(b)) }))
 
-  def check_keywords: Thy_Header =
+  def check(node_name: Document.Node.Name): Thy_Header =
   {
+    val base_name = node_name.theory_base_name
+    if (Long_Name.is_qualified(name)) {
+      error("Bad theory name " + quote(name) + " with qualification" + Position.here(pos))
+    }
+    if (base_name != name) {
+      error("Bad theory name " + quote(name) + " for file " +
+        Thy_Header.thy_path(Path.basic(base_name)) + Position.here(pos) +
+        Completion.report_theories(pos, List(base_name)))
+    }
+
     for ((_, spec) <- keywords) {
       if (spec.kind != Keyword.THY_LOAD && spec.load_command.nonEmpty) {
         error("Illegal load command specification for kind: " + quote(spec.kind) +