# HG changeset patch
# User wenzelm
# Date 1660920360 -7200
# Node ID 2167b9e3157a826b82a277ddba8fe926a00b7d8d
# Parent  2ee3ea69e8f113cd6ea4484d44b89ee35be9d773
clarified signature: support for adhoc file types;

diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -17,7 +17,7 @@
     (for {
       file <-
         File.find_files(Path.explode("~~/src/HOL/Tools/Mirabelle").file,
-          pred = _.getName.endsWith(".ML"))
+          pred = file => File.is_ML(file.getName))
       line <- split_lines(File.read(file))
       name <- line match { case Pattern(a) => Some(a) case _ => None }
     } yield name).sorted
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Admin/build_jcef.scala
--- a/src/Pure/Admin/build_jcef.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Admin/build_jcef.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -71,11 +71,11 @@
           for {
             file <- File.find_files(platform_dir.file).iterator
             name = file.getName
-            if name.endsWith(".dll") || name.endsWith(".exe")
+            if File.is_dll(name) || File.is_exe(name)
           } File.set_executable(File.path(file), true)
 
           val classpath =
-            File.find_files(platform_dir.file, pred = (file => file.getName.endsWith(".jar")))
+            File.find_files(platform_dir.file, pred = file => File.is_jar(file.getName))
               .flatMap(file => File.relative_path(platform_dir, File.path(file)))
               .map(jar => "        " + quote("$ISABELLE_JCEF_HOME/" + jar.implode))
               .mkString(" \\\n")
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Admin/build_jedit.scala
--- a/src/Pure/Admin/build_jedit.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Admin/build_jedit.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -161,7 +161,7 @@
       for {
         file <- File.find_files(Path.explode("~~/src/Tools/jEdit/patches").file).iterator
         name = file.getName
-        if !name.endsWith("~") && !name.endsWith(".orig")
+        if !File.is_backup(name)
       } {
         progress.bash("patch -p2 < " + File.bash_path(File.path(file)),
           cwd = source_dir.file, echo = true).check
@@ -181,7 +181,7 @@
 
       val java_sources =
         for {
-          file <- File.find_files(org_source_dir.file, file => file.getName.endsWith(".java"))
+          file <- File.find_files(org_source_dir.file, file => File.is_java(file.getName))
           package_name <- Scala_Project.package_name(File.path(file))
           if !exclude_package(package_name)
         } yield File.path(component_dir.java_path.relativize(file.toPath).toFile).implode
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -108,8 +108,8 @@
     def apply(file: JFile): Log_File = {
       val name = file.getName
       val text =
-        if (name.endsWith(".gz")) File.read_gzip(file)
-        else if (name.endsWith(".xz")) File.read_xz(file)
+        if (File.is_gz(name)) File.read_gzip(file)
+        else if (File.is_xz(name)) File.read_xz(file)
         else File.read(file)
       apply(name, text)
     }
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Admin/check_sources.scala
--- a/src/Pure/Admin/check_sources.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Admin/check_sources.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -50,7 +50,7 @@
     val hg = Mercurial.repository(root)
     for {
       file <- hg.known_files()
-      if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
+      if File.is_thy(file) || File.is_ML(file) || file.endsWith("/ROOT")
     } check_file(root + Path.explode(file))
   }
 
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/General/file.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -69,6 +69,26 @@
   def url(path: Path): URL = url(path.file)
 
 
