equal
deleted
inserted
replaced
55 |
55 |
56 /* dictionaries */ |
56 /* dictionaries */ |
57 |
57 |
58 class Dictionary private[Spell_Checker](val path: Path) |
58 class Dictionary private[Spell_Checker](val path: Path) |
59 { |
59 { |
60 val lang = path.split_ext._1.base.implode |
60 val lang = path.split_ext._1.base_name |
61 val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang) |
61 val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang) |
62 override def toString: String = lang |
62 override def toString: String = lang |
63 } |
63 } |
64 |
64 |
65 private object Decl |
65 private object Decl |