13 import java.lang.Class |
13 import java.lang.Class |
14 |
14 |
15 import scala.collection.mutable |
15 import scala.collection.mutable |
16 import scala.swing.ComboBox |
16 import scala.swing.ComboBox |
17 import scala.annotation.tailrec |
17 import scala.annotation.tailrec |
|
18 import scala.collection.immutable.{SortedSet, SortedMap} |
18 |
19 |
19 |
20 |
20 object Spell_Checker |
21 object Spell_Checker |
21 { |
22 { |
22 /* marked words within text */ |
23 /* marked words within text */ |
53 } |
54 } |
54 result.toList |
55 result.toList |
55 } |
56 } |
56 |
57 |
57 |
58 |
58 /* dictionary consisting of word list */ |
59 /* dictionary -- include/exclude word list */ |
|
60 |
|
61 private val USER_DICTIONARIES = Path.explode("$ISABELLE_HOME_USER/dictionaries") |
59 |
62 |
60 class Dictionary private [Spell_Checker](path: Path) |
63 class Dictionary private [Spell_Checker](path: Path) |
61 { |
64 { |
62 val lang = path.split_ext._1.base.implode |
65 val lang = path.split_ext._1.base.implode |
63 override def toString: String = lang |
66 override def toString: String = lang |
64 |
67 |
65 def load_words: List[String] = |
68 private val user_path = USER_DICTIONARIES + Path.basic(lang) |
66 path.split_ext._2 match { |
69 |
67 case "gz" => split_lines(File.read_gzip(path)) |
70 def load(): (List[String], List[String], List[String]) = |
68 case "" => split_lines(File.read(path)) |
71 { |
69 case ext => error("Bad file extension for dictionary " + path) |
72 val main = split_lines(File.read_gzip(path)) |
70 } |
73 |
|
74 val user_entries = |
|
75 if (user_path.is_file) |
|
76 for { |
|
77 raw_line <- split_lines(File.read(user_path)) |
|
78 line = raw_line.trim |
|
79 if line != "" && !line.startsWith("#") |
|
80 entry = |
|
81 Library.try_unprefix("-", line) match { |
|
82 case Some(s) => (s, false) |
|
83 case None => (line, true) |
|
84 } |
|
85 } yield entry |
|
86 else Nil |
|
87 val user = SortedMap.empty[String, Boolean] ++ user_entries |
|
88 val include = user.toList.filter(_._2).map(_._1) |
|
89 val exclude = user.toList.filterNot(_._2).map(_._1) |
|
90 |
|
91 (main, include, exclude) |
|
92 } |
|
93 |
|
94 def save(include: List[String], exclude: List[String]) |
|
95 { |
|
96 if (!include.isEmpty || !exclude.isEmpty || user_path.is_file) { |
|
97 val header = """# Spell-checker dictionary |
|
98 # |
|
99 # * each line contains at most one word |
|
100 # * extra blanks are ignored |
|
101 # * lines starting with "#" are ignored |
|
102 # * lines starting with "-" indicate excluded words |
|
103 # * later entries take precedence |
|
104 # |
|
105 """ |
|
106 Isabelle_System.mkdirs(USER_DICTIONARIES) |
|
107 File.write(user_path, header + cat_lines(include ::: exclude.map("-" + _))) |
|
108 } |
|
109 } |
71 } |
110 } |
72 |
111 |
73 |
112 |
74 /* known dictionaries */ |
113 /* known dictionaries */ |
75 |
114 |
115 |
154 |
116 class Spell_Checker private(dictionary: Spell_Checker.Dictionary) |
155 class Spell_Checker private(dictionary: Spell_Checker.Dictionary) |
117 { |
156 { |
118 override def toString: String = dictionary.toString |
157 override def toString: String = dictionary.toString |
119 |
158 |
120 private val dict = |
159 private var dict = new Object |
|
160 private var include_set = SortedSet.empty[String] |
|
161 private var exclude_set = SortedSet.empty[String] |
|
162 |
|
163 private def make_dict() |
121 { |
164 { |
122 val factory_class = Class.forName("com.inet.jortho.DictionaryFactory") |
165 val factory_class = Class.forName("com.inet.jortho.DictionaryFactory") |
123 val factory_cons = factory_class.getConstructor() |
166 val factory_cons = factory_class.getConstructor() |
124 factory_cons.setAccessible(true) |
167 factory_cons.setAccessible(true) |
125 val factory = factory_cons.newInstance() |
168 val factory = factory_cons.newInstance() |
126 |
169 |
127 val add = factory_class.getDeclaredMethod("add", classOf[String]) |
170 val add = factory_class.getDeclaredMethod("add", classOf[String]) |
128 add.setAccessible(true) |
171 add.setAccessible(true) |
129 dictionary.load_words.foreach(add.invoke(factory, _)) |
172 |
|
173 val (main, include, exclude) = dictionary.load() |
|
174 include_set = SortedSet.empty[String] ++ include |
|
175 exclude_set = SortedSet.empty[String] ++ exclude |
|
176 |
|
177 for { |
|
178 word <- main.iterator ++ include.iterator |
|
179 if !exclude_set.contains(word) |
|
180 } add.invoke(factory, word) |
130 |
181 |
131 val create = factory_class.getDeclaredMethod("create") |
182 val create = factory_class.getDeclaredMethod("create") |
132 create.setAccessible(true) |
183 create.setAccessible(true) |
133 create.invoke(factory) |
184 dict = create.invoke(factory) |
134 } |
185 } |
135 |
186 make_dict() |
136 def add(word: String) |
187 |
137 { |
188 def save() |
|
189 { |
|
190 dictionary.save(include_set.toList, exclude_set.toList) |
|
191 } |
|
192 |
|
193 def include(word: String) |
|
194 { |
|
195 include_set += word |
|
196 exclude_set -= word |
|
197 |
138 val m = dict.getClass.getDeclaredMethod("add", classOf[String]) |
198 val m = dict.getClass.getDeclaredMethod("add", classOf[String]) |
139 m.setAccessible(true) |
199 m.setAccessible(true) |
140 m.invoke(dict, word) |
200 m.invoke(dict, word) |
|
201 |
|
202 save() |
|
203 } |
|
204 |
|
205 def exclude(word: String) |
|
206 { |
|
207 include_set -= word |
|
208 exclude_set += word |
|
209 |
|
210 save() |
|
211 make_dict() |
141 } |
212 } |
142 |
213 |
143 def contains(word: String): Boolean = |
214 def contains(word: String): Boolean = |
144 { |
215 { |
145 val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String]) |
216 val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String]) |