clarified modules: spell-checker in Pure;
authorwenzelm
Tue Mar 07 14:33:14 2017 +0100 (2017-03-07)
changeset 651390a2c0712e432
parent 65138 64dfee6bd243
child 65140 1191df79aa1c
clarified modules: spell-checker in Pure;
src/Pure/PIDE/rendering.scala
src/Pure/Tools/spell_checker.scala
src/Pure/build-jars
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/context_menu.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/jedit_rendering.scala
src/Tools/jEdit/src/jedit_spell_checker.scala
src/Tools/jEdit/src/spell_checker.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Tue Mar 07 13:55:49 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Mar 07 14:33:14 2017 +0100
     1.3 @@ -169,6 +169,21 @@
     1.4      }
     1.5  
     1.6  
     1.7 +  /* spell checker */
     1.8 +
     1.9 +  private lazy val spell_checker_elements =
    1.10 +    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
    1.11 +
    1.12 +  def spell_checker_ranges(range: Text.Range): List[Text.Range] =
    1.13 +    snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
    1.14 +
    1.15 +  def spell_checker_point(range: Text.Range): Option[Text.Range] =
    1.16 +    snapshot.select(range, spell_checker_elements, _ =>
    1.17 +      {
    1.18 +        case info => Some(snapshot.convert(info.range))
    1.19 +      }).headOption.map(_.info)
    1.20 +
    1.21 +
    1.22    /* tooltips */
    1.23  
    1.24    def timing_threshold: Double
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/spell_checker.scala	Tue Mar 07 14:33:14 2017 +0100
     2.3 @@ -0,0 +1,272 @@
     2.4 +/*  Title:      Tools/jEdit/src/spell_checker.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Spell checker with completion, based on JOrtho (see
     2.8 +http://sourceforge.net/projects/jortho).
     2.9 +*/
    2.10 +
    2.11 +package isabelle
    2.12 +
    2.13 +
    2.14 +import java.lang.Class
    2.15 +
    2.16 +import scala.collection.mutable
    2.17 +import scala.annotation.tailrec
    2.18 +import scala.collection.immutable.SortedMap
    2.19 +
    2.20 +
    2.21 +object Spell_Checker
    2.22 +{
    2.23 +  /* words within text */
    2.24 +
    2.25 +  def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
    2.26 +    : List[Text.Info[String]] =
    2.27 +  {
    2.28 +    val result = new mutable.ListBuffer[Text.Info[String]]
    2.29 +    var offset = 0
    2.30 +
    2.31 +    def apostrophe(c: Int): Boolean =
    2.32 +      c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
    2.33 +
    2.34 +    @tailrec def scan(pred: Int => Boolean)
    2.35 +    {
    2.36 +      if (offset < text.length) {
    2.37 +        val c = text.codePointAt(offset)
    2.38 +        if (pred(c)) {
    2.39 +          offset += Character.charCount(c)
    2.40 +          scan(pred)
    2.41 +        }
    2.42 +      }
    2.43 +    }
    2.44 +
    2.45 +    while (offset < text.length) {
    2.46 +      scan(c => !Character.isLetter(c))
    2.47 +      val start = offset
    2.48 +      scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
    2.49 +      val stop = offset
    2.50 +      if (stop - start >= 2) {
    2.51 +        val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
    2.52 +        if (mark(info)) result += info
    2.53 +      }
    2.54 +    }
    2.55 +    result.toList
    2.56 +  }
    2.57 +
    2.58 +
    2.59 +  /* dictionaries */
    2.60 +
    2.61 +  class Dictionary private[Spell_Checker](val path: Path)
    2.62 +  {
    2.63 +    val lang = path.split_ext._1.base.implode
    2.64 +    val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
    2.65 +    override def toString: String = lang
    2.66 +  }
    2.67 +
    2.68 +  private object Decl
    2.69 +  {
    2.70 +    def apply(name: String, include: Boolean): String =
    2.71 +      if (include) name else "-" + name
    2.72 +
    2.73 +    def unapply(decl: String): Option[(String, Boolean)] =
    2.74 +    {
    2.75 +      val decl1 = decl.trim
    2.76 +      if (decl1 == "" || decl1.startsWith("#")) None
    2.77 +      else
    2.78 +        Library.try_unprefix("-", decl1.trim) match {
    2.79 +          case None => Some((decl1, true))
    2.80 +          case Some(decl2) => Some((decl2, false))
    2.81 +        }
    2.82 +    }
    2.83 +  }
    2.84 +
    2.85 +  def dictionaries(): List[Dictionary] =
    2.86 +    for {
    2.87 +      path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
    2.88 +      if path.is_file
    2.89 +    } yield new Dictionary(path)
    2.90 +
    2.91 +
    2.92 +  /* create spell checker */
    2.93 +
    2.94 +  def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
    2.95 +
    2.96 +  private sealed case class Update(include: Boolean, permanent: Boolean)
    2.97 +}
    2.98 +
    2.99 +
   2.100 +class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
   2.101 +{
   2.102 +  override def toString: String = dictionary.toString
   2.103 +
   2.104 +
   2.105 +  /* main dictionary content */
   2.106 +
   2.107 +  private var dict = new Object
   2.108 +  private var updates = SortedMap.empty[String, Spell_Checker.Update]
   2.109 +
   2.110 +  private def included_iterator(): Iterator[String] =
   2.111 +    for {
   2.112 +      (word, upd) <- updates.iterator
   2.113 +      if upd.include
   2.114 +    } yield word
   2.115 +
   2.116 +  private def excluded(word: String): Boolean =
   2.117 +    updates.get(word) match {
   2.118 +      case Some(upd) => !upd.include
   2.119 +      case None => false
   2.120 +    }
   2.121 +
   2.122 +  private def load()
   2.123 +  {
   2.124 +    val main_dictionary = split_lines(File.read_gzip(dictionary.path))
   2.125 +
   2.126 +    val permanent_updates =
   2.127 +      if (dictionary.user_path.is_file)
   2.128 +        for {
   2.129 +          Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
   2.130 +        } yield (word, Spell_Checker.Update(include, true))
   2.131 +      else Nil
   2.132 +
   2.133 +    updates =
   2.134 +      updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
   2.135 +        permanent_updates
   2.136 +
   2.137 +    val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
   2.138 +    val factory_cons = factory_class.getConstructor()
   2.139 +    factory_cons.setAccessible(true)
   2.140 +    val factory = factory_cons.newInstance()
   2.141 +
   2.142 +    val add = Untyped.method(factory_class, "add", classOf[String])
   2.143 +
   2.144 +    for {
   2.145 +      word <- main_dictionary.iterator ++ included_iterator()
   2.146 +      if !excluded(word)
   2.147 +    } add.invoke(factory, word)
   2.148 +
   2.149 +    dict = Untyped.method(factory_class, "create").invoke(factory)
   2.150 +  }
   2.151 +  load()
   2.152 +
   2.153 +  private def save()
   2.154 +  {
   2.155 +    val permanent_decls =
   2.156 +      (for {
   2.157 +        (word, upd) <- updates.iterator
   2.158 +        if upd.permanent
   2.159 +      } yield Spell_Checker.Decl(word, upd.include)).toList
   2.160 +
   2.161 +    if (permanent_decls.nonEmpty || dictionary.user_path.is_file) {
   2.162 +      val header = """# User updates for spell-checker dictionary
   2.163 +#
   2.164 +#   * each line contains at most one word
   2.165 +#   * extra blanks are ignored
   2.166 +#   * lines starting with "#" are stripped
   2.167 +#   * lines starting with "-" indicate excluded words
   2.168 +#
   2.169 +#:mode=text:encoding=UTF-8:
   2.170 +
   2.171 +"""
   2.172 +      Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
   2.173 +      File.write(dictionary.user_path, header + cat_lines(permanent_decls))
   2.174 +    }
   2.175 +  }
   2.176 +
   2.177 +  def update(word: String, include: Boolean, permanent: Boolean)
   2.178 +  {
   2.179 +    updates += (word -> Spell_Checker.Update(include, permanent))
   2.180 +
   2.181 +    if (include) {
   2.182 +      if (permanent) save()
   2.183 +      Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
   2.184 +    }
   2.185 +    else { save(); load() }
   2.186 +  }
   2.187 +
   2.188 +  def reset()
   2.189 +  {
   2.190 +    updates = SortedMap.empty
   2.191 +    load()
   2.192 +  }
   2.193 +
   2.194 +  def reset_enabled(): Int =
   2.195 +    updates.valuesIterator.filter(upd => !upd.permanent).length
   2.196 +
   2.197 +
   2.198 +  /* check known words */
   2.199 +
   2.200 +  def contains(word: String): Boolean =
   2.201 +    Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
   2.202 +      invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
   2.203 +
   2.204 +  def check(word: String): Boolean =
   2.205 +    word match {
   2.206 +      case Word.Case(c) if c != Word.Lowercase =>
   2.207 +        contains(word) || contains(Word.lowercase(word))
   2.208 +      case _ =>
   2.209 +        contains(word)
   2.210 +    }
   2.211 +
   2.212 +  def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
   2.213 +    Spell_Checker.marked_words(base, text, info => !check(info.info))
   2.214 +
   2.215 +
   2.216 +  /* suggestions for unknown words */
   2.217 +
   2.218 +  private def suggestions(word: String): Option[List[String]] =
   2.219 +  {
   2.220 +    val res =
   2.221 +      Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
   2.222 +        invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
   2.223 +    if (res.isEmpty) None else Some(res)
   2.224 +  }
   2.225 +
   2.226 +  def complete(word: String): List[String] =
   2.227 +    if (check(word)) Nil
   2.228 +    else {
   2.229 +      val word_case = Word.Case.unapply(word)
   2.230 +      def recover_case(s: String) =
   2.231 +        word_case match {
   2.232 +          case Some(c) => Word.Case(c, s)
   2.233 +          case None => s
   2.234 +        }
   2.235 +      val result =
   2.236 +        word_case match {
   2.237 +          case Some(c) if c != Word.Lowercase =>
   2.238 +            suggestions(word) orElse suggestions(Word.lowercase(word))
   2.239 +          case _ =>
   2.240 +            suggestions(word)
   2.241 +        }
   2.242 +      result.getOrElse(Nil).map(recover_case)
   2.243 +    }
   2.244 +
   2.245 +  def complete_enabled(word: String): Boolean = complete(word).nonEmpty
   2.246 +}
   2.247 +
   2.248 +
   2.249 +class Spell_Checker_Variable
   2.250 +{
   2.251 +  private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
   2.252 +  private var current_spell_checker = no_spell_checker
   2.253 +
   2.254 +  def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
   2.255 +
   2.256 +  def update(options: Options): Unit = synchronized {
   2.257 +    if (options.bool("spell_checker")) {
   2.258 +      val lang = options.string("spell_checker_dictionary")
   2.259 +      if (current_spell_checker._1 != lang) {
   2.260 +        Spell_Checker.dictionaries.find(_.lang == lang) match {
   2.261 +          case Some(dictionary) =>
   2.262 +            val spell_checker =
   2.263 +              Exn.capture { Spell_Checker(dictionary) } match {
   2.264 +                case Exn.Res(spell_checker) => Some(spell_checker)
   2.265 +                case Exn.Exn(_) => None
   2.266 +              }
   2.267 +            current_spell_checker = (lang, spell_checker)
   2.268 +          case None =>
   2.269 +            current_spell_checker = no_spell_checker
   2.270 +        }
   2.271 +      }
   2.272 +    }
   2.273 +    else current_spell_checker = no_spell_checker
   2.274 +  }
   2.275 +}
     3.1 --- a/src/Pure/build-jars	Tue Mar 07 13:55:49 2017 +0100
     3.2 +++ b/src/Pure/build-jars	Tue Mar 07 14:33:14 2017 +0100
     3.3 @@ -139,6 +139,7 @@
     3.4    Tools/print_operation.scala
     3.5    Tools/profiling_report.scala
     3.6    Tools/simplifier_trace.scala
     3.7 +  Tools/spell_checker.scala
     3.8    Tools/task_statistics.scala
     3.9    Tools/update_cartouches.scala
    3.10    Tools/update_header.scala
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 07 13:55:49 2017 +0100
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 07 14:33:14 2017 +0100
     4.3 @@ -43,6 +43,7 @@
     4.4    "src/jedit_rendering.scala"
     4.5    "src/jedit_resources.scala"
     4.6    "src/jedit_sessions.scala"
     4.7 +  "src/jedit_spell_checker.scala"
     4.8    "src/keymap_merge.scala"
     4.9    "src/monitor_dockable.scala"
    4.10    "src/output_dockable.scala"
    4.11 @@ -60,7 +61,6 @@
    4.12    "src/simplifier_trace_dockable.scala"
    4.13    "src/simplifier_trace_window.scala"
    4.14    "src/sledgehammer_dockable.scala"
    4.15 -  "src/spell_checker.scala"
    4.16    "src/state_dockable.scala"
    4.17    "src/symbols_dockable.scala"
    4.18    "src/syslog_dockable.scala"
     5.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Mar 07 13:55:49 2017 +0100
     5.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Mar 07 14:33:14 2017 +0100
     5.3 @@ -381,7 +381,7 @@
     5.4                case Some(rendering) =>
     5.5                  Completion.Result.merge(history, result1,
     5.6                    Completion.Result.merge(history,
     5.7 -                    Spell_Checker.completion(text_area, explicit, rendering),
     5.8 +                    JEdit_Spell_Checker.completion(text_area, explicit, rendering),
     5.9                      Completion.Result.merge(history,
    5.10                        path_completion(rendering),
    5.11                        Bibtex_JEdit.completion(history, text_area, rendering))))
     6.1 --- a/src/Tools/jEdit/src/context_menu.scala	Tue Mar 07 13:55:49 2017 +0100
     6.2 +++ b/src/Tools/jEdit/src/context_menu.scala	Tue Mar 07 14:33:14 2017 +0100
     6.3 @@ -29,7 +29,7 @@
     6.4          if (evt != null && evt.getSource == text_area.getPainter) {
     6.5            val offset = text_area.xyToOffset(evt.getX, evt.getY)
     6.6            if (offset >= 0)
     6.7 -            Spell_Checker.context_menu(text_area, offset) :::
     6.8 +            JEdit_Spell_Checker.context_menu(text_area, offset) :::
     6.9              Debugger_Dockable.context_menu(text_area, offset)
    6.10            else Nil
    6.11          }
     7.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 07 13:55:49 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 07 14:33:14 2017 +0100
     7.3 @@ -419,7 +419,7 @@
     7.4        doc_view <- Document_View.get(text_area)
     7.5        rendering = doc_view.get_rendering()
     7.6        range = JEdit_Lib.caret_range(text_area)
     7.7 -      Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
     7.8 +      Text.Info(_, word) <- JEdit_Spell_Checker.current_word(text_area, rendering, range)
     7.9      } {
    7.10        spell_checker.update(word, include, permanent)
    7.11        JEdit_Lib.jedit_views().foreach(_.repaint())
     8.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Tue Mar 07 13:55:49 2017 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Tue Mar 07 14:33:14 2017 +0100
     8.3 @@ -42,7 +42,7 @@
     8.4    val options = PIDE.options
     8.5  
     8.6    private val predefined =
     8.7 -    List(JEdit_Sessions.logic_selector(false), Spell_Checker.dictionaries_selector())
     8.8 +    List(JEdit_Sessions.logic_selector(false), JEdit_Spell_Checker.dictionaries_selector())
     8.9  
    8.10    protected val components =
    8.11      options.make_components(predefined,
     9.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Mar 07 13:55:49 2017 +0100
     9.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Mar 07 14:33:14 2017 +0100
     9.3 @@ -251,21 +251,6 @@
     9.4        }).headOption.map(_.info)
     9.5  
     9.6  
     9.7 -  /* spell checker */
     9.8 -
     9.9 -  private lazy val spell_checker_elements =
    9.10 -    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
    9.11 -
    9.12 -  def spell_checker_ranges(range: Text.Range): List[Text.Range] =
    9.13 -    snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
    9.14 -
    9.15 -  def spell_checker_point(range: Text.Range): Option[Text.Range] =
    9.16 -    snapshot.select(range, spell_checker_elements, _ =>
    9.17 -      {
    9.18 -        case info => Some(snapshot.convert(info.range))
    9.19 -      }).headOption.map(_.info)
    9.20 -
    9.21 -
    9.22    /* breakpoints */
    9.23  
    9.24    def breakpoint(range: Text.Range): Option[(Command, Long)] =
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala	Tue Mar 07 14:33:14 2017 +0100
    10.3 @@ -0,0 +1,129 @@
    10.4 +/*  Title:      Tools/jEdit/src/jedit_spell_checker.scala
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +Specific spell-checker support for Isabelle/jEdit.
    10.8 +*/
    10.9 +
   10.10 +package isabelle.jedit
   10.11 +
   10.12 +
   10.13 +import isabelle._
   10.14 +
   10.15 +import javax.swing.JMenuItem
   10.16 +import scala.swing.ComboBox
   10.17 +
   10.18 +import org.gjt.sp.jedit.menu.EnhancedMenuItem
   10.19 +import org.gjt.sp.jedit.jEdit
   10.20 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
   10.21 +
   10.22 +
   10.23 +object JEdit_Spell_Checker
   10.24 +{
   10.25 +  /* words within text */
   10.26 +
   10.27 +  def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range)
   10.28 +    : Option[Text.Info[String]] =
   10.29 +  {
   10.30 +    for {
   10.31 +      spell_range <- rendering.spell_checker_point(range)
   10.32 +      text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
   10.33 +      info <- Spell_Checker.marked_words(
   10.34 +        spell_range.start, text, info => info.range.overlaps(range)).headOption
   10.35 +    } yield info
   10.36 +  }
   10.37 +
   10.38 +
   10.39 +  /* completion */
   10.40 +
   10.41 +  def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering)
   10.42 +      : Option[Completion.Result] =
   10.43 +  {
   10.44 +    for {
   10.45 +      spell_checker <- PIDE.spell_checker.get
   10.46 +      if explicit
   10.47 +      range = JEdit_Lib.before_caret_range(text_area, rendering)
   10.48 +      word <- current_word(text_area, rendering, range)
   10.49 +      words = spell_checker.complete(word.info)
   10.50 +      if words.nonEmpty
   10.51 +      descr = "(from dictionary " + quote(spell_checker.toString) + ")"
   10.52 +      items =
   10.53 +        words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
   10.54 +    } yield Completion.Result(word.range, word.info, false, items)
   10.55 +  }
   10.56 +
   10.57 +
   10.58 +  /* context menu */
   10.59 +
   10.60 +  def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
   10.61 +  {
   10.62 +    val result =
   10.63 +      for {
   10.64 +        spell_checker <- PIDE.spell_checker.get
   10.65 +        doc_view <- Document_View.get(text_area)
   10.66 +        rendering = doc_view.get_rendering()
   10.67 +        range = JEdit_Lib.point_range(text_area.getBuffer, offset)
   10.68 +        Text.Info(_, word) <- current_word(text_area, rendering, range)
   10.69 +      } yield (spell_checker, word)
   10.70 +
   10.71 +    result match {
   10.72 +      case Some((spell_checker, word)) =>
   10.73 +
   10.74 +        val context = jEdit.getActionContext()
   10.75 +        def item(name: String): JMenuItem =
   10.76 +          new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
   10.77 +
   10.78 +        val complete_items =
   10.79 +          if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word"))
   10.80 +          else Nil
   10.81 +
   10.82 +        val update_items =
   10.83 +          if (spell_checker.check(word))
   10.84 +            List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
   10.85 +          else
   10.86 +            List(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
   10.87 +
   10.88 +        val reset_items =
   10.89 +          spell_checker.reset_enabled() match {
   10.90 +            case 0 => Nil
   10.91 +            case n =>
   10.92 +              val name = "isabelle.reset-words"
   10.93 +              val label = context.getAction(name).getLabel
   10.94 +              List(new EnhancedMenuItem(label + " (" + n + ")", name, context))
   10.95 +          }
   10.96 +
   10.97 +        complete_items ::: update_items ::: reset_items
   10.98 +
   10.99 +      case None => Nil
  10.100 +    }
  10.101 +  }
  10.102 +
  10.103 +
  10.104 +  /* dictionaries */
  10.105 +
  10.106 +  def dictionaries_selector(): Option_Component =
  10.107 +  {
  10.108 +    GUI_Thread.require {}
  10.109 +
  10.110 +    val option_name = "spell_checker_dictionary"
  10.111 +    val opt = PIDE.options.value.check_name(option_name)
  10.112 +
  10.113 +    val entries = Spell_Checker.dictionaries()
  10.114 +    val component = new ComboBox(entries) with Option_Component {
  10.115 +      name = option_name
  10.116 +      val title = opt.title()
  10.117 +      def load: Unit =
  10.118 +      {
  10.119 +        val lang = PIDE.options.string(option_name)
  10.120 +        entries.find(_.lang == lang) match {
  10.121 +          case Some(entry) => selection.item = entry
  10.122 +          case None =>
  10.123 +        }
  10.124 +      }
  10.125 +      def save: Unit = PIDE.options.string(option_name) = selection.item.lang
  10.126 +    }
  10.127 +
  10.128 +    component.load()
  10.129 +    component.tooltip = GUI.tooltip_lines(opt.print_default)
  10.130 +    component
  10.131 +  }
  10.132 +}
    11.1 --- a/src/Tools/jEdit/src/spell_checker.scala	Tue Mar 07 13:55:49 2017 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,392 +0,0 @@
    11.4 -/*  Title:      Tools/jEdit/src/spell_checker.scala
    11.5 -    Author:     Makarius
    11.6 -
    11.7 -Spell checker with completion, based on JOrtho (see
    11.8 -http://sourceforge.net/projects/jortho).
    11.9 -*/
   11.10 -
   11.11 -package isabelle.jedit
   11.12 -
   11.13 -
   11.14 -import isabelle._
   11.15 -
   11.16 -import java.lang.Class
   11.17 -
   11.18 -import javax.swing.JMenuItem
   11.19 -
   11.20 -import scala.collection.mutable
   11.21 -import scala.swing.ComboBox
   11.22 -import scala.annotation.tailrec
   11.23 -import scala.collection.immutable.SortedMap
   11.24 -
   11.25 -import org.gjt.sp.jedit.menu.EnhancedMenuItem
   11.26 -import org.gjt.sp.jedit.{jEdit, Buffer}
   11.27 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
   11.28 -
   11.29 -
   11.30 -object Spell_Checker
   11.31 -{
   11.32 -  /** words within text **/
   11.33 -
   11.34 -  def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean)
   11.35 -    : List[Text.Info[String]] =
   11.36 -  {
   11.37 -    val result = new mutable.ListBuffer[Text.Info[String]]
   11.38 -    var offset = 0
   11.39 -
   11.40 -    def apostrophe(c: Int): Boolean =
   11.41 -      c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'')
   11.42 -
   11.43 -    @tailrec def scan(pred: Int => Boolean)
   11.44 -    {
   11.45 -      if (offset < text.length) {
   11.46 -        val c = text.codePointAt(offset)
   11.47 -        if (pred(c)) {
   11.48 -          offset += Character.charCount(c)
   11.49 -          scan(pred)
   11.50 -        }
   11.51 -      }
   11.52 -    }
   11.53 -
   11.54 -    while (offset < text.length) {
   11.55 -      scan(c => !Character.isLetter(c))
   11.56 -      val start = offset
   11.57 -      scan(c => Character.isLetterOrDigit(c) || apostrophe(c))
   11.58 -      val stop = offset
   11.59 -      if (stop - start >= 2) {
   11.60 -        val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop))
   11.61 -        if (mark(info)) result += info
   11.62 -      }
   11.63 -    }
   11.64 -    result.toList
   11.65 -  }
   11.66 -
   11.67 -  def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range)
   11.68 -    : Option[Text.Info[String]] =
   11.69 -  {
   11.70 -    for {
   11.71 -      spell_range <- rendering.spell_checker_point(range)
   11.72 -      text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range)
   11.73 -      info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption
   11.74 -    } yield info
   11.75 -  }
   11.76 -
   11.77 -
   11.78 -
   11.79 -  /** completion **/
   11.80 -
   11.81 -  def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering)
   11.82 -      : Option[Completion.Result] =
   11.83 -  {
   11.84 -    for {
   11.85 -      spell_checker <- PIDE.spell_checker.get
   11.86 -      if explicit
   11.87 -      range = JEdit_Lib.before_caret_range(text_area, rendering)
   11.88 -      word <- current_word(text_area, rendering, range)
   11.89 -      words = spell_checker.complete(word.info)
   11.90 -      if words.nonEmpty
   11.91 -      descr = "(from dictionary " + quote(spell_checker.toString) + ")"
   11.92 -      items =
   11.93 -        words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
   11.94 -    } yield Completion.Result(word.range, word.info, false, items)
   11.95 -  }
   11.96 -
   11.97 -
   11.98 -
   11.99 -  /** context menu **/
  11.100 -
  11.101 -  def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
  11.102 -  {
  11.103 -    val result =
  11.104 -      for {
  11.105 -        spell_checker <- PIDE.spell_checker.get
  11.106 -        doc_view <- Document_View.get(text_area)
  11.107 -        rendering = doc_view.get_rendering()
  11.108 -        range = JEdit_Lib.point_range(text_area.getBuffer, offset)
  11.109 -        Text.Info(_, word) <- current_word(text_area, rendering, range)
  11.110 -      } yield (spell_checker, word)
  11.111 -
  11.112 -    result match {
  11.113 -      case Some((spell_checker, word)) =>
  11.114 -
  11.115 -        val context = jEdit.getActionContext()
  11.116 -        def item(name: String): JMenuItem =
  11.117 -          new EnhancedMenuItem(context.getAction(name).getLabel, name, context)
  11.118 -
  11.119 -        val complete_items =
  11.120 -          if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word"))
  11.121 -          else Nil
  11.122 -
  11.123 -        val update_items =
  11.124 -          if (spell_checker.check(word))
  11.125 -            List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently"))
  11.126 -          else
  11.127 -            List(item("isabelle.include-word"), item("isabelle.include-word-permanently"))
  11.128 -
  11.129 -        val reset_items =
  11.130 -          spell_checker.reset_enabled() match {
  11.131 -            case 0 => Nil
  11.132 -            case n =>
  11.133 -              val name = "isabelle.reset-words"
  11.134 -              val label = context.getAction(name).getLabel
  11.135 -              List(new EnhancedMenuItem(label + " (" + n + ")", name, context))
  11.136 -          }
  11.137 -
  11.138 -        complete_items ::: update_items ::: reset_items
  11.139 -
  11.140 -      case None => Nil
  11.141 -    }
  11.142 -  }
  11.143 -
  11.144 -
  11.145 -
  11.146 -  /** dictionary **/
  11.147 -
  11.148 -  /* declarations */
  11.149 -
  11.150 -  class Dictionary private[Spell_Checker](val path: Path)
  11.151 -  {
  11.152 -    val lang = path.split_ext._1.base.implode
  11.153 -    val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
  11.154 -    override def toString: String = lang
  11.155 -  }
  11.156 -
  11.157 -  private object Decl
  11.158 -  {
  11.159 -    def apply(name: String, include: Boolean): String =
  11.160 -      if (include) name else "-" + name
  11.161 -
  11.162 -    def unapply(decl: String): Option[(String, Boolean)] =
  11.163 -    {
  11.164 -      val decl1 = decl.trim
  11.165 -      if (decl1 == "" || decl1.startsWith("#")) None
  11.166 -      else
  11.167 -        Library.try_unprefix("-", decl1.trim) match {
  11.168 -          case None => Some((decl1, true))
  11.169 -          case Some(decl2) => Some((decl2, false))
  11.170 -        }
  11.171 -    }
  11.172 -  }
  11.173 -
  11.174 -
  11.175 -  /* known dictionaries */
  11.176 -
  11.177 -  def dictionaries(): List[Dictionary] =
  11.178 -    for {
  11.179 -      path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES"))
  11.180 -      if path.is_file
  11.181 -    } yield new Dictionary(path)
  11.182 -
  11.183 -  def dictionaries_selector(): Option_Component =
  11.184 -  {
  11.185 -    GUI_Thread.require {}
  11.186 -
  11.187 -    val option_name = "spell_checker_dictionary"
  11.188 -    val opt = PIDE.options.value.check_name(option_name)
  11.189 -
  11.190 -    val entries = dictionaries()
  11.191 -    val component = new ComboBox(entries) with Option_Component {
  11.192 -      name = option_name
  11.193 -      val title = opt.title()
  11.194 -      def load: Unit =
  11.195 -      {
  11.196 -        val lang = PIDE.options.string(option_name)
  11.197 -        entries.find(_.lang == lang) match {
  11.198 -          case Some(entry) => selection.item = entry
  11.199 -          case None =>
  11.200 -        }
  11.201 -      }
  11.202 -      def save: Unit = PIDE.options.string(option_name) = selection.item.lang
  11.203 -    }
  11.204 -
  11.205 -    component.load()
  11.206 -    component.tooltip = GUI.tooltip_lines(opt.print_default)
  11.207 -    component
  11.208 -  }
  11.209 -
  11.210 -
  11.211 -  /* create spell checker */
  11.212 -
  11.213 -  def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary)
  11.214 -
  11.215 -  private sealed case class Update(include: Boolean, permanent: Boolean)
  11.216 -}
  11.217 -
  11.218 -
  11.219 -class Spell_Checker private(dictionary: Spell_Checker.Dictionary)
  11.220 -{
  11.221 -  override def toString: String = dictionary.toString
  11.222 -
  11.223 -
  11.224 -  /* main dictionary content */
  11.225 -
  11.226 -  private var dict = new Object
  11.227 -  private var updates = SortedMap.empty[String, Spell_Checker.Update]
  11.228 -
  11.229 -  private def included_iterator(): Iterator[String] =
  11.230 -    for {
  11.231 -      (word, upd) <- updates.iterator
  11.232 -      if upd.include
  11.233 -    } yield word
  11.234 -
  11.235 -  private def excluded(word: String): Boolean =
  11.236 -    updates.get(word) match {
  11.237 -      case Some(upd) => !upd.include
  11.238 -      case None => false
  11.239 -    }
  11.240 -
  11.241 -  private def load()
  11.242 -  {
  11.243 -    val main_dictionary = split_lines(File.read_gzip(dictionary.path))
  11.244 -
  11.245 -    val permanent_updates =
  11.246 -      if (dictionary.user_path.is_file)
  11.247 -        for {
  11.248 -          Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
  11.249 -        } yield (word, Spell_Checker.Update(include, true))
  11.250 -      else Nil
  11.251 -
  11.252 -    updates =
  11.253 -      updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++
  11.254 -        permanent_updates
  11.255 -
  11.256 -    val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
  11.257 -    val factory_cons = factory_class.getConstructor()
  11.258 -    factory_cons.setAccessible(true)
  11.259 -    val factory = factory_cons.newInstance()
  11.260 -
  11.261 -    val add = Untyped.method(factory_class, "add", classOf[String])
  11.262 -
  11.263 -    for {
  11.264 -      word <- main_dictionary.iterator ++ included_iterator()
  11.265 -      if !excluded(word)
  11.266 -    } add.invoke(factory, word)
  11.267 -
  11.268 -    dict = Untyped.method(factory_class, "create").invoke(factory)
  11.269 -  }
  11.270 -  load()
  11.271 -
  11.272 -  private def save()
  11.273 -  {
  11.274 -    val permanent_decls =
  11.275 -      (for {
  11.276 -        (word, upd) <- updates.iterator
  11.277 -        if upd.permanent
  11.278 -      } yield Spell_Checker.Decl(word, upd.include)).toList
  11.279 -
  11.280 -    if (permanent_decls.nonEmpty || dictionary.user_path.is_file) {
  11.281 -      val header = """# User updates for spell-checker dictionary
  11.282 -#
  11.283 -#   * each line contains at most one word
  11.284 -#   * extra blanks are ignored
  11.285 -#   * lines starting with "#" are stripped
  11.286 -#   * lines starting with "-" indicate excluded words
  11.287 -#
  11.288 -#:mode=text:encoding=UTF-8:
  11.289 -
  11.290 -"""
  11.291 -      Isabelle_System.mkdirs(dictionary.user_path.expand.dir)
  11.292 -      File.write(dictionary.user_path, header + cat_lines(permanent_decls))
  11.293 -    }
  11.294 -  }
  11.295 -
  11.296 -  def update(word: String, include: Boolean, permanent: Boolean)
  11.297 -  {
  11.298 -    updates += (word -> Spell_Checker.Update(include, permanent))
  11.299 -
  11.300 -    if (include) {
  11.301 -      if (permanent) save()
  11.302 -      Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
  11.303 -    }
  11.304 -    else { save(); load() }
  11.305 -  }
  11.306 -
  11.307 -  def reset()
  11.308 -  {
  11.309 -    updates = SortedMap.empty
  11.310 -    load()
  11.311 -  }
  11.312 -
  11.313 -  def reset_enabled(): Int =
  11.314 -    updates.valuesIterator.filter(upd => !upd.permanent).length
  11.315 -
  11.316 -
  11.317 -  /* check known words */
  11.318 -
  11.319 -  def contains(word: String): Boolean =
  11.320 -    Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
  11.321 -      invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
  11.322 -
  11.323 -  def check(word: String): Boolean =
  11.324 -    word match {
  11.325 -      case Word.Case(c) if c != Word.Lowercase =>
  11.326 -        contains(word) || contains(Word.lowercase(word))
  11.327 -      case _ =>
  11.328 -        contains(word)
  11.329 -    }
  11.330 -
  11.331 -  def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] =
  11.332 -    Spell_Checker.marked_words(base, text, info => !check(info.info))
  11.333 -
  11.334 -
  11.335 -  /* suggestions for unknown words */
  11.336 -
  11.337 -  private def suggestions(word: String): Option[List[String]] =
  11.338 -  {
  11.339 -    val res =
  11.340 -      Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
  11.341 -        invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
  11.342 -    if (res.isEmpty) None else Some(res)
  11.343 -  }
  11.344 -
  11.345 -  def complete(word: String): List[String] =
  11.346 -    if (check(word)) Nil
  11.347 -    else {
  11.348 -      val word_case = Word.Case.unapply(word)
  11.349 -      def recover_case(s: String) =
  11.350 -        word_case match {
  11.351 -          case Some(c) => Word.Case(c, s)
  11.352 -          case None => s
  11.353 -        }
  11.354 -      val result =
  11.355 -        word_case match {
  11.356 -          case Some(c) if c != Word.Lowercase =>
  11.357 -            suggestions(word) orElse suggestions(Word.lowercase(word))
  11.358 -          case _ =>
  11.359 -            suggestions(word)
  11.360 -        }
  11.361 -      result.getOrElse(Nil).map(recover_case)
  11.362 -    }
  11.363 -
  11.364 -  def complete_enabled(word: String): Boolean = complete(word).nonEmpty
  11.365 -}
  11.366 -
  11.367 -
  11.368 -class Spell_Checker_Variable
  11.369 -{
  11.370 -  private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None)
  11.371 -  private var current_spell_checker = no_spell_checker
  11.372 -
  11.373 -  def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 }
  11.374 -
  11.375 -  def update(options: Options): Unit = synchronized {
  11.376 -    if (options.bool("spell_checker")) {
  11.377 -      val lang = options.string("spell_checker_dictionary")
  11.378 -      if (current_spell_checker._1 != lang) {
  11.379 -        Spell_Checker.dictionaries.find(_.lang == lang) match {
  11.380 -          case Some(dictionary) =>
  11.381 -            val spell_checker =
  11.382 -              Exn.capture { Spell_Checker(dictionary) } match {
  11.383 -                case Exn.Res(spell_checker) => Some(spell_checker)
  11.384 -                case Exn.Exn(_) => None
  11.385 -              }
  11.386 -            current_spell_checker = (lang, spell_checker)
  11.387 -          case None =>
  11.388 -            current_spell_checker = no_spell_checker
  11.389 -        }
  11.390 -      }
  11.391 -    }
  11.392 -    else current_spell_checker = no_spell_checker
  11.393 -  }
  11.394 -}
  11.395 -