src/Pure/Tools/spell_checker.scala
changeset 71951 9644811b5b0a
parent 71816 97ccf48c2f0c
child 72611 e48d93811ed7
equal deleted inserted replaced
71950:713fafb3de79 71951:9644811b5b0a
   139     updates =
   139     updates =
   140       updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
   140       updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
   141         permanent_updates
   141         permanent_updates
   142 
   142 
   143     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
   143     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
   144     val factory_cons = factory_class.getConstructor()
   144     val factory_constructor = factory_class.getConstructor()
   145     factory_cons.setAccessible(true)
   145     factory_constructor.setAccessible(true)
   146     val factory = factory_cons.newInstance()
   146     val factory = factory_constructor.newInstance()
   147 
   147 
   148     val add = Untyped.method(factory_class, "add", classOf[String])
   148     val add = Untyped.method(factory_class, "add", classOf[String])
   149 
   149 
   150     for {
   150     for {
   151       word <- main_dictionary.iterator ++ included_iterator()
   151       word <- main_dictionary.iterator ++ included_iterator()