--- 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
}
--- 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)
--- 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 */
--- 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)
--- 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
}