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 }