# HG changeset patch # User wenzelm # Date 1488912782 -3600 # Node ID a1aaa18091b0f58d132fbc61ca9e19593b006fc7 # Parent 115bcddf2ea21d2b6b9756d6d1191c8eaaa7d6c8# Parent 69ea3f1715be6ad754bc1b230f44d4abc75c08d9 merged diff -r 115bcddf2ea2 -r a1aaa18091b0 etc/options --- a/etc/options Tue Mar 07 16:22:17 2017 +0100 +++ b/etc/options Tue Mar 07 19:53:02 2017 +0100 @@ -193,6 +193,18 @@ -- "limit for completion within the formal context" +section "Spell Checker" + +public option spell_checker : bool = true + -- "enable spell-checker for prose words within document text, comments etc." + +public option spell_checker_dictionary : string = "en" + -- "spell-checker dictionary name" + +public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment" + -- "relevant markup elements for spell-checker, separated by commas" + + section "Secure Shell" option ssh_config_dir : string = "~/.ssh" diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Tue Mar 07 19:53:02 2017 +0100 @@ -26,12 +26,12 @@ val markdown_item2 = Value("markdown_item2") val markdown_item3 = Value("markdown_item3") val markdown_item4 = Value("markdown_item4") - val background = values + val background_colors = values // foreground val quoted = Value("quoted") val antiquoted = Value("antiquoted") - val foreground = values -- background + val foreground_colors = values -- background_colors // message underline val writeln = Value("writeln") @@ -39,7 +39,7 @@ val warning = Value("warning") val legacy = Value("legacy") val error = Value("error") - val message_underline = values -- background -- foreground + val message_underline_colors = values -- background_colors -- foreground_colors // message background val writeln_message = Value("writeln_message") @@ -48,7 +48,33 @@ val warning_message = Value("warning_message") val legacy_message = Value("legacy_message") val error_message = Value("error_message") - val message_background = values -- background -- foreground -- message_underline + val message_background_colors = + values -- background_colors -- foreground_colors -- message_underline_colors + + // text + val main = Value("main") + val keyword1 = Value("keyword1") + val keyword2 = Value("keyword2") + val keyword3 = Value("keyword3") + val quasi_keyword = Value("quasi_keyword") + val improper = Value("improper") + val operator = Value("operator") + val tfree = Value("tfree") + val tvar = Value("tvar") + val free = Value("free") + val skolem = Value("skolem") + val bound = Value("bound") + val var_ = Value("var") + val inner_numeral = Value("inner_numeral") + val inner_quoted = Value("inner_quoted") + val inner_cartouche = Value("inner_cartouche") + val inner_comment = Value("inner_comment") + val dynamic = Value("dynamic") + val class_parameter = Value("class_parameter") + val antiquote = Value("antiquote") + val text_colors = + values -- background_colors -- foreground_colors -- message_underline_colors -- + message_background_colors } @@ -95,6 +121,45 @@ error_pri -> Color.error_message) + /* text color */ + + val text_color = Map( + Markup.KEYWORD1 -> Color.keyword1, + Markup.KEYWORD2 -> Color.keyword2, + Markup.KEYWORD3 -> Color.keyword3, + Markup.QUASI_KEYWORD -> Color.quasi_keyword, + Markup.IMPROPER -> Color.improper, + Markup.OPERATOR -> Color.operator, + Markup.STRING -> Color.main, + Markup.ALT_STRING -> Color.main, + Markup.VERBATIM -> Color.main, + Markup.CARTOUCHE -> Color.main, + Markup.LITERAL -> Color.keyword1, + Markup.DELIMITER -> Color.main, + Markup.TFREE -> Color.tfree, + Markup.TVAR -> Color.tvar, + Markup.FREE -> Color.free, + Markup.SKOLEM -> Color.skolem, + Markup.BOUND -> Color.bound, + Markup.VAR -> Color.var_, + Markup.INNER_STRING -> Color.inner_quoted, + Markup.INNER_CARTOUCHE -> Color.inner_cartouche, + Markup.INNER_COMMENT -> Color.inner_comment, + Markup.DYNAMIC_FACT -> Color.dynamic, + Markup.CLASS_PARAMETER -> Color.class_parameter, + Markup.ANTIQUOTE -> Color.antiquote, + Markup.ML_KEYWORD1 -> Color.keyword1, + Markup.ML_KEYWORD2 -> Color.keyword2, + Markup.ML_KEYWORD3 -> Color.keyword3, + Markup.ML_DELIMITER -> Color.main, + Markup.ML_NUMERAL -> Color.inner_numeral, + Markup.ML_CHAR -> Color.inner_quoted, + Markup.ML_STRING -> Color.inner_quoted, + Markup.ML_COMMENT -> Color.inner_comment, + Markup.SML_STRING -> Color.inner_quoted, + Markup.SML_COMMENT -> Color.inner_comment) + + /* markup elements */ val active_elements = @@ -141,6 +206,8 @@ Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body) val caret_focus_elements = Markup.Elements(Markup.ENTITY) + + val text_color_elements = Markup.Elements(text_color.keySet) } abstract class Rendering( @@ -169,6 +236,21 @@ } + /* spell checker */ + + private lazy val spell_checker_elements = + Markup.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) + + def spell_checker_point(range: Text.Range): Option[Text.Range] = + snapshot.select(range, spell_checker_elements, _ => + { + case info => Some(snapshot.convert(info.range)) + }).headOption.map(_.info) + + /* tooltips */ def timing_threshold: Double diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Pure/System/isabelle_tool.scala Tue Mar 07 19:53:02 2017 +0100 @@ -117,9 +117,9 @@ Update_Header.isabelle_tool, Update_Then.isabelle_tool, Update_Theorems.isabelle_tool, + isabelle.vscode.Build_VSCode.isabelle_tool, isabelle.vscode.Grammar.isabelle_tool, - isabelle.vscode.Server.isabelle_tool, - isabelle.vscode.Symbols.isabelle_tool) + isabelle.vscode.Server.isabelle_tool) private def list_internal(): List[(String, String)] = for (tool <- internal_tools.toList if tool.accessible) diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Pure/Tools/spell_checker.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/spell_checker.scala Tue Mar 07 19:53:02 2017 +0100 @@ -0,0 +1,272 @@ +/* Title: Tools/jEdit/src/spell_checker.scala + Author: Makarius + +Spell checker with completion, based on JOrtho (see +http://sourceforge.net/projects/jortho). +*/ + +package isabelle + + +import java.lang.Class + +import scala.collection.mutable +import scala.annotation.tailrec +import scala.collection.immutable.SortedMap + + +object Spell_Checker +{ + /* words within text */ + + def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean) + : List[Text.Info[String]] = + { + val result = new mutable.ListBuffer[Text.Info[String]] + var offset = 0 + + def apostrophe(c: Int): Boolean = + c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'') + + @tailrec def scan(pred: Int => Boolean) + { + if (offset < text.length) { + val c = text.codePointAt(offset) + if (pred(c)) { + offset += Character.charCount(c) + scan(pred) + } + } + } + + while (offset < text.length) { + scan(c => !Character.isLetter(c)) + val start = offset + scan(c => Character.isLetterOrDigit(c) || apostrophe(c)) + val stop = offset + if (stop - start >= 2) { + val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop)) + if (mark(info)) result += info + } + } + result.toList + } + + + /* dictionaries */ + + class Dictionary private[Spell_Checker](val path: Path) + { + val lang = path.split_ext._1.base.implode + val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang) + override def toString: String = lang + } + + private object Decl + { + def apply(name: String, include: Boolean): String = + if (include) name else "-" + name + + def unapply(decl: String): Option[(String, Boolean)] = + { + val decl1 = decl.trim + if (decl1 == "" || decl1.startsWith("#")) None + else + Library.try_unprefix("-", decl1.trim) match { + case None => Some((decl1, true)) + case Some(decl2) => Some((decl2, false)) + } + } + } + + def dictionaries(): List[Dictionary] = + for { + path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES")) + if path.is_file + } yield new Dictionary(path) + + + /* create spell checker */ + + def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary) + + private sealed case class Update(include: Boolean, permanent: Boolean) +} + + +class Spell_Checker private(dictionary: Spell_Checker.Dictionary) +{ + override def toString: String = dictionary.toString + + + /* main dictionary content */ + + private var dict = new Object + private var updates = SortedMap.empty[String, Spell_Checker.Update] + + private def included_iterator(): Iterator[String] = + for { + (word, upd) <- updates.iterator + if upd.include + } yield word + + private def excluded(word: String): Boolean = + updates.get(word) match { + case Some(upd) => !upd.include + case None => false + } + + private def load() + { + val main_dictionary = split_lines(File.read_gzip(dictionary.path)) + + val permanent_updates = + if (dictionary.user_path.is_file) + for { + Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path)) + } yield (word, Spell_Checker.Update(include, true)) + else Nil + + updates = + updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++ + permanent_updates + + 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 add = Untyped.method(factory_class, "add", classOf[String]) + + for { + word <- main_dictionary.iterator ++ included_iterator() + if !excluded(word) + } add.invoke(factory, word) + + dict = Untyped.method(factory_class, "create").invoke(factory) + } + load() + + private def save() + { + val permanent_decls = + (for { + (word, upd) <- updates.iterator + if upd.permanent + } yield Spell_Checker.Decl(word, upd.include)).toList + + if (permanent_decls.nonEmpty || dictionary.user_path.is_file) { + val header = """# User updates for spell-checker dictionary +# +# * each line contains at most one word +# * extra blanks are ignored +# * lines starting with "#" are stripped +# * lines starting with "-" indicate excluded words +# +#:mode=text:encoding=UTF-8: + +""" + Isabelle_System.mkdirs(dictionary.user_path.expand.dir) + File.write(dictionary.user_path, header + cat_lines(permanent_decls)) + } + } + + def update(word: String, include: Boolean, permanent: Boolean) + { + updates += (word -> Spell_Checker.Update(include, permanent)) + + if (include) { + if (permanent) save() + Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word) + } + else { save(); load() } + } + + def reset() + { + updates = SortedMap.empty + load() + } + + def reset_enabled(): Int = + updates.valuesIterator.filter(upd => !upd.permanent).length + + + /* check known words */ + + def contains(word: String): Boolean = + Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]). + invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue + + def check(word: String): Boolean = + word match { + case Word.Case(c) if c != Word.Lowercase => + contains(word) || contains(Word.lowercase(word)) + case _ => + contains(word) + } + + def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] = + Spell_Checker.marked_words(base, text, info => !check(info.info)) + + + /* suggestions for unknown words */ + + private def suggestions(word: String): Option[List[String]] = + { + val res = + Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]). + invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString) + if (res.isEmpty) None else Some(res) + } + + def complete(word: String): List[String] = + if (check(word)) Nil + else { + val word_case = Word.Case.unapply(word) + def recover_case(s: String) = + word_case match { + case Some(c) => Word.Case(c, s) + case None => s + } + val result = + word_case match { + case Some(c) if c != Word.Lowercase => + suggestions(word) orElse suggestions(Word.lowercase(word)) + case _ => + suggestions(word) + } + result.getOrElse(Nil).map(recover_case) + } + + def complete_enabled(word: String): Boolean = complete(word).nonEmpty +} + + +class Spell_Checker_Variable +{ + private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None) + private var current_spell_checker = no_spell_checker + + def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 } + + def update(options: Options): Unit = synchronized { + if (options.bool("spell_checker")) { + val lang = options.string("spell_checker_dictionary") + if (current_spell_checker._1 != lang) { + Spell_Checker.dictionaries.find(_.lang == lang) match { + case Some(dictionary) => + val spell_checker = + Exn.capture { Spell_Checker(dictionary) } match { + case Exn.Res(spell_checker) => Some(spell_checker) + case Exn.Exn(_) => None + } + current_spell_checker = (lang, spell_checker) + case None => + current_spell_checker = no_spell_checker + } + } + } + else current_spell_checker = no_spell_checker + } +} diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Pure/build-jars --- a/src/Pure/build-jars Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Pure/build-jars Tue Mar 07 19:53:02 2017 +0100 @@ -139,6 +139,7 @@ Tools/print_operation.scala Tools/profiling_report.scala Tools/simplifier_trace.scala + Tools/spell_checker.scala Tools/task_statistics.scala Tools/update_cartouches.scala Tools/update_header.scala @@ -160,12 +161,12 @@ ../Tools/Graphview/popups.scala ../Tools/Graphview/shapes.scala ../Tools/Graphview/tree_panel.scala + ../Tools/VSCode/src/build_vscode.scala ../Tools/VSCode/src/channel.scala ../Tools/VSCode/src/document_model.scala ../Tools/VSCode/src/grammar.scala ../Tools/VSCode/src/protocol.scala ../Tools/VSCode/src/server.scala - ../Tools/VSCode/src/symbols.scala ../Tools/VSCode/src/vscode_rendering.scala ../Tools/VSCode/src/vscode_resources.scala ) diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/README.md --- a/src/Tools/VSCode/README.md Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/README.md Tue Mar 07 19:53:02 2017 +0100 @@ -25,13 +25,9 @@ ## Build ## -* shell> `cd src/Tools/VSCode/extension` - -* shell> `isabelle vscode_grammar` +* shell> `isabelle build_vscode` -* shell> `isabelle vscode_symbols` - -* shell> `vsce package` +* Extensions / ... / Install from VSIX: src/Tools/VSCode/extension/isabelle-X.Y.Z.vsix ## Relevant links ## diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/etc/options --- a/src/Tools/VSCode/etc/options Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/etc/options Tue Mar 07 19:53:02 2017 +0100 @@ -18,5 +18,8 @@ option vscode_timing_threshold : real = 0.1 -- "default threshold for timing display (seconds)" +option vscode_pide_extensions : bool = false + -- "use PIDE extensions for Language Server Protocol" + option vscode_unicode_symbols : bool = false -- "output Isabelle symbols via Unicode (according to etc/symbols)" diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/extension/README.md --- a/src/Tools/VSCode/extension/README.md Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/extension/README.md Tue Mar 07 19:53:02 2017 +0100 @@ -28,5 +28,5 @@ Symbols Mode. It needs to be configured manually as follows: $ISABELLE_HOME/src/Tools/VSCode/extension/isabelle-symbols.json contains a -configuration (generated via `isabelle vscode_symbols`). Its content needs to +configuration (generated via `isabelle build_vscode`). Its content needs to be copied carefully into the regular VSCode User Preferences. diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/extension/package.json Tue Mar 07 19:53:02 2017 +0100 @@ -99,7 +99,47 @@ "isabelle.information_light_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }, "isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" }, "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }, - "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" } + "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" }, + "isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" }, + "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" }, + "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" }, + "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(0, 102, 153, 1.00)" }, + "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" }, + "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(0, 153, 102, 1.00)" }, + "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" }, + "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(0, 153, 255, 1.00)" }, + "isabelle.quasi_keyword_light_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" }, + "isabelle.quasi_keyword_dark_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" }, + "isabelle.improper_light_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" }, + "isabelle.improper_dark_color": { "type": "string", "default": "rgba(255, 80, 80, 1.00)" }, + "isabelle.operator_light_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" }, + "isabelle.operator_dark_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" }, + "isabelle.tfree_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, + "isabelle.tfree_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, + "isabelle.tvar_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, + "isabelle.tvar_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" }, + "isabelle.free_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" }, + "isabelle.free_dark_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" }, + "isabelle.skolem_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, + "isabelle.skolem_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, + "isabelle.bound_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, + "isabelle.bound_dark_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" }, + "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" }, + "isabelle.var_dark_color": { "type": "string", "default": "rgba(0, 0, 155, 1.00)" }, + "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" }, + "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(255, 0, 0, 1.00)" }, + "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" }, + "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(255, 0, 204, 1.00)" }, + "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" }, + "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(204, 102, 0, 1.00)" }, + "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" }, + "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(204, 0, 0, 1.00)" }, + "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" }, + "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(123, 164, 40, 1.00)" }, + "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, + "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" }, + "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" }, + "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" } } } }, diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/extension/src/decorations.ts --- a/src/Tools/VSCode/extension/src/decorations.ts Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/extension/src/decorations.ts Tue Mar 07 19:53:02 2017 +0100 @@ -36,6 +36,28 @@ "warning" ] +const text_colors = [ + "keyword1", + "keyword2", + "keyword3", + "quasi_keyword", + "improper", + "operator", + "tfree", + "tvar", + "free", + "skolem", + "bound", + "var", + "inner_numeral", + "inner_quoted", + "inner_cartouche", + "inner_comment", + "dynamic", + "class_parameter", + "antiquote" +] + function get_color(color: string, light: boolean): string { const config = color.concat(light ? "_light" : "_dark").concat("_color") @@ -58,9 +80,16 @@ dark: { backgroundColor: get_color(color, false) } }) } - function dotted(color: string): TextEditorDecorationType + function text_color(color: string): TextEditorDecorationType { - const border = "2px none; border-bottom-style: dotted; border-color: " + return decoration( + { light: { color: get_color(color, true) }, + dark: { color: get_color(color, false) } }) + } + + function bottom_border(width: string, style: string, color: string): TextEditorDecorationType + { + const border = `${width} none; border-bottom-style: ${style}; border-color: ` return decoration( { light: { border: border.concat(get_color(color, true)) }, dark: { border: border.concat(get_color(color, false)) } }) @@ -74,8 +103,12 @@ types["foreground_".concat(color)] = background(color) // approximation } for (let color of dotted_colors) { - types["dotted_".concat(color)] = dotted(color) + types["dotted_".concat(color)] = bottom_border("2px", "dotted", color) } + for (let color of text_colors) { + types["text_".concat(color)] = text_color(color) + } + types["spell_checker"] = bottom_border("1px", "solid", "spell_checker") } diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Tue Mar 07 19:53:02 2017 +0100 @@ -23,7 +23,7 @@ vscode.window.showErrorMessage("Missing user settings: isabelle.home") else { let isabelle_tool = isabelle_home.concat("/bin/isabelle") - let standard_args = ["-o", "vscode_unicode_symbols"] + let standard_args = ["-o", "vscode_unicode_symbols", "-o", "vscode_pide_extensions"] let run = is_windows ? { command: cygwin_root.concat("/bin/bash"), diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/src/build_vscode.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/build_vscode.scala Tue Mar 07 19:53:02 2017 +0100 @@ -0,0 +1,103 @@ +/* Title: Pure/Admin/build_vscode.scala + Author: Makarius + +Build VSCode configuration and extension module for Isabelle. +*/ + +package isabelle.vscode + + +import isabelle._ + + +object Build_VSCode +{ + val extension_dir = Path.explode("~~/src/Tools/VSCode/extension") + + + /* Prettify Symbols Mode */ + + def prettify_config: String = + """{ + "prettifySymbolsMode.substitutions": [ + { + "language": "isabelle", + "revealOn": "none", + "adjustCursorMovement": true, + "substitutions": [""" + + (for ((s, c) <- Symbol.codes) + yield + JSON.Format( + Map("ugly" -> Library.escape_regex(s), + "pretty" -> Library.escape_regex(Codepoint.string(c))))) + .mkString("\n ", ",\n ", "") + + """] + } + ] +}""" + + def build_symbols(progress: Progress = No_Progress) + { + val output_path = extension_dir + Path.explode("isabelle-symbols.json") + progress.echo(output_path.implode) + File.write_backup(output_path, prettify_config) + } + + + /* grammar */ + + def build_grammar(options: Options, progress: Progress = No_Progress) + { + val logic = Grammar.default_logic + val keywords = Build.outer_syntax(options, Nil, logic).keywords + + val output_path = extension_dir + Path.explode(Grammar.default_output(logic)) + progress.echo(output_path.implode) + File.write_backup(output_path, Grammar.generate(keywords)) + } + + + /* extension */ + + def build_extension(progress: Progress = No_Progress, publish: Boolean = false) + { + val output_path = extension_dir + Path.explode("out") + progress.echo(output_path.implode) + + val cmd = "vsce " + (if (publish) "publish" else "package") + progress.bash(cmd, cwd = extension_dir.file, echo = true).check + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("build_vscode", "build Isabelle/VSCode extension module", args => + { + var publish = false + + val getopts = Getopts(""" +Usage: isabelle build_vscode + + Options are: + -P publish the package + +Build Isabelle/VSCode extension module in directory +""" + extension_dir.expand + """ + +This requires npm and the vsce build and publishing tool, see also +https://code.visualstudio.com/docs/tools/vscecli +""", + "P" -> (_ => publish = true)) + + val more_args = getopts(args) + if (more_args.nonEmpty) getopts.usage() + + val options = Options.init() + val progress = new Console_Progress() + + build_symbols(progress) + build_grammar(options, progress) + build_extension(progress, publish = publish) + }, admin = true) +} diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Tue Mar 07 19:53:02 2017 +0100 @@ -16,6 +16,13 @@ { /* decorations */ + object Decoration + { + def empty(typ: String): Decoration = Decoration(typ, Nil) + + def ranges(typ: String, ranges: List[Text.Range]): Decoration = + Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body]))) + } sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]]) @@ -127,7 +134,7 @@ val diagnostics = rendering.diagnostics val decorations = if (node_visible) rendering.decorations - else { for (deco <- published_decorations) yield Document_Model.Decoration(deco.typ, Nil) } + else { for (deco <- published_decorations) yield Document_Model.Decoration.empty(deco.typ) } val changed_diagnostics = if (diagnostics == published_diagnostics) None else Some(diagnostics) diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/src/grammar.scala --- a/src/Tools/VSCode/src/grammar.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/src/grammar.scala Tue Mar 07 19:53:02 2017 +0100 @@ -16,9 +16,9 @@ { /* generate grammar */ - private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") + lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") - private def default_output(logic: String = ""): String = + def default_output(logic: String = ""): String = if (logic == "" || logic == default_logic) "isabelle-grammar.json" else "isabelle-" + logic + "-grammar.json" diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/src/symbols.scala --- a/src/Tools/VSCode/src/symbols.scala Tue Mar 07 16:22:17 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,55 +0,0 @@ -/* Title: Tools/VSCode/src/symbols.scala - Author: Makarius - -Generate configuration for VSCode editor extension Prettify Symbols Mode. -*/ - -package isabelle.vscode - - -import isabelle._ - - -object Symbols -{ - /* generate configuration */ - - def prettify_config: String = - """{ - "prettifySymbolsMode.substitutions": [ - { - "language": "isabelle", - "revealOn": "none", - "adjustCursorMovement": true, - "substitutions": [""" + - (for ((s, c) <- Symbol.codes) - yield - JSON.Format( - Map("ugly" -> Library.escape_regex(s), - "pretty" -> Library.escape_regex(Codepoint.string(c))))) - .mkString("\n ", ",\n ", "") + - """] - } - ] -}""" - - - /* Isabelle tool wrapper */ - - val isabelle_tool = Isabelle_Tool("vscode_symbols", - "generate configuration for VSCode Prettify Symbols Mode", args => - { - val getopts = Getopts(""" -Usage: isabelle vscode_symbols - - Generate configuration for VSCode editor extension Prettify Symbols Mode. -""") - - val more_args = getopts(args) - if (more_args.nonEmpty) getopts.usage() - - val output_path = Path.explode("isabelle-symbols.json") - Output.writeln(output_path.implode) - File.write_backup(output_path, prettify_config) - }) -} diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Tue Mar 07 19:53:02 2017 +0100 @@ -25,8 +25,7 @@ case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil))) } types.toList.map(c => - Document_Model.Decoration(prefix + c.toString, - color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: List[XML.Body])))) + Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse)) } private val dotted_colors = @@ -71,7 +70,7 @@ model.content.try_get_text(complete_range) match { case Some(original) => names.complete(complete_range, Completion.History.empty, - resources.decode_text, original) match { + resources.unicode_symbols, original) match { case Some(result) => result.items.map(item => Protocol.CompletionItem( @@ -112,21 +111,50 @@ } + /* text color */ + + def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = + { + snapshot.select(range, Rendering.text_color_elements, _ => + { + case Text.Info(_, elem) => Rendering.text_color.get(elem.name) + }) + } + + /* dotted underline */ def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] = message_underline_color(VSCode_Rendering.dotted_elements, range) + /* spell checker */ + + def spell_checker: Document_Model.Decoration = + { + val ranges = + (for { + spell_checker <- resources.spell_checker.get.iterator + spell_range <- spell_checker_ranges(model.content.text_range).iterator + text <- model.content.try_get_text(spell_range).iterator + info <- spell_checker.marked_words(spell_range.start, text).iterator + } yield info.range).toList + Document_Model.Decoration.ranges("spell_checker", ranges) + } + + /* decorations */ def decorations: List[Document_Model.Decoration] = // list of canonical length and order - VSCode_Rendering.color_decorations("background_", Rendering.Color.background, + VSCode_Rendering.color_decorations("background_", Rendering.Color.background_colors, background(model.content.text_range, Set.empty)) ::: - VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground, + VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors, foreground(model.content.text_range)) ::: + VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors, + text_color(model.content.text_range)) ::: VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors, - dotted(model.content.text_range)) + dotted(model.content.text_range)) ::: + List(spell_checker) def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration = { diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Tue Mar 07 19:53:02 2017 +0100 @@ -47,6 +47,14 @@ private val state = Synchronized(VSCode_Resources.State()) + /* options */ + + def pide_extensions: Boolean = options.bool("vscode_pide_extensions") + def unicode_symbols: Boolean = options.bool("vscode_unicode_symbols") + def tooltip_margin: Int = options.int("vscode_tooltip_margin") + def message_margin: Int = options.int("vscode_message_margin") + + /* document node name */ def node_file(name: Document.Node.Name): JFile = new JFile(name.node) @@ -238,8 +246,10 @@ yield { for (diags <- changed_diags) channel.write(Protocol.PublishDiagnostics(file, rendering.diagnostics_output(diags))) - for (decos <- changed_decos; deco <- decos) - channel.write(rendering.decoration_output(deco).json(file)) + if (pide_extensions) { + for (decos <- changed_decos; deco <- decos) + channel.write(rendering.decoration_output(deco).json(file)) + } (file, model1) } st.copy( @@ -252,12 +262,8 @@ /* output text */ - def decode_text: Boolean = options.bool("vscode_unicode_symbols") - def tooltip_margin: Int = options.int("vscode_tooltip_margin") - def message_margin: Int = options.int("vscode_message_margin") - def output_text(s: String): String = - if (decode_text) Symbol.decode(s) else Symbol.encode(s) + if (unicode_symbols) Symbol.decode(s) else Symbol.encode(s) def output_xml(xml: XML.Tree): String = output_text(XML.content(xml)) @@ -266,4 +272,10 @@ output_text(Pretty.string_of(body, margin)) def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) + + + /* spell checker */ + + val spell_checker = new Spell_Checker_Variable + spell_checker.update(options) } diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/jEdit/etc/options Tue Mar 07 19:53:02 2017 +0100 @@ -73,18 +73,6 @@ -- "glob patterns to ignore in file-system path completion (separated by colons)" -section "Spell Checker" - -public option spell_checker : bool = true - -- "enable spell-checker for prose words within document text, comments etc." - -public option spell_checker_dictionary : string = "en" - -- "spell-checker dictionary name" - -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" diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue Mar 07 19:53:02 2017 +0100 @@ -43,6 +43,7 @@ "src/jedit_rendering.scala" "src/jedit_resources.scala" "src/jedit_sessions.scala" + "src/jedit_spell_checker.scala" "src/keymap_merge.scala" "src/monitor_dockable.scala" "src/output_dockable.scala" @@ -60,7 +61,6 @@ "src/simplifier_trace_dockable.scala" "src/simplifier_trace_window.scala" "src/sledgehammer_dockable.scala" - "src/spell_checker.scala" "src/state_dockable.scala" "src/symbols_dockable.scala" "src/syslog_dockable.scala" diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Tue Mar 07 19:53:02 2017 +0100 @@ -381,7 +381,7 @@ case Some(rendering) => Completion.Result.merge(history, result1, Completion.Result.merge(history, - Spell_Checker.completion(text_area, explicit, rendering), + JEdit_Spell_Checker.completion(text_area, explicit, rendering), Completion.Result.merge(history, path_completion(rendering), Bibtex_JEdit.completion(history, text_area, rendering)))) diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/src/context_menu.scala --- a/src/Tools/jEdit/src/context_menu.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/jEdit/src/context_menu.scala Tue Mar 07 19:53:02 2017 +0100 @@ -29,7 +29,7 @@ if (evt != null && evt.getSource == text_area.getPainter) { val offset = text_area.xyToOffset(evt.getX, evt.getY) if (offset >= 0) - Spell_Checker.context_menu(text_area, offset) ::: + JEdit_Spell_Checker.context_menu(text_area, offset) ::: Debugger_Dockable.context_menu(text_area, offset) else Nil } diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Mar 07 19:53:02 2017 +0100 @@ -419,7 +419,7 @@ doc_view <- Document_View.get(text_area) rendering = doc_view.get_rendering() range = JEdit_Lib.caret_range(text_area) - Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range) + Text.Info(_, word) <- JEdit_Spell_Checker.current_word(text_area, rendering, range) } { spell_checker.update(word, include, permanent) JEdit_Lib.jedit_views().foreach(_.repaint()) diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Mar 07 19:53:02 2017 +0100 @@ -42,7 +42,7 @@ val options = PIDE.options private val predefined = - List(JEdit_Sessions.logic_selector(false), Spell_Checker.dictionaries_selector()) + List(JEdit_Sessions.logic_selector(false), JEdit_Spell_Checker.dictionaries_selector()) protected val components = options.make_components(predefined, diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Mar 07 16:22:17 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Mar 07 19:53:02 2017 +0100 @@ -162,12 +162,16 @@ { /* colors */ - def color(s: String): Color = Color_Value(options.string(s)) + def color(s: String): Color = + if (s == "main_color") main_color + else Color_Value(options.string(s)) + + def color(c: Rendering.Color.Value): Color = _rendering_colors(c) lazy val _rendering_colors: Map[Rendering.Color.Value, Color] = Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap - def color(c: Rendering.Color.Value): Color = _rendering_colors(c) + val main_color = jEdit.getColorProperty("view.fgColor") val outdated_color = color("outdated_color") val unprocessed_color = color("unprocessed_color") @@ -181,33 +185,13 @@ val breakpoint_disabled_color = color("breakpoint_disabled_color") val breakpoint_enabled_color = color("breakpoint_enabled_color") val caret_debugger_color = color("caret_debugger_color") - val antiquote_color = color("antiquote_color") val highlight_color = color("highlight_color") val hyperlink_color = color("hyperlink_color") val active_hover_color = color("active_hover_color") - val keyword1_color = color("keyword1_color") - val keyword2_color = color("keyword2_color") - val keyword3_color = color("keyword3_color") - val quasi_keyword_color = color("quasi_keyword_color") - val improper_color = color("improper_color") - val operator_color = color("operator_color") val caret_invisible_color = color("caret_invisible_color") val completion_color = color("completion_color") val search_color = color("search_color") - val tfree_color = color("tfree_color") - val tvar_color = color("tvar_color") - val free_color = color("free_color") - val skolem_color = color("skolem_color") - val bound_color = color("bound_color") - val var_color = color("var_color") - val inner_numeral_color = color("inner_numeral_color") - val inner_quoted_color = color("inner_quoted_color") - val inner_cartouche_color = color("inner_cartouche_color") - val inner_comment_color = color("inner_comment_color") - val dynamic_color = color("dynamic_color") - val class_parameter_color = color("class_parameter_color") - /* indentation */ @@ -251,21 +235,6 @@ }).headOption.map(_.info) - /* spell checker */ - - private lazy val spell_checker_elements = - Markup.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) - - def spell_checker_point(range: Text.Range): Option[Text.Range] = - snapshot.select(range, spell_checker_elements, _ => - { - case info => Some(snapshot.convert(info.range)) - }).headOption.map(_.info) - - /* breakpoints */ def breakpoint(range: Text.Range): Option[(Command, Long)] = @@ -478,54 +447,13 @@ /* text color */ - val foreground_color = jEdit.getColorProperty("view.fgColor") - - private lazy val text_colors: Map[String, Color] = Map( - Markup.KEYWORD1 -> keyword1_color, - Markup.KEYWORD2 -> keyword2_color, - Markup.KEYWORD3 -> keyword3_color, - Markup.QUASI_KEYWORD -> quasi_keyword_color, - Markup.IMPROPER -> improper_color, - Markup.OPERATOR -> operator_color, - Markup.STRING -> foreground_color, - Markup.ALT_STRING -> foreground_color, - Markup.VERBATIM -> foreground_color, - Markup.CARTOUCHE -> foreground_color, - Markup.LITERAL -> keyword1_color, - Markup.DELIMITER -> foreground_color, - Markup.TFREE -> tfree_color, - Markup.TVAR -> tvar_color, - Markup.FREE -> free_color, - Markup.SKOLEM -> skolem_color, - Markup.BOUND -> bound_color, - Markup.VAR -> var_color, - Markup.INNER_STRING -> inner_quoted_color, - Markup.INNER_CARTOUCHE -> inner_cartouche_color, - Markup.INNER_COMMENT -> inner_comment_color, - Markup.DYNAMIC_FACT -> dynamic_color, - Markup.CLASS_PARAMETER -> class_parameter_color, - Markup.ANTIQUOTE -> antiquote_color, - Markup.ML_KEYWORD1 -> keyword1_color, - Markup.ML_KEYWORD2 -> keyword2_color, - Markup.ML_KEYWORD3 -> keyword3_color, - Markup.ML_DELIMITER -> foreground_color, - Markup.ML_NUMERAL -> inner_numeral_color, - Markup.ML_CHAR -> inner_quoted_color, - Markup.ML_STRING -> inner_quoted_color, - Markup.ML_COMMENT -> inner_comment_color, - Markup.SML_STRING -> inner_quoted_color, - Markup.SML_COMMENT -> inner_comment_color) - - private lazy val text_color_elements = - Markup.Elements(text_colors.keySet) - - def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] = + def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] = { - if (color == Token_Markup.hidden_color) List(Text.Info(range, color)) + if (current_color == Token_Markup.hidden_color) List(Text.Info(range, current_color)) else - snapshot.cumulate(range, color, text_color_elements, _ => + snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ => { - case (_, Text.Info(_, elem)) => text_colors.get(elem.name) + case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color(_)) }) } diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/src/jedit_spell_checker.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Tue Mar 07 19:53:02 2017 +0100 @@ -0,0 +1,129 @@ +/* Title: Tools/jEdit/src/jedit_spell_checker.scala + Author: Makarius + +Specific spell-checker support for Isabelle/jEdit. +*/ + +package isabelle.jedit + + +import isabelle._ + +import javax.swing.JMenuItem +import scala.swing.ComboBox + +import org.gjt.sp.jedit.menu.EnhancedMenuItem +import org.gjt.sp.jedit.jEdit +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} + + +object JEdit_Spell_Checker +{ + /* words within text */ + + def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range) + : Option[Text.Info[String]] = + { + for { + spell_range <- rendering.spell_checker_point(range) + text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range) + info <- Spell_Checker.marked_words( + spell_range.start, text, info => info.range.overlaps(range)).headOption + } yield info + } + + + /* completion */ + + def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering) + : Option[Completion.Result] = + { + for { + spell_checker <- PIDE.spell_checker.get + if explicit + range = JEdit_Lib.before_caret_range(text_area, rendering) + word <- current_word(text_area, rendering, range) + words = spell_checker.complete(word.info) + if words.nonEmpty + descr = "(from dictionary " + quote(spell_checker.toString) + ")" + items = + words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false)) + } yield Completion.Result(word.range, word.info, false, items) + } + + + /* context menu */ + + def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = + { + val result = + for { + spell_checker <- PIDE.spell_checker.get + doc_view <- Document_View.get(text_area) + rendering = doc_view.get_rendering() + range = JEdit_Lib.point_range(text_area.getBuffer, offset) + Text.Info(_, word) <- current_word(text_area, rendering, range) + } yield (spell_checker, word) + + result match { + case Some((spell_checker, word)) => + + val context = jEdit.getActionContext() + def item(name: String): JMenuItem = + new EnhancedMenuItem(context.getAction(name).getLabel, name, context) + + val complete_items = + if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word")) + else Nil + + val update_items = + if (spell_checker.check(word)) + List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently")) + else + List(item("isabelle.include-word"), item("isabelle.include-word-permanently")) + + val reset_items = + spell_checker.reset_enabled() match { + case 0 => Nil + case n => + val name = "isabelle.reset-words" + val label = context.getAction(name).getLabel + List(new EnhancedMenuItem(label + " (" + n + ")", name, context)) + } + + complete_items ::: update_items ::: reset_items + + case None => Nil + } + } + + + /* dictionaries */ + + def dictionaries_selector(): Option_Component = + { + GUI_Thread.require {} + + val option_name = "spell_checker_dictionary" + val opt = PIDE.options.value.check_name(option_name) + + val entries = Spell_Checker.dictionaries() + val component = new ComboBox(entries) with Option_Component { + name = option_name + val title = opt.title() + def load: Unit = + { + val lang = PIDE.options.string(option_name) + entries.find(_.lang == lang) match { + case Some(entry) => selection.item = entry + case None => + } + } + def save: Unit = PIDE.options.string(option_name) = selection.item.lang + } + + component.load() + component.tooltip = GUI.tooltip_lines(opt.print_default) + component + } +} diff -r 115bcddf2ea2 -r a1aaa18091b0 src/Tools/jEdit/src/spell_checker.scala --- a/src/Tools/jEdit/src/spell_checker.scala Tue Mar 07 16:22:17 2017 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,392 +0,0 @@ -/* Title: Tools/jEdit/src/spell_checker.scala - Author: Makarius - -Spell checker with completion, based on JOrtho (see -http://sourceforge.net/projects/jortho). -*/ - -package isabelle.jedit - - -import isabelle._ - -import java.lang.Class - -import javax.swing.JMenuItem - -import scala.collection.mutable -import scala.swing.ComboBox -import scala.annotation.tailrec -import scala.collection.immutable.SortedMap - -import org.gjt.sp.jedit.menu.EnhancedMenuItem -import org.gjt.sp.jedit.{jEdit, Buffer} -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} - - -object Spell_Checker -{ - /** words within text **/ - - def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean) - : List[Text.Info[String]] = - { - val result = new mutable.ListBuffer[Text.Info[String]] - var offset = 0 - - def apostrophe(c: Int): Boolean = - c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'') - - @tailrec def scan(pred: Int => Boolean) - { - if (offset < text.length) { - val c = text.codePointAt(offset) - if (pred(c)) { - offset += Character.charCount(c) - scan(pred) - } - } - } - - while (offset < text.length) { - scan(c => !Character.isLetter(c)) - val start = offset - scan(c => Character.isLetterOrDigit(c) || apostrophe(c)) - val stop = offset - if (stop - start >= 2) { - val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop)) - if (mark(info)) result += info - } - } - result.toList - } - - def current_word(text_area: TextArea, rendering: JEdit_Rendering, range: Text.Range) - : Option[Text.Info[String]] = - { - for { - spell_range <- rendering.spell_checker_point(range) - text <- JEdit_Lib.try_get_text(text_area.getBuffer, spell_range) - info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption - } yield info - } - - - - /** completion **/ - - def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering) - : Option[Completion.Result] = - { - for { - spell_checker <- PIDE.spell_checker.get - if explicit - range = JEdit_Lib.before_caret_range(text_area, rendering) - word <- current_word(text_area, rendering, range) - words = spell_checker.complete(word.info) - if words.nonEmpty - descr = "(from dictionary " + quote(spell_checker.toString) + ")" - items = - words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false)) - } yield Completion.Result(word.range, word.info, false, items) - } - - - - /** context menu **/ - - def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = - { - val result = - for { - spell_checker <- PIDE.spell_checker.get - doc_view <- Document_View.get(text_area) - rendering = doc_view.get_rendering() - range = JEdit_Lib.point_range(text_area.getBuffer, offset) - Text.Info(_, word) <- current_word(text_area, rendering, range) - } yield (spell_checker, word) - - result match { - case Some((spell_checker, word)) => - - val context = jEdit.getActionContext() - def item(name: String): JMenuItem = - new EnhancedMenuItem(context.getAction(name).getLabel, name, context) - - val complete_items = - if (spell_checker.complete_enabled(word)) List(item("isabelle.complete-word")) - else Nil - - val update_items = - if (spell_checker.check(word)) - List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently")) - else - List(item("isabelle.include-word"), item("isabelle.include-word-permanently")) - - val reset_items = - spell_checker.reset_enabled() match { - case 0 => Nil - case n => - val name = "isabelle.reset-words" - val label = context.getAction(name).getLabel - List(new EnhancedMenuItem(label + " (" + n + ")", name, context)) - } - - complete_items ::: update_items ::: reset_items - - case None => Nil - } - } - - - - /** dictionary **/ - - /* declarations */ - - class Dictionary private[Spell_Checker](val path: Path) - { - val lang = path.split_ext._1.base.implode - val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang) - override def toString: String = lang - } - - private object Decl - { - def apply(name: String, include: Boolean): String = - if (include) name else "-" + name - - def unapply(decl: String): Option[(String, Boolean)] = - { - val decl1 = decl.trim - if (decl1 == "" || decl1.startsWith("#")) None - else - Library.try_unprefix("-", decl1.trim) match { - case None => Some((decl1, true)) - case Some(decl2) => Some((decl2, false)) - } - } - } - - - /* known dictionaries */ - - def dictionaries(): List[Dictionary] = - for { - path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES")) - if path.is_file - } yield new Dictionary(path) - - def dictionaries_selector(): Option_Component = - { - GUI_Thread.require {} - - val option_name = "spell_checker_dictionary" - val opt = PIDE.options.value.check_name(option_name) - - val entries = dictionaries() - val component = new ComboBox(entries) with Option_Component { - name = option_name - val title = opt.title() - def load: Unit = - { - val lang = PIDE.options.string(option_name) - entries.find(_.lang == lang) match { - case Some(entry) => selection.item = entry - case None => - } - } - def save: Unit = PIDE.options.string(option_name) = selection.item.lang - } - - component.load() - component.tooltip = GUI.tooltip_lines(opt.print_default) - component - } - - - /* create spell checker */ - - def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary) - - private sealed case class Update(include: Boolean, permanent: Boolean) -} - - -class Spell_Checker private(dictionary: Spell_Checker.Dictionary) -{ - override def toString: String = dictionary.toString - - - /* main dictionary content */ - - private var dict = new Object - private var updates = SortedMap.empty[String, Spell_Checker.Update] - - private def included_iterator(): Iterator[String] = - for { - (word, upd) <- updates.iterator - if upd.include - } yield word - - private def excluded(word: String): Boolean = - updates.get(word) match { - case Some(upd) => !upd.include - case None => false - } - - private def load() - { - val main_dictionary = split_lines(File.read_gzip(dictionary.path)) - - val permanent_updates = - if (dictionary.user_path.is_file) - for { - Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path)) - } yield (word, Spell_Checker.Update(include, true)) - else Nil - - updates = - updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++ - permanent_updates - - 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 add = Untyped.method(factory_class, "add", classOf[String]) - - for { - word <- main_dictionary.iterator ++ included_iterator() - if !excluded(word) - } add.invoke(factory, word) - - dict = Untyped.method(factory_class, "create").invoke(factory) - } - load() - - private def save() - { - val permanent_decls = - (for { - (word, upd) <- updates.iterator - if upd.permanent - } yield Spell_Checker.Decl(word, upd.include)).toList - - if (permanent_decls.nonEmpty || dictionary.user_path.is_file) { - val header = """# User updates for spell-checker dictionary -# -# * each line contains at most one word -# * extra blanks are ignored -# * lines starting with "#" are stripped -# * lines starting with "-" indicate excluded words -# -#:mode=text:encoding=UTF-8: - -""" - Isabelle_System.mkdirs(dictionary.user_path.expand.dir) - File.write(dictionary.user_path, header + cat_lines(permanent_decls)) - } - } - - def update(word: String, include: Boolean, permanent: Boolean) - { - updates += (word -> Spell_Checker.Update(include, permanent)) - - if (include) { - if (permanent) save() - Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word) - } - else { save(); load() } - } - - def reset() - { - updates = SortedMap.empty - load() - } - - def reset_enabled(): Int = - updates.valuesIterator.filter(upd => !upd.permanent).length - - - /* check known words */ - - def contains(word: String): Boolean = - Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]). - invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue - - def check(word: String): Boolean = - word match { - case Word.Case(c) if c != Word.Lowercase => - contains(word) || contains(Word.lowercase(word)) - case _ => - contains(word) - } - - def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] = - Spell_Checker.marked_words(base, text, info => !check(info.info)) - - - /* suggestions for unknown words */ - - private def suggestions(word: String): Option[List[String]] = - { - val res = - Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]). - invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString) - if (res.isEmpty) None else Some(res) - } - - def complete(word: String): List[String] = - if (check(word)) Nil - else { - val word_case = Word.Case.unapply(word) - def recover_case(s: String) = - word_case match { - case Some(c) => Word.Case(c, s) - case None => s - } - val result = - word_case match { - case Some(c) if c != Word.Lowercase => - suggestions(word) orElse suggestions(Word.lowercase(word)) - case _ => - suggestions(word) - } - result.getOrElse(Nil).map(recover_case) - } - - def complete_enabled(word: String): Boolean = complete(word).nonEmpty -} - - -class Spell_Checker_Variable -{ - private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None) - private var current_spell_checker = no_spell_checker - - def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 } - - def update(options: Options): Unit = synchronized { - if (options.bool("spell_checker")) { - val lang = options.string("spell_checker_dictionary") - if (current_spell_checker._1 != lang) { - Spell_Checker.dictionaries.find(_.lang == lang) match { - case Some(dictionary) => - val spell_checker = - Exn.capture { Spell_Checker(dictionary) } match { - case Exn.Res(spell_checker) => Some(spell_checker) - case Exn.Exn(_) => None - } - current_spell_checker = (lang, spell_checker) - case None => - current_spell_checker = no_spell_checker - } - } - } - else current_spell_checker = no_spell_checker - } -} -