+  /* adhoc file types */
+
+  def is_ML(s: String): Boolean = s.endsWith(".ML")
+  def is_bib(s: String): Boolean = s.endsWith(".bib")
+  def is_dll(s: String): Boolean = s.endsWith(".dll")
+  def is_exe(s: String): Boolean = s.endsWith(".exe")
+  def is_gz(s: String): Boolean = s.endsWith(".gz")
+  def is_html(s: String): Boolean = s.endsWith(".html")
+  def is_jar(s: String): Boolean = s.endsWith(".jar")
+  def is_java(s: String): Boolean = s.endsWith(".java")
+  def is_node(s: String): Boolean = s.endsWith(".node")
+  def is_pdf(s: String): Boolean = s.endsWith(".pdf")
+  def is_png(s: String): Boolean = s.endsWith(".png")
+  def is_thy(s: String): Boolean = s.endsWith(".thy")
+  def is_xz(s: String): Boolean = s.endsWith(".xz")
+  def is_zip(s: String): Boolean = s.endsWith(".zip")
+
+  def is_backup(s: String): Boolean = s.endsWith("~") || s.endsWith(".orig")
+
+
   /* relative paths */
 
   def relative_path(base: Path, other: Path): Option[Path] = {
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/General/mailman.scala
--- a/src/Pure/General/mailman.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/General/mailman.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -420,7 +420,7 @@
 
     def find_messages(dir: Path): List[Message] = {
       for {
-        file <- File.find_files(dir.file, file => file.getName.endsWith(".html"))
+        file <- File.find_files(dir.file, file => File.is_html(file.getName))
         rel_path <- File.relative_path(dir, File.path(file))
       }
       yield {
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/System/classpath.scala
--- a/src/Pure/System/classpath.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/System/classpath.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -29,7 +29,7 @@
       } yield File.absolute(new JFile(s))
 
     val jar_files1 =
-      jar_files.flatMap(start => File.find_files(start, _.getName.endsWith(".jar")))
+      jar_files.flatMap(start => File.find_files(start, file => File.is_jar(file.getName)))
         .map(File.absolute)
 
     val tmp_jars =
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -14,10 +14,7 @@
 
   private def is_external(dir: Path, name: String): Boolean = {
     val file = (dir + Path.explode(name)).file
-    try {
-      file.isFile && file.canRead && file.canExecute &&
-        !name.endsWith("~") && !name.endsWith(".orig")
-    }
+    try { file.isFile && file.canRead && file.canExecute && !File.is_backup(name) }
     catch { case _: SecurityException => false }
   }
 
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Thy/bibtex.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -17,8 +17,6 @@
 object Bibtex {
   /** file format **/
 
-  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
-
   class File_Format extends isabelle.File_Format {
     val format_name: String = "bibtex"
     val file_ext: String = "bib"
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -48,7 +48,7 @@
       Path.explode("files") + Path.explode(file).squash.html
 
     def smart_html(theory: Nodes.Theory, file: String): Path =
-      if (file.endsWith(".thy")) theory_html(theory) else file_html(file)
+      if (File.is_thy(file)) theory_html(theory) else file_html(file)
 
     def files_path(session: String, path: Path): Path =
       session_dir(session) + Path.explode("files") + path.squash.html
@@ -151,8 +151,8 @@
           case Nil => error("Unknown theory file for " + quote(name))
           case a :: bs =>
             def for_theory: String = " for theory " + quote(name)
-            if (!a.endsWith(".thy")) error("Bad .thy file " + quote(a) + for_theory)
-            for (b <- bs if b.endsWith(".thy")) error("Bad auxiliary file " + quote(b) + for_theory)
+            if (!File.is_thy(a)) error("Bad .thy file " + quote(a) + for_theory)
+            for (b <- bs if File.is_thy(b)) error("Bad auxiliary file " + quote(b) + for_theory)
             (a, bs)
         }
 
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -537,7 +537,7 @@
     lazy val bibtex_entries: List[Text.Info[String]] =
       (for {
         (document_dir, file) <- document_files.iterator
-        if Bibtex.is_bibtex(file.file_name)
+        if File.is_bib(file.file_name)
         info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator
       } yield info).toList
 
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -91,7 +91,7 @@
 
   def import_name(s: String): String =
     s match {
-      case File_Name(name) if !name.endsWith(".thy") => name
+      case File_Name(name) if !File.is_thy(name) => name
       case _ => error("Malformed theory import: " + quote(s))
     }
 
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Tools/update_cartouches.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -97,7 +97,7 @@
         for {
           spec <- specs
           file <- File.find_files(Path.explode(spec).file,
-            file => file.getName.endsWith(".thy") || file.getName == "ROOT")
+            file => File.is_thy(file.getName) || file.getName == "ROOT")
         } update_cartouches(replace_text, File.path(file))
       })
 }
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Tools/update_comments.scala
--- a/src/Pure/Tools/update_comments.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Tools/update_comments.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -60,7 +60,7 @@
 
         for {
           spec <- specs
-          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+          file <- File.find_files(Path.explode(spec).file, file => File.is_thy(file.getName))
         } update_comments(File.path(file))
       })
 }
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Tools/update_header.scala
--- a/src/Pure/Tools/update_header.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Tools/update_header.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -54,7 +54,7 @@
 
         for {
           spec <- specs
-          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+          file <- File.find_files(Path.explode(spec).file, file => File.is_thy(file.getName))
         } update_header(section, File.path(file))
       })
 }
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Tools/update_then.scala
--- a/src/Pure/Tools/update_then.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Tools/update_then.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -48,7 +48,7 @@
   
         for {
           spec <- specs
-          file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+          file <- File.find_files(Path.explode(spec).file, file => File.is_thy(file.getName))
         } update_then(File.path(file))
       })
 }
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Pure/Tools/update_theorems.scala
--- a/src/Pure/Tools/update_theorems.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Pure/Tools/update_theorems.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -50,7 +50,7 @@
 
       for {
         spec <- specs
-        file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
+        file <- File.find_files(Path.explode(spec).file, file => File.is_thy(file.getName))
       } update_theorems(File.path(file))
     })
 }
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Tools/Graphview/graph_file.scala
--- a/src/Tools/Graphview/graph_file.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Tools/Graphview/graph_file.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -27,8 +27,8 @@
     }
 
     val name = file.getName
