tuned signature;

--- a/src/Pure/Admin/build_postgresql.scala	Fri Jan 20 21:52:29 2023 +0100
+++ b/src/Pure/Admin/build_postgresql.scala	Fri Jan 20 21:56:34 2023 +0100
@@ -88,7 +88,7 @@
 
     /* jar */
 
-    val jar = component_dir.path + Path.basic(download_name).ext("jar")
+    val jar = component_dir.path + Path.basic(download_name).jar
     Isabelle_System.download_file(download_url, jar, progress = progress)
   }
 

--- a/src/Pure/Admin/build_sqlite.scala	Fri Jan 20 21:52:29 2023 +0100
+++ b/src/Pure/Admin/build_sqlite.scala	Fri Jan 20 21:56:34 2023 +0100
@@ -50,7 +50,7 @@
 
     /* jar */
 
-    val jar = component_dir.lib + Path.basic(download_name).ext("jar")
+    val jar = component_dir.lib + Path.basic(download_name).jar
     Isabelle_System.make_directory(jar.dir)
     Isabelle_System.download_file(download_url, jar, progress = progress)
 

--- a/src/Pure/General/path.scala	Fri Jan 20 21:52:29 2023 +0100
+++ b/src/Pure/General/path.scala	Fri Jan 20 21:56:34 2023 +0100
@@ -233,8 +233,12 @@
       prfx + Path.basic(s + "." + e)
     }
 
+  def bib: Path = ext("bib")
+  def blg: Path = ext("blg")
+  def db: Path = ext("db")
   def gz: Path = ext("gz")
   def html: Path = ext("html")
+  def jar: Path = ext("jar")
   def log: Path = ext("log")
   def orig: Path = ext("orig")
   def patch: Path = ext("patch")

--- a/src/Pure/Thy/bibtex.scala	Fri Jan 20 21:52:29 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Jan 20 21:56:34 2023 +0100
@@ -52,7 +52,7 @@
   /** bibtex errors **/
 
   def bibtex_errors(dir: Path, root_name: String): List[String] = {
-    val log_path = dir + Path.explode(root_name).ext("blg")
+    val log_path = dir + Path.explode(root_name).blg
     if (log_path.is_file) {
       val Error1 = """^(I couldn't open database file .+)$""".r
       val Error2 = """^(I found no .+)$""".r
@@ -651,7 +651,7 @@
       }
 
       for ((a, b) <- bib_files zip bib_names) {
-        Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
+        Isabelle_System.copy_file(a.bib, tmp_dir + Path.basic(b).bib)
       }
 
 

--- a/src/Pure/Thy/latex.scala	Fri Jan 20 21:52:29 2023 +0100
+++ b/src/Pure/Thy/latex.scala	Fri Jan 20 21:56:34 2023 +0100
@@ -363,7 +363,7 @@
   /* latex log */
 
   def latex_errors(dir: Path, root_name: String): List[String] = {
-    val root_log_path = dir + Path.explode(root_name).ext("log")
+    val root_log_path = dir + Path.explode(root_name).log
     if (root_log_path.is_file) {
       for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
         yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)

--- a/src/Pure/Thy/sessions.scala	Fri Jan 20 21:52:29 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Jan 20 21:56:34 2023 +0100
@@ -1386,9 +1386,9 @@
     /* file names */
 
     def heap(name: String): Path = Path.basic(name)
-    def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db")
+    def database(name: String): Path = Path.basic("log") + Path.basic(name).db
     def log(name: String): Path = Path.basic("log") + Path.basic(name)
-    def log_gz(name: String): Path = log(name).ext("gz")
+    def log_gz(name: String): Path = log(name).gz
 
     def output_heap(name: String): Path = output_dir + heap(name)
     def output_database(name: String): Path = output_dir + database(name)