# HG changeset patch
# User wenzelm
# Date 1543418320 -3600
# Node ID 34b7550b66c79b8202cd47cc859bb4a8edb7a097
# Parent  b6dacf6eabe3ba4ea84d5848a4f672dcbd5e789f
tuned signature;

diff -r b6dacf6eabe3 -r 34b7550b66c7 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Wed Nov 28 16:14:31 2018 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Wed Nov 28 16:18:40 2018 +0100
@@ -97,7 +97,7 @@
       val tmp_dir = dir + Path.explode("tmp")
       Isabelle_System.mkdirs(tmp_dir)
 
-      if (archive.split_ext._2 == "zip") {
+      if (archive.get_ext == "zip") {
         Isabelle_System.bash(
           "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check
       }
diff -r b6dacf6eabe3 -r 34b7550b66c7 src/Pure/Admin/check_sources.scala
--- a/src/Pure/Admin/check_sources.scala	Wed Nov 28 16:14:31 2018 +0100
+++ b/src/Pure/Admin/check_sources.scala	Wed Nov 28 16:18:40 2018 +0100
@@ -15,7 +15,7 @@
     val file_pos = path.position
     def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
 
-    if (space_explode('/', Word.lowercase(path.expand.split_ext._1.implode)).contains("aux"))
+    if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux"))
       Output.warning("Illegal file-name on Windows" + Position.here(file_pos))
 
     val content = File.read(path)
diff -r b6dacf6eabe3 -r 34b7550b66c7 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Wed Nov 28 16:14:31 2018 +0100
+++ b/src/Pure/General/path.scala	Wed Nov 28 16:18:40 2018 +0100
@@ -180,6 +180,9 @@
     }
   }
 
+  def drop_ext: Path = split_ext._1
+  def get_ext: String = split_ext._2
+
 
   /* expand */
 
diff -r b6dacf6eabe3 -r 34b7550b66c7 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Wed Nov 28 16:14:31 2018 +0100
+++ b/src/Pure/Thy/bibtex.scala	Wed Nov 28 16:18:40 2018 +0100
@@ -634,7 +634,7 @@
     {
       /* database files */
 
-      val bib_files = bib.map(path => path.split_ext._1)
+      val bib_files = bib.map(_.drop_ext)
       val bib_names =
       {
         val names0 = bib_files.map(_.file_name)
diff -r b6dacf6eabe3 -r 34b7550b66c7 src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Wed Nov 28 16:14:31 2018 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Wed Nov 28 16:18:40 2018 +0100
@@ -66,7 +66,7 @@
 
   class Dictionary private[Spell_Checker](val path: Path)
   {
-    val lang = path.split_ext._1.file_name
+    val lang = path.drop_ext.file_name
     val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
     override def toString: String = lang
   }