# HG changeset patch
# User wenzelm
# Date 1607287432 -3600
# Node ID a597300290de4337a998d3f67f55f77d99051761
# Parent  27a7a54995112305acba3bde6f9c64d05ef659ee
clarified File_Format.detect: needs to operate on full node name;

diff -r 27a7a5499511 -r a597300290de src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Sun Dec 06 20:49:44 2020 +0100
+++ b/src/Pure/Thy/file_format.scala	Sun Dec 06 21:43:52 2020 +0100
@@ -70,21 +70,22 @@
   def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
   {
     for {
-      (_, ext_name) <- Thy_Header.split_file_name(name.node)
-      if detect(ext_name) && theory_suffix.nonEmpty
+      (_, thy) <- Thy_Header.split_file_name(name.node)
+      if detect(name.node) && theory_suffix.nonEmpty
     }
     yield {
       val thy_node = resources.append(name.node, Path.explode(theory_suffix))
-      Document.Node.Name(thy_node, name.master_dir, ext_name)
+      Document.Node.Name(thy_node, name.master_dir, thy)
     }
   }
 
   def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] =
   {
     for {
-      (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == theory_suffix
-      (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
-      s <- proper_string(theory_content(ext_name))
+      (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node)
+      if detect(prefix) && suffix == theory_suffix
+      (_, thy) <- Thy_Header.split_file_name(prefix)
+      s <- proper_string(theory_content(thy))
     } yield s
   }
 
diff -r 27a7a5499511 -r a597300290de src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Dec 06 20:49:44 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Dec 06 21:43:52 2020 +0100
@@ -44,7 +44,12 @@
   {
     val format_name: String = roots_name
     val file_ext = ""
-    override def detect(name: String): Boolean = name == roots_name
+
+    override def detect(name: String): Boolean =
+      Thy_Header.split_file_name(name) match {
+        case Some((_, file_name)) => file_name == roots_name
+        case None => false
+      }
 
     override def theory_suffix: String = "ROOTS_file"
     override def theory_content(name: String): String =