added commands for spell-checker dictionary;
authorwenzelm
Tue Jun 20 15:04:34 2017 +0200 (2017-06-20)
changeset 66138f7ef4c50b747
parent 66137 d2923067b376
child 66139 6a8f8be2741c
added commands for spell-checker dictionary;
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/extension.ts
src/Tools/VSCode/extension/src/protocol.ts
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_resources.scala
     1.1 --- a/src/Tools/VSCode/extension/package.json	Tue Jun 20 11:19:06 2017 +0200
     1.2 +++ b/src/Tools/VSCode/extension/package.json	Tue Jun 20 15:04:34 2017 +0200
     1.3 @@ -72,6 +72,31 @@
     1.4                      "light": "./media/ViewSource.svg",
     1.5                      "dark": "./media/ViewSource_inverse.svg"
     1.6                  }
     1.7 +            },
     1.8 +            {
     1.9 +                "command": "isabelle.include-word",
    1.10 +                "title": "Include word",
    1.11 +                "category": "Isabelle"
    1.12 +            },
    1.13 +            {
    1.14 +                "command": "isabelle.include-word-permanently",
    1.15 +                "title": "Include word permanently",
    1.16 +                "category": "Isabelle"
    1.17 +            },
    1.18 +            {
    1.19 +                "command": "isabelle.exclude-word",
    1.20 +                "title": "Exclude word",
    1.21 +                "category": "Isabelle"
    1.22 +            },
    1.23 +            {
    1.24 +                "command": "isabelle.exclude-word-permanently",
    1.25 +                "title": "Exclude word permanently",
    1.26 +                "category": "Isabelle"
    1.27 +            },
    1.28 +            {
    1.29 +                "command": "isabelle.reset-words",
    1.30 +                "title": "Reset non-permanent words",
    1.31 +                "category": "Isabelle"
    1.32              }
    1.33          ],
    1.34          "menus": {
     2.1 --- a/src/Tools/VSCode/extension/src/extension.ts	Tue Jun 20 11:19:06 2017 +0200
     2.2 +++ b/src/Tools/VSCode/extension/src/extension.ts	Tue Jun 20 15:04:34 2017 +0200
     2.3 @@ -141,6 +141,25 @@
     2.4          languages.registerCompletionItemProvider(mode, completion_provider))
     2.5      }
     2.6  
     2.7 +
     2.8 +    /* spell checker */
     2.9 +
    2.10 +    language_client.onReady().then(() =>
    2.11 +    {
    2.12 +      context.subscriptions.push(
    2.13 +        commands.registerCommand("isabelle.include-word", uri =>
    2.14 +          language_client.sendNotification(protocol.include_word_type)),
    2.15 +        commands.registerCommand("isabelle.include-word-permanently", uri =>
    2.16 +          language_client.sendNotification(protocol.include_word_permanently_type)),
    2.17 +        commands.registerCommand("isabelle.exclude-word", uri =>
    2.18 +          language_client.sendNotification(protocol.exclude_word_type)),
    2.19 +        commands.registerCommand("isabelle.exclude-word-permanently", uri =>
    2.20 +          language_client.sendNotification(protocol.exclude_word_permanently_type)),
    2.21 +        commands.registerCommand("isabelle.reset-words", uri =>
    2.22 +          language_client.sendNotification(protocol.reset_words_type)))
    2.23 +    })
    2.24 +
    2.25 +
    2.26      /* start server */
    2.27  
    2.28      context.subscriptions.push(language_client.start())
     3.1 --- a/src/Tools/VSCode/extension/src/protocol.ts	Tue Jun 20 11:19:06 2017 +0200
     3.2 +++ b/src/Tools/VSCode/extension/src/protocol.ts	Tue Jun 20 15:04:34 2017 +0200
     3.3 @@ -104,3 +104,21 @@
     3.4  
     3.5  export const symbols_request_type =
     3.6    new NotificationType<void, void>("PIDE/symbols_request")
     3.7 +
     3.8 +
     3.9 +/* spell checker */
    3.10 +
    3.11 +export const include_word_type =
    3.12 +  new NotificationType<void, void>("PIDE/include_word")
    3.13 +
    3.14 +export const include_word_permanently_type =
    3.15 +  new NotificationType<void, void>("PIDE/include_word_permanently")
    3.16 +
    3.17 +export const exclude_word_type =
    3.18 +  new NotificationType<void, void>("PIDE/exclude_word")
    3.19 +
    3.20 +export const exclude_word_permanently_type =
    3.21 +  new NotificationType<void, void>("PIDE/exclude_word_permanently")
    3.22 +
    3.23 +export const reset_words_type =
    3.24 +  new NotificationType<void, void>("PIDE/reset_words")
     4.1 --- a/src/Tools/VSCode/src/protocol.scala	Tue Jun 20 11:19:06 2017 +0200
     4.2 +++ b/src/Tools/VSCode/src/protocol.scala	Tue Jun 20 15:04:34 2017 +0200
     4.3 @@ -258,6 +258,15 @@
     4.4    }
     4.5  
     4.6  
     4.7 +  /* commands */
     4.8 +
     4.9 +  sealed case class Command(title: String, command: String, arguments: List[JSON.T] = Nil)
    4.10 +  {
    4.11 +    def json: JSON.T =
    4.12 +      Map("title" -> title, "command" -> command, "arguments" -> arguments)
    4.13 +  }
    4.14 +
    4.15 +
    4.16    /* document edits */
    4.17  
    4.18    object DidOpenTextDocument
    4.19 @@ -323,7 +332,8 @@
    4.20      detail: Option[String] = None,
    4.21      documentation: Option[String] = None,
    4.22      insertText: Option[String] = None,
    4.23 -    range: Option[Line.Range] = None)
    4.24 +    range: Option[Line.Range] = None,
    4.25 +    command: Option[Command] = None)
    4.26    {
    4.27      def json: JSON.T =
    4.28        Map("label" -> label) ++
    4.29 @@ -333,7 +343,8 @@
    4.30        JSON.optional("insertText" -> insertText) ++
    4.31        JSON.optional("range" -> range.map(Range(_))) ++
    4.32        JSON.optional("textEdit" ->
    4.33 -        range.map(r => Map("range" -> Range(r), "newText" -> insertText.getOrElse(label))))
    4.34 +        range.map(r => Map("range" -> Range(r), "newText" -> insertText.getOrElse(label)))) ++
    4.35 +      JSON.optional("command" -> command.map(_.json))
    4.36    }
    4.37  
    4.38    object Completion extends RequestTextDocumentPosition("textDocument/completion")
    4.39 @@ -343,6 +354,15 @@
    4.40    }
    4.41  
    4.42  
    4.43 +  /* spell checker */
    4.44 +
    4.45 +  object Include_Word extends Notification0("PIDE/include_word")
    4.46 +  object Include_Word_Permanently extends Notification0("PIDE/include_word_permanently")
    4.47 +  object Exclude_Word extends Notification0("PIDE/exclude_word")
    4.48 +  object Exclude_Word_Permanently extends Notification0("PIDE/exclude_word_permanently")
    4.49 +  object Reset_Words extends Notification0("PIDE/reset_words")
    4.50 +
    4.51 +
    4.52    /* hover request */
    4.53  
    4.54    object Hover extends RequestTextDocumentPosition("textDocument/hover")
     5.1 --- a/src/Tools/VSCode/src/server.scala	Tue Jun 20 11:19:06 2017 +0200
     5.2 +++ b/src/Tools/VSCode/src/server.scala	Tue Jun 20 15:04:34 2017 +0200
     5.3 @@ -208,11 +208,22 @@
     5.4        if (resources.flush_output(channel)) delay_output.invoke()
     5.5      }
     5.6  
     5.7 +  def update_output(changed_nodes: Traversable[JFile])
     5.8 +  {
     5.9 +    resources.update_output(changed_nodes)
    5.10 +    delay_output.invoke()
    5.11 +  }
    5.12 +
    5.13 +  def update_output_visible()
    5.14 +  {
    5.15 +    resources.update_output_visible()
    5.16 +    delay_output.invoke()
    5.17 +  }
    5.18 +
    5.19    private val prover_output =
    5.20      Session.Consumer[Session.Commands_Changed](getClass.getName) {
    5.21        case changed =>
    5.22 -        resources.update_output(changed.nodes.toList.map(resources.node_file(_)))
    5.23 -        delay_output.invoke()
    5.24 +        update_output(changed.nodes.toList.map(resources.node_file(_)))
    5.25      }
    5.26  
    5.27    private val syslog =
    5.28 @@ -337,6 +348,32 @@
    5.29    }
    5.30  
    5.31  
    5.32 +  /* spell-checker dictionary */
    5.33 +
    5.34 +  def update_dictionary(include: Boolean, permanent: Boolean)
    5.35 +  {
    5.36 +    for {
    5.37 +      spell_checker <- resources.spell_checker.get
    5.38 +      caret <- resources.get_caret()
    5.39 +      rendering = caret.model.rendering()
    5.40 +      range = rendering.before_caret_range(caret.offset)
    5.41 +      Text.Info(_, word) <- Spell_Checker.current_word(rendering, range)
    5.42 +    } {
    5.43 +      spell_checker.update(word, include, permanent)
    5.44 +      update_output_visible()
    5.45 +    }
    5.46 +  }
    5.47 +
    5.48 +  def reset_dictionary()
    5.49 +  {
    5.50 +    for (spell_checker <- resources.spell_checker.get)
    5.51 +    {
    5.52 +      spell_checker.reset()
    5.53 +      update_output_visible()
    5.54 +    }
    5.55 +  }
    5.56 +
    5.57 +
    5.58    /* hover */
    5.59  
    5.60    def hover(id: Protocol.Id, node_pos: Line.Node_Position)
    5.61 @@ -400,6 +437,11 @@
    5.62            case Protocol.DidChangeTextDocument(file, _, changes) => change_document(file, changes)
    5.63            case Protocol.DidCloseTextDocument(file) => close_document(file)
    5.64            case Protocol.Completion(id, node_pos) => completion(id, node_pos)
    5.65 +          case Protocol.Include_Word(()) => update_dictionary(true, false)
    5.66 +          case Protocol.Include_Word_Permanently(()) => update_dictionary(true, true)
    5.67 +          case Protocol.Exclude_Word(()) => update_dictionary(false, false)
    5.68 +          case Protocol.Exclude_Word_Permanently(()) => update_dictionary(false, true)
    5.69 +          case Protocol.Reset_Words(()) => reset_dictionary()
    5.70            case Protocol.Hover(id, node_pos) => hover(id, node_pos)
    5.71            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
    5.72            case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
     6.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Jun 20 11:19:06 2017 +0200
     6.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Jun 20 15:04:34 2017 +0200
     6.3 @@ -285,6 +285,10 @@
     6.4    def update_output(changed_nodes: Traversable[JFile]): Unit =
     6.5      state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
     6.6  
     6.7 +  def update_output_visible(): Unit =
     6.8 +    state.change(st => st.copy(pending_output = st.pending_output ++
     6.9 +      (for ((file, model) <- st.models.iterator if model.node_visible) yield file)))
    6.10 +
    6.11    def flush_output(channel: Channel): Boolean =
    6.12    {
    6.13      state.change_result(st =>