# HG changeset patch # User wenzelm # Date 1397332770 -7200 # Node ID 1afb78a933768fc128c2a6eb1eb47b3b1dcda5c5 # Parent 8f1e7596deb7db5943b24680a3583267ce190f80# Parent 7bef3cd6a69ce4ccd2d57b9f7d288f49173d4f36 merged diff -r 8f1e7596deb7 -r 1afb78a93376 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sat Apr 12 11:27:36 2014 +0200 +++ b/Admin/components/components.sha1 Sat Apr 12 21:59:30 2014 +0200 @@ -42,6 +42,7 @@ 054c1300128f8abd0f46a3e92c756ccdb96ff2af jedit_build-20140405.tar.gz 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz +ffe179867cf5ffaabbb6bb096db9bdc0d7110065 jortho-1.0.tar.gz 6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz 5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz 377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz diff -r 8f1e7596deb7 -r 1afb78a93376 Admin/components/main --- a/Admin/components/main Sat Apr 12 11:27:36 2014 +0200 +++ b/Admin/components/main Sat Apr 12 21:59:30 2014 +0200 @@ -6,6 +6,7 @@ jdk-7u40 jedit_build-20140405 jfreechart-1.0.14-1 +jortho-1.0 kodkodi-1.5.2 polyml-5.5.1-1 scala-2.10.4 diff -r 8f1e7596deb7 -r 1afb78a93376 NEWS --- a/NEWS Sat Apr 12 11:27:36 2014 +0200 +++ b/NEWS Sat Apr 12 21:59:30 2014 +0200 @@ -94,6 +94,8 @@ - More reliable treatment of GUI events vs. completion popups: avoid loosing keystrokes with slow / remote graphics displays. +* Spell-checker support for document text, comments etc. + * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. Open text buffers take precedence over copies within the file-system. diff -r 8f1e7596deb7 -r 1afb78a93376 src/Pure/GUI/color_value.scala --- a/src/Pure/GUI/color_value.scala Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Pure/GUI/color_value.scala Sat Apr 12 21:59:30 2014 +0200 @@ -31,7 +31,7 @@ val g = new java.lang.Integer(c.getGreen) val b = new java.lang.Integer(c.getBlue) val a = new java.lang.Integer(c.getAlpha) - String.format("%02x%02x%02x%02x", r, g, b, a).toUpperCase + Library.uppercase(String.format("%02x%02x%02x%02x", r, g, b, a)) } def apply(s: String): Color = diff -r 8f1e7596deb7 -r 1afb78a93376 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Pure/PIDE/markup.ML Sat Apr 12 21:59:30 2014 +0200 @@ -62,6 +62,7 @@ val breakN: string val break: int -> T val fbreakN: string val fbreak: T val itemN: string val item: T + val wordsN: string val words: T val hiddenN: string val hidden: T val system_optionN: string val theoryN: string @@ -354,7 +355,9 @@ val (itemN, item) = markup_elem "item"; -(* hidden text *) +(* text properties *) + +val (wordsN, words) = markup_elem "words"; val (hiddenN, hidden) = markup_elem "hidden"; diff -r 8f1e7596deb7 -r 1afb78a93376 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Pure/PIDE/markup.scala Sat Apr 12 21:59:30 2014 +0200 @@ -137,7 +137,9 @@ val SEPARATOR = "separator" - /* hidden text */ + /* text properties */ + + val WORDS = "words" val HIDDEN = "hidden" diff -r 8f1e7596deb7 -r 1afb78a93376 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Pure/System/options.scala Sat Apr 12 21:59:30 2014 +0200 @@ -58,7 +58,7 @@ case word :: rest if word == strip => rest case _ => words } - words1.map(Library.capitalize).mkString(" ") + words1.map(Library.capitalize(_)).mkString(" ") } def unknown: Boolean = typ == Unknown diff -r 8f1e7596deb7 -r 1afb78a93376 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Pure/Thy/thy_output.ML Sat Apr 12 21:59:30 2014 +0200 @@ -24,7 +24,6 @@ val integer: string -> int datatype markup = Markup | MarkupEnv | Verbatim val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string - val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string val check_text: Symbol_Pos.source -> Toplevel.state -> unit val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T @@ -157,7 +156,7 @@ end; -(* eval_antiquote *) +(* eval_antiq *) fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) = let @@ -169,18 +168,25 @@ val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes; in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end; + +(* check_text *) + fun eval_antiquote lex state (txt, pos) = let + fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)] + | words (Antiquote.Antiq _) = []; + fun expand (Antiquote.Text ss) = Symbol_Pos.content ss | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq; + val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos); + val _ = Position.reports (maps words ants); in if Toplevel.is_toplevel state andalso not (forall Antiquote.is_text ants) then error ("Unknown context -- cannot expand document antiquotations" ^ Position.here pos) else implode (map expand ants) end; - fun check_text {delimited, text, pos} state = (Position.report pos (Markup.language_document delimited); if Toplevel.is_skipped_proof state then () diff -r 8f1e7596deb7 -r 1afb78a93376 src/Pure/library.scala --- a/src/Pure/library.scala Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Pure/library.scala Sat Apr 12 21:59:30 2014 +0200 @@ -103,12 +103,19 @@ /* strings */ - def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH) - def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH) + def lowercase(str: String, locale: Locale = Locale.ENGLISH): String = str.toLowerCase(locale) + def uppercase(str: String, locale: Locale = Locale.ENGLISH): String = str.toUpperCase(locale) + + def capitalize(str: String, locale: Locale = Locale.ENGLISH): String = + if (str.length == 0) str + else uppercase(str.substring(0, 1), locale) + str.substring(1) - def capitalize(str: String): String = - if (str.length == 0) str - else uppercase(str.substring(0, 1)) + str.substring(1) + def is_capitalized(str: String): Boolean = + str.length > 0 && + Character.isUpperCase(str(0)) && str.substring(1).forall(Character.isLowerCase(_)) + + def is_all_caps(str: String): Boolean = + str.length > 0 && str.forall(Character.isUpperCase(_)) def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None diff -r 8f1e7596deb7 -r 1afb78a93376 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Tools/jEdit/etc/options Sat Apr 12 21:59:30 2014 +0200 @@ -49,6 +49,18 @@ -- "insert uniquely completed abbreviation immediately into buffer" +section "Spell Checker" + +public option spell_checker : bool = true + -- "enable spell-checker for prose words within document text, comments etc." + +public option spell_checker_language : string = "en" + -- "language for spell-checker locale and dictionary (en, de, fr)" + +public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment" + -- "relevant markup elements for spell-checker, separated by commas" + + section "Rendering of Document Content" option outdated_color : string = "EEE3E3FF" @@ -68,6 +80,7 @@ option tracing_message_color : string = "F0F8FFFF" option warning_message_color : string = "EEE8AAFF" option error_message_color : string = "FFC1C1FF" +option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" option quoted_color : string = "8B8B8B19" diff -r 8f1e7596deb7 -r 1afb78a93376 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sat Apr 12 21:59:30 2014 +0200 @@ -42,6 +42,7 @@ "src/sledgehammer_dockable.scala" "src/simplifier_trace_dockable.scala" "src/simplifier_trace_window.scala" + "src/spell_checker.scala" "src/symbols_dockable.scala" "src/syslog_dockable.scala" "src/text_overview.scala" diff -r 8f1e7596deb7 -r 1afb78a93376 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Sat Apr 12 21:59:30 2014 +0200 @@ -47,6 +47,28 @@ lazy val editor = new JEdit_Editor + /* spell checker */ + + private val no_spell_checker: (String, Exn.Result[Spell_Checker]) = + ("", Exn.Exn(ERROR("No spell checker"))) + + @volatile private var current_spell_checker = no_spell_checker + + def get_spell_checker: Option[Spell_Checker] = + current_spell_checker match { + case (_, Exn.Res(spell_checker)) => Some(spell_checker) + case _ => None + } + + def update_spell_checker(): Unit = + if (options.bool("spell_checker")) { + val lang = options.string("spell_checker_language") + if (current_spell_checker._1 != lang) + current_spell_checker = (lang, Exn.capture { Spell_Checker(lang) }) + } + else current_spell_checker = no_spell_checker + + /* popups */ def dismissed_popups(view: View): Boolean = @@ -330,6 +352,7 @@ } case msg: PropertiesChanged => + PIDE.update_spell_checker() PIDE.session.update_options(PIDE.options.value) case _ => @@ -348,6 +371,7 @@ PIDE.options.update(Options.init()) PIDE.completion_history.load() + PIDE.update_spell_checker() SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender) if (ModeProvider.instance.isInstanceOf[ModeProvider]) diff -r 8f1e7596deb7 -r 1afb78a93376 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Sat Apr 12 21:59:30 2014 +0200 @@ -225,6 +225,7 @@ val tracing_message_color = color_value("tracing_message_color") val warning_message_color = color_value("warning_message_color") val error_message_color = color_value("error_message_color") + val spell_checker_color = color_value("spell_checker_color") val bad_color = color_value("bad_color") val intensify_color = color_value("intensify_color") val quoted_color = color_value("quoted_color") @@ -283,6 +284,15 @@ }).headOption.map(_.info) + /* spell checker */ + + private lazy val spell_checker_elements = + Document.Elements(space_explode(',', options.string("spell_checker_elements")): _*) + + def spell_checker_ranges(range: Text.Range): List[Text.Range] = + snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range) + + /* command status overview */ def overview_limit: Int = options.int("jedit_text_overview_limit") diff -r 8f1e7596deb7 -r 1afb78a93376 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Sat Apr 12 21:59:30 2014 +0200 @@ -316,6 +316,19 @@ gfx.drawLine(x1, y1, x1 + 1, y1) } } + + // spell-checker + for { + spell_checker <- PIDE.get_spell_checker + range0 <- rendering.spell_checker_ranges(line_range) + text <- JEdit_Lib.try_get_text(buffer, range0) + range <- spell_checker.bad_words(text) + r <- JEdit_Lib.gfx_range(text_area, range + range0.start) + } { + gfx.setColor(rendering.spell_checker_color) + val y0 = r.y + fm.getAscent + 2 + gfx.drawLine(r.x, y0, r.x + r.length, y0) + } } } } diff -r 8f1e7596deb7 -r 1afb78a93376 src/Tools/jEdit/src/spell_checker.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/spell_checker.scala Sat Apr 12 21:59:30 2014 +0200 @@ -0,0 +1,117 @@ +/* Title: Tools/jEdit/src/spell_checker.scala + Author: Makarius + +Spell-checker based on JOrtho (see http://sourceforge.net/projects/jortho). +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.lang.Class +import java.net.URL +import java.util.Locale +import java.text.BreakIterator + +import scala.collection.mutable + + +object Spell_Checker +{ + def known_dictionaries: List[String] = + space_explode(',', Isabelle_System.getenv_strict("JORTHO_DICTIONARIES")) + + def apply(lang: String): Spell_Checker = + if (known_dictionaries.contains(lang)) + new Spell_Checker( + lang, Locale.forLanguageTag(lang), + classOf[com.inet.jortho.SpellChecker].getResource("dictionary_" + lang + ".ortho")) + else error("Unknown spell-checker dictionary for " + quote(lang)) + + def apply(lang: String, locale: Locale, dict: URL): Spell_Checker = + new Spell_Checker(lang, locale, dict) +} + +class Spell_Checker private(lang: String, locale: Locale, dict: URL) +{ + override def toString: String = "Spell_Checker(" + lang + ")" + + private val dictionary = + { + val factory_class = Class.forName("com.inet.jortho.DictionaryFactory") + val factory_cons = factory_class.getConstructor() + factory_cons.setAccessible(true) + val factory = factory_cons.newInstance() + + val load_word_list = factory_class.getDeclaredMethod("loadWordList", classOf[URL]) + load_word_list.setAccessible(true) + load_word_list.invoke(factory, dict) + + val create = factory_class.getDeclaredMethod("create") + create.setAccessible(true) + create.invoke(factory) + } + + def load(file_name: String) + { + val m = dictionary.getClass.getDeclaredMethod("load", classOf[String]) + m.setAccessible(true) + m.invoke(dictionary, file_name) + } + + def save(file_name: String) + { + val m = dictionary.getClass.getDeclaredMethod("save", classOf[String]) + m.setAccessible(true) + m.invoke(dictionary, file_name) + } + + def add(word: String) + { + val m = dictionary.getClass.getDeclaredMethod("add", classOf[String]) + m.setAccessible(true) + m.invoke(dictionary, word) + } + + def contains(word: String): Boolean = + { + val m = dictionary.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String]) + m.setAccessible(true) + m.invoke(dictionary, word).asInstanceOf[java.lang.Boolean].booleanValue + } + + def check(word: String): Boolean = + contains(word) || + Library.is_all_caps(word) && contains(Library.lowercase(word, locale)) || + Library.is_capitalized(word) && + (contains(Library.lowercase(word, locale)) || contains(Library.uppercase(word, locale))) + + def complete(word: String): List[String] = + { + val m = dictionary.getClass.getSuperclass. + getDeclaredMethod("searchSuggestions", classOf[String]) + m.setAccessible(true) + m.invoke(dictionary, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString) + } + + def bad_words(text: String): List[Text.Range] = + { + val result = new mutable.ListBuffer[Text.Range] + + val it = BreakIterator.getWordInstance(locale) + it.setText(text) + + var i = 0 + var j = it.next + while (j != BreakIterator.DONE) { + val word = text.substring(i, j) + if (word.length >= 2 && Character.isLetter(word(0)) && !check(word)) + result += Text.Range(i, j) + i = j + j = it.next + } + result.toList + } +} + diff -r 8f1e7596deb7 -r 1afb78a93376 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 12 11:27:36 2014 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Sat Apr 12 21:59:30 2014 +0200 @@ -85,7 +85,7 @@ } reactions += { case ValueChanged(`search`) => delay_search.invoke() } }, "Search Symbols") - pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") ) + pages.map(p => p.title = space_explode('_', p.title).map(Library.capitalize(_)).mkString(" ")) } set_content(group_tabs) }