# HG changeset patch
# User wenzelm
# Date 1497971304 -7200
# Node ID 81c8bb1d33b97a2da5486d148978699829cea657
# Parent  cdb6c10122b6f66d81418e74b12ac8ca50c96445
clarified modules;

diff -r cdb6c10122b6 -r 81c8bb1d33b9 src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Jun 20 16:17:54 2017 +0200
+++ b/src/Pure/build-jars	Tue Jun 20 17:08:24 2017 +0200
@@ -174,6 +174,7 @@
   ../Tools/VSCode/src/state_panel.scala
   ../Tools/VSCode/src/vscode_rendering.scala
   ../Tools/VSCode/src/vscode_resources.scala
+  ../Tools/VSCode/src/vscode_spell_checker.scala
 )
 
 
diff -r cdb6c10122b6 -r 81c8bb1d33b9 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 16:17:54 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 17:08:24 2017 +0200
@@ -100,7 +100,7 @@
           val results =
             Completion.Result.merge(history,
               Completion.Result.merge(history, semantic_completion, syntax_completion),
-              spell_checker_completion(caret))
+              VSCode_Spell_Checker.completion(rendering, caret))
           results match {
             case None => Nil
             case Some(result) =>
@@ -109,7 +109,7 @@
                   label = item.replacement,
                   detail = Some(item.description.mkString(" ")),
                   range = Some(doc.range(item.range)))) :::
-              spell_checker_menu(caret)
+              VSCode_Spell_Checker.menu_items(rendering, caret)
           }
         }
     }
@@ -192,67 +192,6 @@
     message_underline_color(VSCode_Rendering.dotted_elements, range)
 
 
-  /* spell checker */
-
-  def spell_checker: Document_Model.Decoration =
-  {
-    val ranges =
-      (for {
-        spell_checker <- model.resources.spell_checker.get.iterator
-        spell_range <- spell_checker_ranges(model.content.text_range).iterator
-        text <- model.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)
-  }
-
-  def spell_checker_completion(caret: Text.Offset): Option[Completion.Result] =
-    model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
-
-  def spell_checker_menu(caret: Text.Offset): List[Protocol.CompletionItem] =
-  {
-    val result =
-      for {
-        spell_checker <- model.resources.spell_checker.get
-        range = before_caret_range(caret)
-        Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
-      } yield (spell_checker, word)
-
-    result match {
-      case Some((spell_checker, word)) =>
-
-        def item(command: Protocol.Command): Protocol.CompletionItem =
-          Protocol.CompletionItem(
-            label = command.title,
-            text = Some(""),
-            range = Some(model.content.doc.range(Text.Range(caret))),
-            command = Some(command))
-
-        val update_items =
-          if (spell_checker.check(word))
-            List(
-              item(Protocol.Exclude_Word.command),
-              item(Protocol.Exclude_Word_Permanently.command))
-          else
-            List(
-              item(Protocol.Include_Word.command),
-              item(Protocol.Include_Word_Permanently.command))
-
-        val reset_items =
-          spell_checker.reset_enabled() match {
-            case 0 => Nil
-            case n =>
-              val command = Protocol.Reset_Words.command
-              List(item(command).copy(label = command.title + " (" + n + ")"))
-          }
-
-        update_items ::: reset_items
-
-      case None => Nil
-    }
-  }
-
-
   /* decorations */
 
   def decorations: List[Document_Model.Decoration] = // list of canonical length and order
@@ -273,7 +212,7 @@
         () =>
           VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
             dotted(model.content.text_range)))).flatten :::
-    List(spell_checker)
+    List(VSCode_Spell_Checker.decoration(rendering))
 
   def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
   {
diff -r cdb6c10122b6 -r 81c8bb1d33b9 src/Tools/VSCode/src/vscode_spell_checker.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/vscode_spell_checker.scala	Tue Jun 20 17:08:24 2017 +0200
@@ -0,0 +1,74 @@
+/*  Title:      Tools/VSCode/src/vscode_spell_checker.scala
+    Author:     Makarius
+
+Specific spell-checker support for Isabelle/VSCode.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object VSCode_Spell_Checker
+{
+  def decoration(rendering: VSCode_Rendering): Document_Model.Decoration =
+  {
+    val model = rendering.model
+    val ranges =
+      (for {
+        spell_checker <- model.resources.spell_checker.get.iterator
+        spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator
+        text <- model.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)
+  }
+
+  def completion(rendering: VSCode_Rendering, caret: Text.Offset): Option[Completion.Result] =
+    rendering.model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
+
+  def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[Protocol.CompletionItem] =
+  {
+    val model = rendering.model
+    val result =
+      for {
+        spell_checker <- model.resources.spell_checker.get
+        range = rendering.before_caret_range(caret)
+        Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
+      } yield (spell_checker, word)
+
+    result match {
+      case Some((spell_checker, word)) =>
+
+        def item(command: Protocol.Command): Protocol.CompletionItem =
+          Protocol.CompletionItem(
+            label = command.title,
+            text = Some(""),
+            range = Some(model.content.doc.range(Text.Range(caret))),
+            command = Some(command))
+
+        val update_items =
+          if (spell_checker.check(word))
+            List(
+              item(Protocol.Exclude_Word.command),
+              item(Protocol.Exclude_Word_Permanently.command))
+          else
+            List(
+              item(Protocol.Include_Word.command),
+              item(Protocol.Include_Word_Permanently.command))
+
+        val reset_items =
+          spell_checker.reset_enabled() match {
+            case 0 => Nil
+            case n =>
+              val command = Protocol.Reset_Words.command
+              List(item(command).copy(label = command.title + " (" + n + ")"))
+          }
+
+        update_items ::: reset_items
+
+      case None => Nil
+    }
+  }
+}