equal
deleted
inserted
replaced
86 case Some(decl2) => Some((decl2, false)) |
86 case Some(decl2) => Some((decl2, false)) |
87 } |
87 } |
88 } |
88 } |
89 } |
89 } |
90 |
90 |
91 def dictionaries(): List[Dictionary] = |
91 def dictionaries: List[Dictionary] = |
92 for { |
92 for { |
93 path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES")) |
93 path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES")) |
94 if path.is_file |
94 if path.is_file |
95 } yield new Dictionary(path) |
95 } yield new Dictionary(path) |
96 |
96 |