-    if (name.endsWith(".png")) Graphics_File.write_png(file, paint, w, h)
-    else if (name.endsWith(".pdf")) Graphics_File.write_pdf(file, paint, w, h)
+    if (File.is_png(name)) Graphics_File.write_png(file, paint, w, h)
+    else if (File.is_pdf(name)) Graphics_File.write_pdf(file, paint, w, h)
     else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
   }
 
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -66,7 +66,7 @@
     def is_linux: Boolean = platform == Platform.Family.linux
 
     def download_name: String = "VSCodium-" + download_template.replace("{VERSION}", version)
-    def download_zip: Boolean = download_name.endsWith(".zip")
+    def download_zip: Boolean = File.is_zip(download_name)
 
     def download(dir: Path, progress: Progress = new Progress): Unit = {
       if (download_zip) Isabelle_System.require_command("unzip", test = "-h")
@@ -222,7 +222,7 @@
         val files =
           File.find_files(dir.file, pred = { file =>
             val name = file.getName
-            name.endsWith(".dll") || name.endsWith(".exe") || name.endsWith(".node")
+            File.is_dll(name) || File.is_exe(name) || File.is_node(name)
           })
         files.foreach(file => File.set_executable(File.path(file), true))
         Isabelle_System.bash("chmod -R o-w " + File.bash_path(dir)).check
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -89,7 +89,7 @@
   def completion(node_pos: Line.Node_Position, caret: Text.Offset): List[LSP.CompletionItem] = {
     val doc = model.content.doc
     val line = node_pos.pos.line
-    val unicode = node_pos.name.endsWith(".thy")
+    val unicode = File.is_thy(node_pos.name)
     doc.offset(Line.Position(line)) match {
       case None => Nil
       case Some(line_start) =>
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -420,7 +420,7 @@
     else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
   def bibtex_entries: List[Text.Info[String]] =
-    if (Bibtex.is_bibtex(node_name.node)) content.bibtex_entries else Nil
+    if (File.is_bib(node_name.node)) content.bibtex_entries else Nil
 
 
   /* edits */
@@ -542,7 +542,7 @@
 
   def bibtex_entries: List[Text.Info[String]] =
     GUI_Thread.require {
-      if (Bibtex.is_bibtex(node_name.node)) {
+      if (File.is_bib(node_name.node)) {
         _bibtex_entries match {
           case Some(entries) => entries
           case None =>
diff -r 2ee3ea69e8f1 -r 2167b9e3157a src/Tools/jEdit/src/jedit_bibtex.scala
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Fri Aug 19 16:19:59 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Fri Aug 19 16:46:00 2022 +0200
@@ -29,7 +29,7 @@
   def context_menu(text_area: JEditTextArea): List[JMenuItem] = {
     text_area.getBuffer match {
       case buffer: Buffer
-      if Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable =>
+      if File.is_bib(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable =>
         val menu = new JMenu("BibTeX entries")
         for (entry <- Bibtex.known_entries) {
           val item = new JMenuItem(entry.kind)