clarified modules;
authorwenzelm
Tue Jun 20 17:08:24 2017 +0200 (2017-06-20)
changeset 6614181c8bb1d33b9
parent 66140 cdb6c10122b6
child 66142 90629b166203
clarified modules;
src/Pure/build-jars
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/VSCode/src/vscode_spell_checker.scala
     1.1 --- a/src/Pure/build-jars	Tue Jun 20 16:17:54 2017 +0200
     1.2 +++ b/src/Pure/build-jars	Tue Jun 20 17:08:24 2017 +0200
     1.3 @@ -174,6 +174,7 @@
     1.4    ../Tools/VSCode/src/state_panel.scala
     1.5    ../Tools/VSCode/src/vscode_rendering.scala
     1.6    ../Tools/VSCode/src/vscode_resources.scala
     1.7 +  ../Tools/VSCode/src/vscode_spell_checker.scala
     1.8  )
     1.9  
    1.10  
     2.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 16:17:54 2017 +0200
     2.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jun 20 17:08:24 2017 +0200
     2.3 @@ -100,7 +100,7 @@
     2.4            val results =
     2.5              Completion.Result.merge(history,
     2.6                Completion.Result.merge(history, semantic_completion, syntax_completion),
     2.7 -              spell_checker_completion(caret))
     2.8 +              VSCode_Spell_Checker.completion(rendering, caret))
     2.9            results match {
    2.10              case None => Nil
    2.11              case Some(result) =>
    2.12 @@ -109,7 +109,7 @@
    2.13                    label = item.replacement,
    2.14                    detail = Some(item.description.mkString(" ")),
    2.15                    range = Some(doc.range(item.range)))) :::
    2.16 -              spell_checker_menu(caret)
    2.17 +              VSCode_Spell_Checker.menu_items(rendering, caret)
    2.18            }
    2.19          }
    2.20      }
    2.21 @@ -192,67 +192,6 @@
    2.22      message_underline_color(VSCode_Rendering.dotted_elements, range)
    2.23  
    2.24  
    2.25 -  /* spell checker */
    2.26 -
    2.27 -  def spell_checker: Document_Model.Decoration =
    2.28 -  {
    2.29 -    val ranges =
    2.30 -      (for {
    2.31 -        spell_checker <- model.resources.spell_checker.get.iterator
    2.32 -        spell_range <- spell_checker_ranges(model.content.text_range).iterator
    2.33 -        text <- model.try_get_text(spell_range).iterator
    2.34 -        info <- spell_checker.marked_words(spell_range.start, text).iterator
    2.35 -      } yield info.range).toList
    2.36 -    Document_Model.Decoration.ranges("spell_checker", ranges)
    2.37 -  }
    2.38 -
    2.39 -  def spell_checker_completion(caret: Text.Offset): Option[Completion.Result] =
    2.40 -    model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
    2.41 -
    2.42 -  def spell_checker_menu(caret: Text.Offset): List[Protocol.CompletionItem] =
    2.43 -  {
    2.44 -    val result =
    2.45 -      for {
    2.46 -        spell_checker <- model.resources.spell_checker.get
    2.47 -        range = before_caret_range(caret)
    2.48 -        Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
    2.49 -      } yield (spell_checker, word)
    2.50 -
    2.51 -    result match {
    2.52 -      case Some((spell_checker, word)) =>
    2.53 -
    2.54 -        def item(command: Protocol.Command): Protocol.CompletionItem =
    2.55 -          Protocol.CompletionItem(
    2.56 -            label = command.title,
    2.57 -            text = Some(""),
    2.58 -            range = Some(model.content.doc.range(Text.Range(caret))),
    2.59 -            command = Some(command))
    2.60 -
    2.61 -        val update_items =
    2.62 -          if (spell_checker.check(word))
    2.63 -            List(
    2.64 -              item(Protocol.Exclude_Word.command),
    2.65 -              item(Protocol.Exclude_Word_Permanently.command))
    2.66 -          else
    2.67 -            List(
    2.68 -              item(Protocol.Include_Word.command),
    2.69 -              item(Protocol.Include_Word_Permanently.command))
    2.70 -
    2.71 -        val reset_items =
    2.72 -          spell_checker.reset_enabled() match {
    2.73 -            case 0 => Nil
    2.74 -            case n =>
    2.75 -              val command = Protocol.Reset_Words.command
    2.76 -              List(item(command).copy(label = command.title + " (" + n + ")"))
    2.77 -          }
    2.78 -
    2.79 -        update_items ::: reset_items
    2.80 -
    2.81 -      case None => Nil
    2.82 -    }
    2.83 -  }
    2.84 -
    2.85 -
    2.86    /* decorations */
    2.87  
    2.88    def decorations: List[Document_Model.Decoration] = // list of canonical length and order
    2.89 @@ -273,7 +212,7 @@
    2.90          () =>
    2.91            VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
    2.92              dotted(model.content.text_range)))).flatten :::
    2.93 -    List(spell_checker)
    2.94 +    List(VSCode_Spell_Checker.decoration(rendering))
    2.95  
    2.96    def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
    2.97    {
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/VSCode/src/vscode_spell_checker.scala	Tue Jun 20 17:08:24 2017 +0200
     3.3 @@ -0,0 +1,74 @@
     3.4 +/*  Title:      Tools/VSCode/src/vscode_spell_checker.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Specific spell-checker support for Isabelle/VSCode.
     3.8 +*/
     3.9 +
    3.10 +package isabelle.vscode
    3.11 +
    3.12 +
    3.13 +import isabelle._
    3.14 +
    3.15 +
    3.16 +object VSCode_Spell_Checker
    3.17 +{
    3.18 +  def decoration(rendering: VSCode_Rendering): Document_Model.Decoration =
    3.19 +  {
    3.20 +    val model = rendering.model
    3.21 +    val ranges =
    3.22 +      (for {
    3.23 +        spell_checker <- model.resources.spell_checker.get.iterator
    3.24 +        spell_range <- rendering.spell_checker_ranges(model.content.text_range).iterator
    3.25 +        text <- model.try_get_text(spell_range).iterator
    3.26 +        info <- spell_checker.marked_words(spell_range.start, text).iterator
    3.27 +      } yield info.range).toList
    3.28 +    Document_Model.Decoration.ranges("spell_checker", ranges)
    3.29 +  }
    3.30 +
    3.31 +  def completion(rendering: VSCode_Rendering, caret: Text.Offset): Option[Completion.Result] =
    3.32 +    rendering.model.resources.spell_checker.get.flatMap(_.completion(rendering, caret))
    3.33 +
    3.34 +  def menu_items(rendering: VSCode_Rendering, caret: Text.Offset): List[Protocol.CompletionItem] =
    3.35 +  {
    3.36 +    val model = rendering.model
    3.37 +    val result =
    3.38 +      for {
    3.39 +        spell_checker <- model.resources.spell_checker.get
    3.40 +        range = rendering.before_caret_range(caret)
    3.41 +        Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
    3.42 +      } yield (spell_checker, word)
    3.43 +
    3.44 +    result match {
    3.45 +      case Some((spell_checker, word)) =>
    3.46 +
    3.47 +        def item(command: Protocol.Command): Protocol.CompletionItem =
    3.48 +          Protocol.CompletionItem(
    3.49 +            label = command.title,
    3.50 +            text = Some(""),
    3.51 +            range = Some(model.content.doc.range(Text.Range(caret))),
    3.52 +            command = Some(command))
    3.53 +
    3.54 +        val update_items =
    3.55 +          if (spell_checker.check(word))
    3.56 +            List(
    3.57 +              item(Protocol.Exclude_Word.command),
    3.58 +              item(Protocol.Exclude_Word_Permanently.command))
    3.59 +          else
    3.60 +            List(
    3.61 +              item(Protocol.Include_Word.command),
    3.62 +              item(Protocol.Include_Word_Permanently.command))
    3.63 +
    3.64 +        val reset_items =
    3.65 +          spell_checker.reset_enabled() match {
    3.66 +            case 0 => Nil
    3.67 +            case n =>
    3.68 +              val command = Protocol.Reset_Words.command
    3.69 +              List(item(command).copy(label = command.title + " (" + n + ")"))
    3.70 +          }
    3.71 +
    3.72 +        update_items ::: reset_items
    3.73 +
    3.74 +      case None => Nil
    3.75 +    }
    3.76 +  }
    3.77 +}