--- 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
--- 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
--- 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.
--- 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 =
--- 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";
--- 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"
--- 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
--- 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 ()
--- 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
--- 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"
--- 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"
--- 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])
--- 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")
--- 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)
+ }
}
}
}
--- /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
+ }
+}
+
--- 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)
}