#import "/utils/todo.typ": TODO
#import "/utils/isabelle.typ": *

== Decorations on File Switch <enhance:decorations>

Previously, when switching theories within #vscode, the dynamic syntax highlighting would not persist. It was possible to get the highlighting to work again by changing the buffer's content; however, until this was done, it never recovered by itself. This was a problem when working on multiple theory files.

To understand how #vscode does dynamic syntax highlighting, we will first examine the structure of the `PIDE/decoration` notifications. Recall that the primary data of notifications is sent within a `params` field. This field contains two components in this case: A `uri` field with the relevant theory file's URI and a list of decorations called `entries`. Each of these entries then consists of a `type` and a list of ranges called `content`. The `type` is a string identifier for an Isabelle decoration type. This includes `text_skolem` for Skolem variables and `dotted_warning` for text that should have a dotted underline. Each entry in the `content` list is another list of four integers describing the line start, line end, column start, and column end of the range to which the specified decoration type should be applied. @pide-decoration-json shows an example of what a `PIDE/decoration` message may look like.

Since this is not part of the standard LSP specification, a language client must implement a special handler for such decoration notifications. Additionally, it was not possible to explicitly request these decorations from the language server. Instead, the language server would send new decorations whenever it deemed necessary, e.g., because the caret moved into areas of the text that have not been decorated yet or because the document's content has changed.

#figure(
  box(width: 90%)[
    ```json
    "jsonrpc": "2.0",
    "method": "PIDE/decoration",
    "params": {
        "uri": "file:///home/user/Documents/Example.thy",
        "entries": [
            {
                "type": "text_main",
                "content": [
                    { "range": [1, 23, 1, 41] },
                    { "range": [5, 10, 5, 11] }
                ]
            },
            {
                "type": "text_operator",
                "content": [
                    { "range": [7, 6, 7, 7] }
                ]
            }
        ]
    }
    ```
  ],
  caption: [Example `PIDE/decoration` notification sent by the language server.],
  kind: raw,
  placement: auto,
) <pide-decoration-json>

On the VSCode side, these decorations were applied via the `TextEditor.setDecoration` API function #footnote[https://code.visualstudio.com/api/references/vscode-api#TextEditor.setDecorations], which does not inherently cache these decorations on file switch. Thus, when switching theories, VSCode did not cache the previously set decorations, nor did the language server send them again, causing the highlighting to disappear.

There were two primary ways to fix this issue:
1. Implement caching of decorations manually in the VSCode extension.

2. Add the ability to request new decorations from the server and do so on file switch.

The main advantage of option 1 is performance. If the client handles caching of decorations, then the server will not have to calculate the decorations anew (which is a rather expensive operation), nor will another round of JSON Serialization and Deserialization have to happen. However, the trade-off is that more work needs to be done on the client side, making new client implementations for other editors potentially harder.

Because of this, we instead introduced a new `PIDE/decoration_request` notification, sent by the client to explicitly signal to the server that it should send a `PIDE/decoration` notification back.

Note that this system is atypical for the LSP. The `PIDE/decoration_request` notification is, semantically speaking, a request and intends a response from the server. Nevertheless, from the perspective of the LSP, it is a unidirectional notification, while its response is also a unidirectional `PIDE/decoration` notification. We chose this approach for two reasons:
1. There was already precedent for such behavior in the Isabelle language server, specifically with `PIDE/preview_request` and `PIDE/preview_response` notifications.

2. The `PIDE/decoration` notification is not only sent after a request. The original automatic sending behavior that existed before is still present and has not been altered. If we were to implement `PIDE/decoration_request`s as an LSP request instead, this would only result in extra implementation work on the client side because a client would need to implement the same decoration application logic for both the `PIDE/decoration` notification and the `PIDE/decoration_request` response. By defining `PIDE/decoration_request`s as notifications, the client only needs to implement a singular handler for `PIDE/decoration` notifications, which automatically covers both scenarios simultaneously.

Later, we found that client-side caching was already implemented for the Isabelle VSCode extension; however, incorrectly so. The caching was implemented with the help of a JavaScript `Map` #footnote[https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/Map]. This `Map` used `URI`s #footnote[https://code.visualstudio.com/api/references/vscode-api#Uri] as keys and the content list from the decoration messages as values. However, the `URI` type does not explicitly implement an equality function, thus resulting in an inconsistent equality check where two `URI`s referencing the same file may not have passed an equality check. Switching the key to using string representations of the URIs fixed the issue. However, we decided to keep the `PIDE/decoration_request` notification. While it may not be used by #vscode directly, other Isabelle language client implementations may make use of this functionality.

// #TODO[
//   - currently breaks when switching files/tabs
//   - originally solved by implementing decoration request and requesting them every time we switch file/tab
//   - later found that client-side caching was implemented, but used URI as key instead of URI strings which didn't work
//   - decoration request kept in, in case a different client needs it (Foreshadowing to Sublime Text implementation which used it)
// ]
