# HG changeset patch
# User wenzelm
# Date 1606661093 -3600
# Node ID 27a464537fb07146a02e0ae0003aec09b1ab78fc
# Parent  0a94eb91190d2db4b63f4f0d11f47fa329c771b3
tuned signature;

diff -r 0a94eb91190d -r 27a464537fb0 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Sun Nov 29 15:41:36 2020 +0100
+++ b/src/Pure/General/path.scala	Sun Nov 29 15:44:53 2020 +0100
@@ -203,6 +203,7 @@
   def xz: Path = ext("xz")
   def tex: Path = ext("tex")
   def pdf: Path = ext("pdf")
+  def thy: Path = ext("thy")
 
   def backup: Path =
   {
diff -r 0a94eb91190d -r 27a464537fb0 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sun Nov 29 15:41:36 2020 +0100
+++ b/src/Pure/PIDE/resources.scala	Sun Nov 29 15:44:53 2020 +0100
@@ -145,7 +145,7 @@
 
   def find_theory_node(theory: String): Option[Document.Node.Name] =
   {
-    val thy_file = Thy_Header.thy_path(Path.basic(Long_Name.base_name(theory)))
+    val thy_file = Path.basic(Long_Name.base_name(theory)).thy
     val session = session_base.theory_qualifier(theory)
     val dirs =
       sessions_structure.get(session) match {
@@ -159,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_Header.thy_path(Path.explode(s)), theory)
+    def theory_node = make_theory_node(dir, Path.explode(s).thy, theory)
 
     if (!Thy_Header.is_base_name(s)) theory_node
     else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
diff -r 0a94eb91190d -r 27a464537fb0 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:41:36 2020 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Nov 29 15:44:53 2020 +0100
@@ -122,8 +122,6 @@
     for { Thy_File_Name(name) <- files } yield name
   }
 
-  def thy_path(path: Path): Path = path.ext("thy")
-
 
   /* parser */
 
@@ -252,9 +250,8 @@
       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)))
+      error("Bad theory name " + quote(name) + " for file " + Path.basic(base_name).thy +
+        Position.here(pos) + Completion.report_theories(pos, List(base_name)))
     }
 
     for ((_, spec) <- keywords) {