src/Pure/Tools/spell_checker.scala
changeset 69367 34b7550b66c7
parent 69366 b6dacf6eabe3
child 71383 8313dca6dee9
--- 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
   }