# HG changeset patch
# User wenzelm
# Date 1488899202 -3600
# Node ID 368004bed323f006a35cc8d5a722283f39e4b3b8
# Parent  c706b57b16942f9e6f5e0fe611f2e40752cca719
decorations for spell-checker;

diff -r c706b57b1694 -r 368004bed323 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Tue Mar 07 15:35:54 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Tue Mar 07 16:06:42 2017 +0100
@@ -99,7 +99,9 @@
                 "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)" }
             }
         }
     },
diff -r c706b57b1694 -r 368004bed323 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 07 15:35:54 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Tue Mar 07 16:06:42 2017 +0100
@@ -58,9 +58,9 @@
         dark: { backgroundColor: get_color(color, false) } })
   }
 
-  function dotted(color: string): TextEditorDecorationType
+  function bottom_border(width: string, style: string, color: string): TextEditorDecorationType
   {
-    const border = "2px none; border-bottom-style: dotted; border-color: "
+    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 +74,9 @@
     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)
   }
+  types["spell_checker"] = bottom_border("1px", "solid", "spell_checker")
 }
 
 
diff -r c706b57b1694 -r 368004bed323 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 15:35:54 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Mar 07 16:06:42 2017 +0100
@@ -117,6 +117,21 @@
     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
@@ -125,7 +140,8 @@
     VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
       foreground(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 c706b57b1694 -r 368004bed323 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 07 15:35:54 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Mar 07 16:06:42 2017 +0100
@@ -272,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)
 }