src/Tools/jEdit/src/spell_checker.scala
changeset 56583 c49607db182a
parent 56581 af3e6576e680
child 56584 9ccbac38bcad
equal deleted inserted replaced
56582:f05b7d6ec592 56583:c49607db182a
    19 import scala.annotation.tailrec
    19 import scala.annotation.tailrec
    20 import scala.collection.immutable.SortedMap
    20 import scala.collection.immutable.SortedMap
    21 
    21 
    22 import org.gjt.sp.jedit.jEdit
    22 import org.gjt.sp.jedit.jEdit
    23 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    23 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    24 import org.gjt.sp.jedit.menu.EnhancedMenuItem;
    24 import org.gjt.sp.jedit.menu.EnhancedMenuItem
    25 import org.gjt.sp.jedit.gui.DynamicContextMenuService;
    25 import org.gjt.sp.jedit.gui.DynamicContextMenuService
    26 
    26 
    27 
    27 
    28 object Spell_Checker
    28 object Spell_Checker
    29 {
    29 {
    30   /* words within text */
    30   /* words within text */