--- 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"
--- 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
--- 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)
--- /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
+ }
+}
--- 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
)
--- 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 ##
--- 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)"
--- 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.
--- 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)" }
}
}
},
--- 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")
}
--- 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"),
--- /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)
+}
--- 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)
--- 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"
--- 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)
- })
-}
--- 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 =
{
--- 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)
}
--- 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"
--- 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"
--- 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))))
--- 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
}
--- 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())
--- 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,
--- 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(_))
})
}
--- /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
+ }
+}
--- 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
- }
-}
-