diff --git a/.github/workflows/cd.yml b/.github/workflows/cd.yml
index 0e25d58a..bddaf5d6 100644
--- a/.github/workflows/cd.yml
+++ b/.github/workflows/cd.yml
@@ -4,37 +4,6 @@ on:
     - published
 
 jobs:
-  publish-extension:
-    runs-on: ubuntu-latest
-    if: success() && startsWith(github.ref, 'refs/tags/')
-    steps:
-    - name: Checkout
-      uses: actions/checkout@v3
-    - name: Install Node.js
-      uses: actions/setup-node@v3
-      with:
-        node-version: 16.x
-    - name: Publish on VsCode marketplace
-      run: |
-        cd client
-        cp ../LICENSE . && cp ../README.md .
-    - name: Publish to Open VSX Registry
-      uses: HaaLeo/publish-vscode-extension@v1
-      id: publishToOpenVSX
-      with:
-        pat: ${{ secrets.OVSX_PAT }}
-        packagePath: ./client/
-        yarn: true
-        preRelease: false
-    - name: Publish to Visual Studio Marketplace
-      uses: HaaLeo/publish-vscode-extension@v1
-      with:
-        pat: ${{ secrets.VSCE_PAT }}
-        packagePath: ./client/
-        registryUrl: https://marketplace.visualstudio.com
-        extensionFile: ${{ steps.publishToOpenVSX.outputs.vsixPath }}
-        yarn: true
-        preRelease: false
 
   publish-opam-package:
     strategy:
diff --git a/.github/workflows/publish-extension.yml b/.github/workflows/publish-extension.yml
new file mode 100644
index 00000000..80b4c7a7
--- /dev/null
+++ b/.github/workflows/publish-extension.yml
@@ -0,0 +1,38 @@
+on: 
+    workflow_dispatch:
+      inputs:
+        tags:
+          description: 'Tag to use for release'  
+
+jobs:
+    publish-extension:
+      runs-on: ubuntu-latest
+      if: success() && startsWith(github.ref, 'refs/tags/')
+      steps:
+      - name: Checkout
+        uses: actions/checkout@v3
+      - name: Install Node.js
+        uses: actions/setup-node@v3
+        with:
+          node-version: 16.x
+      - name: Publish on VsCode marketplace
+        run: |
+          cd client
+          cp ../LICENSE . && cp ../README.md .
+      - name: Publish to Open VSX Registry
+        uses: HaaLeo/publish-vscode-extension@v1
+        id: publishToOpenVSX
+        with:
+          pat: ${{ secrets.OVSX_PAT }}
+          packagePath: ./client/
+          yarn: true
+          preRelease: false
+      - name: Publish to Visual Studio Marketplace
+        uses: HaaLeo/publish-vscode-extension@v1
+        with:
+          pat: ${{ secrets.VSCE_PAT }}
+          packagePath: ./client/
+          registryUrl: https://marketplace.visualstudio.com
+          extensionFile: ${{ steps.publishToOpenVSX.outputs.vsixPath }}
+          yarn: true
+          preRelease: false
\ No newline at end of file
diff --git a/.github/workflows/publish-server.yml b/.github/workflows/publish-server.yml
new file mode 100644
index 00000000..229a6616
--- /dev/null
+++ b/.github/workflows/publish-server.yml
@@ -0,0 +1,49 @@
+on: 
+  workflow_dispatch:
+    inputs:
+      tags:
+        description: 'Tag to use for release'  
+
+jobs:
+
+  publish-opam-package:
+    strategy:
+      matrix:
+        os: [ubuntu-latest]
+        ocaml-compiler: [4.14.x]
+    runs-on: ${{ matrix.os }}
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v3
+
+    - name: Use OCaml ${{ matrix.ocaml-compiler }}
+      uses: avsm/setup-ocaml@v2
+      with:
+        ocaml-compiler: ${{ matrix.ocaml-compiler }}
+
+    - name: Install opam-publish # 2.0.3 because more recent versions do not respect OPAMYES
+      run: opam install -y -j 2 opam-publish=2.0.3
+
+    - name: Inject slug/short variables
+      uses: rlespinasse/github-slug-action@v4
+
+    - uses: webfactory/ssh-agent@v0.8.0
+      with:
+          ssh-private-key: ${{ secrets.BOT_SSH_KEY }}
+
+    - name: Write PAT
+      env:
+        OPAM_PUBLISH_TOKEN: ${{ secrets.OPAM_PUBLISH_TOKEN }}
+      run: |
+        mkdir -p ~/.opam/plugins/opam-publish
+        printf "$OPAM_PUBLISH_TOKEN" > ~/.opam/plugins/opam-publish/vscoqbot.token
+
+    - name: Publish
+      run: |
+        eval $(opam env)
+        VERSION_SLUG="${GITHUB_REF_NAME_SLUG#v}"
+        VERSION="${GITHUB_REF_NAME#v}"
+        cd language-server
+        git config --global user.name vscoqbot
+        git config --global user.email vscoqbot@inria.fr
+        opam publish --no-browser -v $VERSION https://github.com/coq-community/vscoq/releases/download/$GITHUB_REF_NAME/vscoq-language-server-$VERSION_SLUG.tar.gz vscoq-language-server.opam
\ No newline at end of file
diff --git a/README.md b/README.md
index fafbe013..191e9244 100644
--- a/README.md
+++ b/README.md
@@ -16,7 +16,7 @@
 [zulip-link]: https://coq.zulipchat.com/#narrow/stream/237662-VsCoq-devs.20.26.20users
 
 VsCoq is an extension for [Visual Studio Code](https://code.visualstudio.com/)
-(VS Code) and [VSCodium](https://vscodium.com/) with support for the [Coq Proof
+(VS Code) and [VSCodium](https://vscodium.com/) which provides support for the [Coq Proof
 Assistant](https://coq.inria.fr/).
 
 This extension is currently developed and maintained as part of
@@ -29,42 +29,21 @@ This extension is currently developed and maintained as part of
 [Laurent Théry](https://github.com/thery),
 and contributors.
 
-## Problems with VsCoq 2 
+VsCoq is distributed in two flavours:
 
-The latest VsCoq 2 release has broken the extension for many users. We apologize for the inconvenience and are working through a solution to prevent this from happening in the future. 
+- **VsCoq Legacy** (required for Coq < 8.18, compatible with Coq >= 8.7) is based on the original 
+  VsCoq implementation by [C.J. Bell](https://github.com/siegebell). It uses the legacy XML protocol 
+  spoken by CoqIDE.\
+  For more information, see the [VsCoq 1 branch](https://github.com/coq-community/vscoq/tree/vscoq1).
+  *Please note it is no longer actively developed, but still maintained for compatibility purposes.*
 
-Currently, if you are using Coq 8.17 or lower you need to downgrade the current version of the extension. 
-You can either do this using the command line:
-```shell
-#installing vscoq 0.3.9 with codium 
-$ codium --install-extension maximedenes.vscoq@0.3.9
-#or with code
-$ code --install-extension maximedenes.vscoq@0.3.9
-``` 
-Or from the extensions panel in vscode: 
-- Go to the extensions panel 
-- Click on the cog 
-- Select `Install another version` 
-- When prompted choose version 0.3.9
-
-![](gif/downgrading-vscoq.gif)
-
-If you are using Coq 8.18, we are busy getting the language server package in opam ASAP. You can use vscoq 0.3.9 so long.
-
-## Status
-
-- VsCoq 1 (versions 0.x.y) is based on the original VsCoq implementation by [C.J. Bell](https://github.com/siegebell)
-  and compatible with Coq 8.7 or more recent. It uses the legacy XML protocol
-  spoken by CoqIDE. For more information, see the
-  [VsCoq 1 branch](https://github.com/coq-community/vscoq/tree/vscoq1).
-- VsCoq 2 (beta releases versions 1.9.x) is a full reimplementation around a
-  language server which natively speaks the LSP protocol. VsCoq 2 is
-  compatible with Coq 8.18 or more recent, and supports manual or continuous mode
-  checking.
-
-## Installing VsCoq 2
-
-To use VsCoq 2, you need to (1) install the VsCoq 2 language server
+- **VsCoq** (recommended for Coq >= 8.18) is a full reimplementation around a
+  language server which natively speaks the 
+  [LSP protocol](https://learn.microsoft.com/en-us/visualstudio/extensibility/language-server-protocol?view=vs-2022). 
+
+## Installing VsCoq
+
+To use VsCoq, you need to (1) install the VsCoq language server
 and (2) install and configure the VsCoq extension in either VS Code or VSCodium.
 
 ### Installing the language server
@@ -130,8 +109,34 @@ We also support inline queries which then trigger messages in the goal panel.
 After installation and activation of the extension:
 
 (Press `F1` and start typing "settings" to open either workspace/project or user settings.)
+#### Coq configuration
 * `"vscoq.path": ""` -- specify the path to `vscoqtop` (e.g. `path/to/vscoq/bin/vscoqtop`)
 * `"vscoq.args": []` -- an array of strings specifying additional command line arguments for `vscoqtop` (typically accepts the same flags as `coqtop`)
+* `"vscoq.trace.server": off | messages | verbose` -- Toggles the tracing of communications between the server and client
+
+#### Proof checking
+* `"vscoq.proof.cursor.sticky": bool` -- a toggle to specify wether the cursor should move as Coq interactively navigates a document (step forward, backward, etc...)
+* `"vscoq.proof.mode": Continuous | Manual` -- Decide wether documents should checked continuously or using the classig navigation commmands (defaults to `Continuous`)
+* `"vscoq.proof.delegation": None | Skip | Delegate` -- Decides which delegation strategy should be used by the server. 
+  `Skip` allows to skip proofs which are out of focus and should be used in manual mode. `Delegate` allocates a settable amount of workers
+  to delegate proofs. 
+* `"vscoq.proof.workers": int` -- Determines how many workers should be used for proof checking
+
+#### Goal and info view panel
+* `"vscoq.goals.diff.mode": on | off | removed` -- Toggles diff mode. If set to `removed`, only removed characters are shown (defaults to `off`)
+* `"vscoq.goals.display": Tabs | List` -- Decide whether to display goals in seperate tabs or as a list of collapsibles.
+* `"vscoq.goals.messages.full": bool` -- A toggle to include warning and errors in the proof view (defaults to `false`)
+
+#### Diagnostics
+* `"vscoq.diagnostics.full": bool` -- Toggles the printing of `Info` level diagnostics (defaults to `false`)
+
+#### Code completion (experimental)
+* `"vscoq.completion.enable": bool` -- Toggle code completion (defaults to `false`)
+* `"vscoq.completion.algorithm": StructuredSplitUnification | SplitTypeIntersection` -- Which completion algorithm to use
+* `"vscoq.completion.unificationLimit": int` -- Sets the limit for how many theorems unification is attempted
+
+## For extension developers 
+See [Dev docs](https://github.com/coq-community/vscoq/blob/main/docs/developers.md)
 
 ## License
 Unless mentioned otherwise, files in this repository are [distributed under the MIT License](LICENSE).
diff --git a/client/goal-view-ui/yarn.lock b/client/goal-view-ui/yarn.lock
index ff7e63b4..51f723b9 100644
--- a/client/goal-view-ui/yarn.lock
+++ b/client/goal-view-ui/yarn.lock
@@ -17,6 +17,14 @@
   dependencies:
     "@babel/highlight" "^7.18.6"
 
+"@babel/code-frame@^7.22.13":
+  version "7.22.13"
+  resolved "https://registry.yarnpkg.com/@babel/code-frame/-/code-frame-7.22.13.tgz#e3c1c099402598483b7a8c46a721d1038803755e"
+  integrity sha512-XktuhWlJ5g+3TJXc5upd9Ks1HutSArik6jf2eAjYFyIOf4ej3RN+184cZbzDvbPnuTJIUhPKKJE3cIsYTiAT3w==
+  dependencies:
+    "@babel/highlight" "^7.22.13"
+    chalk "^2.4.2"
+
 "@babel/compat-data@^7.20.5":
   version "7.20.10"
   resolved "https://registry.npmjs.org/@babel/compat-data/-/compat-data-7.20.10.tgz"
@@ -52,6 +60,16 @@
     "@jridgewell/gen-mapping" "^0.3.2"
     jsesc "^2.5.1"
 
+"@babel/generator@^7.23.0":
+  version "7.23.0"
+  resolved "https://registry.yarnpkg.com/@babel/generator/-/generator-7.23.0.tgz#df5c386e2218be505b34837acbcb874d7a983420"
+  integrity sha512-lN85QRR+5IbYrMWM6Y4pE/noaQtg4pNiqeNGX60eqOfo6gtEj6uw/JagelB8vVztSd7R6M5n1+PQkDbHbBRU4g==
+  dependencies:
+    "@babel/types" "^7.23.0"
+    "@jridgewell/gen-mapping" "^0.3.2"
+    "@jridgewell/trace-mapping" "^0.3.17"
+    jsesc "^2.5.1"
+
 "@babel/helper-annotate-as-pure@^7.18.6":
   version "7.18.6"
   resolved "https://registry.npmjs.org/@babel/helper-annotate-as-pure/-/helper-annotate-as-pure-7.18.6.tgz"
@@ -75,20 +93,25 @@
   resolved "https://registry.npmjs.org/@babel/helper-environment-visitor/-/helper-environment-visitor-7.18.9.tgz"
   integrity sha512-3r/aACDJ3fhQ/EVgFy0hpj8oHyHpQc+LPtJoY9SzTThAsStm4Ptegq92vqKoE3vD706ZVFWITnMnxucw+S9Ipg==
 
-"@babel/helper-function-name@^7.19.0":
-  version "7.19.0"
-  resolved "https://registry.npmjs.org/@babel/helper-function-name/-/helper-function-name-7.19.0.tgz"
-  integrity sha512-WAwHBINyrpqywkUH0nTnNgI5ina5TFn85HKS0pbPDfxFfhyR/aNQEn4hGi1P1JyT//I0t4OgXUlofzWILRvS5w==
+"@babel/helper-environment-visitor@^7.22.20":
+  version "7.22.20"
+  resolved "https://registry.yarnpkg.com/@babel/helper-environment-visitor/-/helper-environment-visitor-7.22.20.tgz#96159db61d34a29dba454c959f5ae4a649ba9167"
+  integrity sha512-zfedSIzFhat/gFhWfHtgWvlec0nqB9YEIVrpuwjruLlXfUSnA8cJB0miHKwqDnQ7d32aKo2xt88/xZptwxbfhA==
+
+"@babel/helper-function-name@^7.23.0":
+  version "7.23.0"
+  resolved "https://registry.yarnpkg.com/@babel/helper-function-name/-/helper-function-name-7.23.0.tgz#1f9a3cdbd5b2698a670c30d2735f9af95ed52759"
+  integrity sha512-OErEqsrxjZTJciZ4Oo+eoZqeW9UIiOcuYKRJA4ZAgV9myA+pOXhhmpfNCKjEH/auVfEYVFJ6y1Tc4r0eIApqiw==
   dependencies:
-    "@babel/template" "^7.18.10"
-    "@babel/types" "^7.19.0"
+    "@babel/template" "^7.22.15"
+    "@babel/types" "^7.23.0"
 
-"@babel/helper-hoist-variables@^7.18.6":
-  version "7.18.6"
-  resolved "https://registry.npmjs.org/@babel/helper-hoist-variables/-/helper-hoist-variables-7.18.6.tgz"
-  integrity sha512-UlJQPkFqFULIcyW5sbzgbkxn2FKRgwWiRexcuaR8RNJRy8+LLveqPjwZV/bwrLZCN0eUHD/x8D0heK1ozuoo6Q==
+"@babel/helper-hoist-variables@^7.22.5":
+  version "7.22.5"
+  resolved "https://registry.yarnpkg.com/@babel/helper-hoist-variables/-/helper-hoist-variables-7.22.5.tgz#c01a007dac05c085914e8fb652b339db50d823bb"
+  integrity sha512-wGjk9QZVzvknA6yKIUURb8zY3grXCcOZt+/7Wcy8O2uctxhplmUPkOdlgoNhmdVee2c92JXbf1xpMtVNbfoxRw==
   dependencies:
-    "@babel/types" "^7.18.6"
+    "@babel/types" "^7.22.5"
 
 "@babel/helper-module-imports@^7.18.6":
   version "7.18.6"
@@ -130,16 +153,33 @@
   dependencies:
     "@babel/types" "^7.18.6"
 
+"@babel/helper-split-export-declaration@^7.22.6":
+  version "7.22.6"
+  resolved "https://registry.yarnpkg.com/@babel/helper-split-export-declaration/-/helper-split-export-declaration-7.22.6.tgz#322c61b7310c0997fe4c323955667f18fcefb91c"
+  integrity sha512-AsUnxuLhRYsisFiaJwvp1QF+I3KjD5FOxut14q/GzovUe6orHLesW2C7d754kRm53h5gqrz6sFl6sxc4BVtE/g==
+  dependencies:
+    "@babel/types" "^7.22.5"
+
 "@babel/helper-string-parser@^7.19.4":
   version "7.19.4"
   resolved "https://registry.npmjs.org/@babel/helper-string-parser/-/helper-string-parser-7.19.4.tgz"
   integrity sha512-nHtDoQcuqFmwYNYPz3Rah5ph2p8PFeFCsZk9A/48dPc/rGocJ5J3hAAZ7pb76VWX3fZKu+uEr/FhH5jLx7umrw==
 
+"@babel/helper-string-parser@^7.22.5":
+  version "7.22.5"
+  resolved "https://registry.yarnpkg.com/@babel/helper-string-parser/-/helper-string-parser-7.22.5.tgz#533f36457a25814cf1df6488523ad547d784a99f"
+  integrity sha512-mM4COjgZox8U+JcXQwPijIZLElkgEpO5rsERVDJTc2qfCDfERyob6k5WegS14SX18IIjv+XD+GrqNumY5JRCDw==
+
 "@babel/helper-validator-identifier@^7.18.6", "@babel/helper-validator-identifier@^7.19.1":
   version "7.19.1"
   resolved "https://registry.npmjs.org/@babel/helper-validator-identifier/-/helper-validator-identifier-7.19.1.tgz"
   integrity sha512-awrNfaMtnHUr653GgGEs++LlAvW6w+DcPrOliSMXWCKo597CwL5Acf/wWdNkf/tfEQE3mjkeD1YOVZOUV/od1w==
 
+"@babel/helper-validator-identifier@^7.22.20":
+  version "7.22.20"
+  resolved "https://registry.yarnpkg.com/@babel/helper-validator-identifier/-/helper-validator-identifier-7.22.20.tgz#c4ae002c61d2879e724581d96665583dbc1dc0e0"
+  integrity sha512-Y4OZ+ytlatR8AI+8KZfKuL5urKp7qey08ha31L8b3BwewJAoJamTzyvxPR/5D+KkdJCGPq/+8TukHBlY10FX9A==
+
 "@babel/helper-validator-option@^7.18.6":
   version "7.18.6"
   resolved "https://registry.npmjs.org/@babel/helper-validator-option/-/helper-validator-option-7.18.6.tgz"
@@ -163,11 +203,25 @@
     chalk "^2.0.0"
     js-tokens "^4.0.0"
 
-"@babel/parser@^7.20.13", "@babel/parser@^7.20.7":
+"@babel/highlight@^7.22.13":
+  version "7.22.20"
+  resolved "https://registry.yarnpkg.com/@babel/highlight/-/highlight-7.22.20.tgz#4ca92b71d80554b01427815e06f2df965b9c1f54"
+  integrity sha512-dkdMCN3py0+ksCgYmGG8jKeGA/8Tk+gJwSYYlFGxG5lmhfKNoAy004YpLxpS1W2J8m/EK2Ew+yOs9pVRwO89mg==
+  dependencies:
+    "@babel/helper-validator-identifier" "^7.22.20"
+    chalk "^2.4.2"
+    js-tokens "^4.0.0"
+
+"@babel/parser@^7.20.7":
   version "7.20.13"
   resolved "https://registry.npmjs.org/@babel/parser/-/parser-7.20.13.tgz"
   integrity sha512-gFDLKMfpiXCsjt4za2JA9oTMn70CeseCehb11kRZgvd7+F67Hih3OHOK24cRrWECJ/ljfPGac6ygXAs/C8kIvw==
 
+"@babel/parser@^7.22.15", "@babel/parser@^7.23.0":
+  version "7.23.0"
+  resolved "https://registry.yarnpkg.com/@babel/parser/-/parser-7.23.0.tgz#da950e622420bf96ca0d0f2909cdddac3acd8719"
+  integrity sha512-vvPKKdMemU85V9WE/l5wZEmImpCtLqbnTvqDS2U1fJ96KrxoW7KrXhNsNCblQlg8Ck4b85yxdTyelsMUgFUXiw==
+
 "@babel/plugin-syntax-jsx@^7.18.6":
   version "7.18.6"
   resolved "https://registry.npmjs.org/@babel/plugin-syntax-jsx/-/plugin-syntax-jsx-7.18.6.tgz"
@@ -207,7 +261,7 @@
     "@babel/plugin-syntax-jsx" "^7.18.6"
     "@babel/types" "^7.20.7"
 
-"@babel/template@^7.18.10", "@babel/template@^7.20.7":
+"@babel/template@^7.20.7":
   version "7.20.7"
   resolved "https://registry.npmjs.org/@babel/template/-/template-7.20.7.tgz"
   integrity sha512-8SegXApWe6VoNw0r9JHpSteLKTpTiLZ4rMlGIm9JQ18KiCtyQiAMEazujAHrUS5flrcqYZa75ukev3P6QmUwUw==
@@ -216,23 +270,32 @@
     "@babel/parser" "^7.20.7"
     "@babel/types" "^7.20.7"
 
-"@babel/traverse@^7.20.10", "@babel/traverse@^7.20.12", "@babel/traverse@^7.20.13":
-  version "7.20.13"
-  resolved "https://registry.npmjs.org/@babel/traverse/-/traverse-7.20.13.tgz"
-  integrity sha512-kMJXfF0T6DIS9E8cgdLCSAL+cuCK+YEZHWiLK0SXpTo8YRj5lpJu3CDNKiIBCne4m9hhTIqUg6SYTAI39tAiVQ==
+"@babel/template@^7.22.15":
+  version "7.22.15"
+  resolved "https://registry.yarnpkg.com/@babel/template/-/template-7.22.15.tgz#09576efc3830f0430f4548ef971dde1350ef2f38"
+  integrity sha512-QPErUVm4uyJa60rkI73qneDacvdvzxshT3kksGqlGWYdOTIUOwJ7RDUL8sGqslY1uXWSL6xMFKEXDS3ox2uF0w==
   dependencies:
-    "@babel/code-frame" "^7.18.6"
-    "@babel/generator" "^7.20.7"
-    "@babel/helper-environment-visitor" "^7.18.9"
-    "@babel/helper-function-name" "^7.19.0"
-    "@babel/helper-hoist-variables" "^7.18.6"
-    "@babel/helper-split-export-declaration" "^7.18.6"
-    "@babel/parser" "^7.20.13"
-    "@babel/types" "^7.20.7"
+    "@babel/code-frame" "^7.22.13"
+    "@babel/parser" "^7.22.15"
+    "@babel/types" "^7.22.15"
+
+"@babel/traverse@^7.20.10", "@babel/traverse@^7.20.12", "@babel/traverse@^7.20.13":
+  version "7.23.2"
+  resolved "https://registry.yarnpkg.com/@babel/traverse/-/traverse-7.23.2.tgz#329c7a06735e144a506bdb2cad0268b7f46f4ad8"
+  integrity sha512-azpe59SQ48qG6nu2CzcMLbxUudtN+dOM9kDbUqGq3HXUJRlo7i8fvPoxQUzYgLZ4cMVmuZgm8vvBpNeRhd6XSw==
+  dependencies:
+    "@babel/code-frame" "^7.22.13"
+    "@babel/generator" "^7.23.0"
+    "@babel/helper-environment-visitor" "^7.22.20"
+    "@babel/helper-function-name" "^7.23.0"
+    "@babel/helper-hoist-variables" "^7.22.5"
+    "@babel/helper-split-export-declaration" "^7.22.6"
+    "@babel/parser" "^7.23.0"
+    "@babel/types" "^7.23.0"
     debug "^4.1.0"
     globals "^11.1.0"
 
-"@babel/types@^7.18.6", "@babel/types@^7.19.0", "@babel/types@^7.20.2", "@babel/types@^7.20.7":
+"@babel/types@^7.18.6", "@babel/types@^7.20.2", "@babel/types@^7.20.7":
   version "7.20.7"
   resolved "https://registry.npmjs.org/@babel/types/-/types-7.20.7.tgz"
   integrity sha512-69OnhBxSSgK0OzTJai4kyPDiKTIe3j+ctaHdIGVbRahTLAT7L3R9oeXHC2aVSuGYt3cVnoAMDmOCgJ2yaiLMvg==
@@ -241,6 +304,15 @@
     "@babel/helper-validator-identifier" "^7.19.1"
     to-fast-properties "^2.0.0"
 
+"@babel/types@^7.22.15", "@babel/types@^7.22.5", "@babel/types@^7.23.0":
+  version "7.23.0"
+  resolved "https://registry.yarnpkg.com/@babel/types/-/types-7.23.0.tgz#8c1f020c9df0e737e4e247c0619f58c68458aaeb"
+  integrity sha512-0oIyUfKoI3mSqMvsxBdclDwxXKXAUA8v/apZbc+iSyARYou1o8ZGDxbUYyLFoW2arqS2jDGqJuZvv1d/io1axg==
+  dependencies:
+    "@babel/helper-string-parser" "^7.22.5"
+    "@babel/helper-validator-identifier" "^7.22.20"
+    to-fast-properties "^2.0.0"
+
 "@esbuild/linux-loong64@0.14.54":
   version "0.14.54"
   resolved "https://registry.yarnpkg.com/@esbuild/linux-loong64/-/linux-loong64-0.14.54.tgz#de2a4be678bd4d0d1ffbb86e6de779cde5999028"
@@ -268,6 +340,11 @@
   resolved "https://registry.npmjs.org/@jridgewell/resolve-uri/-/resolve-uri-3.1.0.tgz"
   integrity sha512-F2msla3tad+Mfht5cJq7LSXcdudKTWCVYUgw6pLFOOHSTtZlj6SWNYAp+AhuqLmWdBO2X5hPrLcu8cVP8fy28w==
 
+"@jridgewell/resolve-uri@^3.1.0":
+  version "3.1.1"
+  resolved "https://registry.yarnpkg.com/@jridgewell/resolve-uri/-/resolve-uri-3.1.1.tgz#c08679063f279615a3326583ba3a90d1d82cc721"
+  integrity sha512-dSYZh7HhCDtCKm4QakX0xFpsRDqjjtZf/kjI/v3T3Nwt5r8/qz/M19F9ySyOqU94SXBmeG9ttTul+YnR4LOxFA==
+
 "@jridgewell/set-array@^1.0.0", "@jridgewell/set-array@^1.0.1":
   version "1.1.2"
   resolved "https://registry.npmjs.org/@jridgewell/set-array/-/set-array-1.1.2.tgz"
@@ -278,6 +355,19 @@
   resolved "https://registry.npmjs.org/@jridgewell/sourcemap-codec/-/sourcemap-codec-1.4.14.tgz"
   integrity sha512-XPSJHWmi394fuUuzDnGz1wiKqWfo1yXecHQMRf2l6hztTO+nPru658AyDngaBe7isIxEkRsPR3FZh+s7iVa4Uw==
 
+"@jridgewell/sourcemap-codec@^1.4.14":
+  version "1.4.15"
+  resolved "https://registry.yarnpkg.com/@jridgewell/sourcemap-codec/-/sourcemap-codec-1.4.15.tgz#d7c6e6755c78567a951e04ab52ef0fd26de59f32"
+  integrity sha512-eF2rxCRulEKXHTRiDrDy6erMYWqNw4LPdQ8UQA4huuxaQsVeRPFl2oM8oDGxMFhJUWZf9McpLtJasDDZb/Bpeg==
+
+"@jridgewell/trace-mapping@^0.3.17":
+  version "0.3.20"
+  resolved "https://registry.yarnpkg.com/@jridgewell/trace-mapping/-/trace-mapping-0.3.20.tgz#72e45707cf240fa6b081d0366f8265b0cd10197f"
+  integrity sha512-R8LcPeWZol2zR8mmH3JeKQ6QRCFb7XgUhV9ZlGhHLGyg4wpPiPZNQOOWhFZhxKw8u//yTbNGI42Bx/3paXEQ+Q==
+  dependencies:
+    "@jridgewell/resolve-uri" "^3.1.0"
+    "@jridgewell/sourcemap-codec" "^1.4.14"
+
 "@jridgewell/trace-mapping@^0.3.9":
   version "0.3.17"
   resolved "https://registry.npmjs.org/@jridgewell/trace-mapping/-/trace-mapping-0.3.17.tgz"
@@ -405,7 +495,7 @@ caniuse-lite@^1.0.30001400:
   resolved "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001447.tgz"
   integrity sha512-bdKU1BQDPeEXe9A39xJnGtY0uRq/z5osrnXUw0TcK+EYno45Y+U7QU9HhHEyzvMDffpYadFXi3idnSNkcwLkTw==
 
-chalk@^2.0.0:
+chalk@^2.0.0, chalk@^2.4.2:
   version "2.4.2"
   resolved "https://registry.npmjs.org/chalk/-/chalk-2.4.2.tgz"
   integrity sha512-Mti+f9lpJNcwF4tWV8/OrTTtF1gZi+f8FqlyAdouralcFWFQWF2+NgCHShjkCb+IFBLq9buZwE1xckQU4peSuQ==
@@ -668,10 +758,10 @@ ms@2.1.2:
   resolved "https://registry.npmjs.org/ms/-/ms-2.1.2.tgz"
   integrity sha512-sGkPx+VjMtmA6MX27oA4FBFELFCZZ4S4XqeGOXCv68tT+jb3vk/RyaKWP0PTKyWtmLSM0b+adUTEvbs1PEaH2w==
 
-nanoid@^3.3.4:
-  version "3.3.4"
-  resolved "https://registry.npmjs.org/nanoid/-/nanoid-3.3.4.tgz"
-  integrity sha512-MqBkQh/OHTS2egovRtLk45wEyNXwF+cokD+1YPf9u5VfJiRdAiRwB2froX5Co9Rh20xs4siNPm8naNotSD6RBw==
+nanoid@^3.3.6:
+  version "3.3.6"
+  resolved "https://registry.yarnpkg.com/nanoid/-/nanoid-3.3.6.tgz#443380c856d6e9f9824267d960b4236ad583ea4c"
+  integrity sha512-BGcqMMJuToF7i1rt+2PWSNVnWIkGCU78jBG3RxO/bZlnZPK2Cmi2QaffxGO/2RvWi9sL+FAiRiXMgsyxQ1DIDA==
 
 node-releases@^2.0.6:
   version "2.0.8"
@@ -699,11 +789,11 @@ picomatch@^2.2.2:
   integrity sha512-JU3teHTNjmE2VCGFzuY8EXzCDVwEqB2a8fsIvwaStHhAWJEeVd1o1QD80CU6+ZdEXXSLbSsuLwJjkCBWqRQUVA==
 
 postcss@^8.4.13:
-  version "8.4.21"
-  resolved "https://registry.npmjs.org/postcss/-/postcss-8.4.21.tgz"
-  integrity sha512-tP7u/Sn/dVxK2NnruI4H9BG+x+Wxz6oeZ1cJ8P6G/PZY0IKk4k/63TDsQf2kQq3+qoJeLm2kIBUNlZe3zgb4Zg==
+  version "8.4.31"
+  resolved "https://registry.yarnpkg.com/postcss/-/postcss-8.4.31.tgz#92b451050a9f914da6755af352bdc0192508656d"
+  integrity sha512-PS08Iboia9mts/2ygV3eLpY5ghnUcfLV/EXTOW1E2qYxJKGGBUtNjN76FYHnMs36RmARn41bC0AZmn+rR0OVpQ==
   dependencies:
-    nanoid "^3.3.4"
+    nanoid "^3.3.6"
     picocolors "^1.0.0"
     source-map-js "^1.0.2"
 
diff --git a/client/package.json b/client/package.json
index f0738170..d345e35c 100644
--- a/client/package.json
+++ b/client/package.json
@@ -4,7 +4,7 @@
   "description": "VsCoq is an extension for Visual Studio Code with support for the Coq Proof Assistant",
   "publisher": "maximedenes",
   "license": "MIT",
-  "version": "2.0.1",
+  "version": "2.0.2",
   "repository": {
     "type": "git",
     "url": "https://github.com/coq-community/vscoq.git"
diff --git a/client/search-ui/yarn.lock b/client/search-ui/yarn.lock
index 5ea10161..10b4c601 100644
--- a/client/search-ui/yarn.lock
+++ b/client/search-ui/yarn.lock
@@ -17,6 +17,14 @@
   dependencies:
     "@babel/highlight" "^7.18.6"
 
+"@babel/code-frame@^7.22.13":
+  version "7.22.13"
+  resolved "https://registry.yarnpkg.com/@babel/code-frame/-/code-frame-7.22.13.tgz#e3c1c099402598483b7a8c46a721d1038803755e"
+  integrity sha512-XktuhWlJ5g+3TJXc5upd9Ks1HutSArik6jf2eAjYFyIOf4ej3RN+184cZbzDvbPnuTJIUhPKKJE3cIsYTiAT3w==
+  dependencies:
+    "@babel/highlight" "^7.22.13"
+    chalk "^2.4.2"
+
 "@babel/compat-data@^7.20.5":
   version "7.20.10"
   resolved "https://registry.yarnpkg.com/@babel/compat-data/-/compat-data-7.20.10.tgz#9d92fa81b87542fff50e848ed585b4212c1d34ec"
@@ -52,6 +60,16 @@
     "@jridgewell/gen-mapping" "^0.3.2"
     jsesc "^2.5.1"
 
+"@babel/generator@^7.23.0":
+  version "7.23.0"
+  resolved "https://registry.yarnpkg.com/@babel/generator/-/generator-7.23.0.tgz#df5c386e2218be505b34837acbcb874d7a983420"
+  integrity sha512-lN85QRR+5IbYrMWM6Y4pE/noaQtg4pNiqeNGX60eqOfo6gtEj6uw/JagelB8vVztSd7R6M5n1+PQkDbHbBRU4g==
+  dependencies:
+    "@babel/types" "^7.23.0"
+    "@jridgewell/gen-mapping" "^0.3.2"
+    "@jridgewell/trace-mapping" "^0.3.17"
+    jsesc "^2.5.1"
+
 "@babel/helper-annotate-as-pure@^7.18.6":
   version "7.18.6"
   resolved "https://registry.yarnpkg.com/@babel/helper-annotate-as-pure/-/helper-annotate-as-pure-7.18.6.tgz#eaa49f6f80d5a33f9a5dd2276e6d6e451be0a6bb"
@@ -75,20 +93,25 @@
   resolved "https://registry.yarnpkg.com/@babel/helper-environment-visitor/-/helper-environment-visitor-7.18.9.tgz#0c0cee9b35d2ca190478756865bb3528422f51be"
   integrity sha512-3r/aACDJ3fhQ/EVgFy0hpj8oHyHpQc+LPtJoY9SzTThAsStm4Ptegq92vqKoE3vD706ZVFWITnMnxucw+S9Ipg==
 
-"@babel/helper-function-name@^7.19.0":
-  version "7.19.0"
-  resolved "https://registry.yarnpkg.com/@babel/helper-function-name/-/helper-function-name-7.19.0.tgz#941574ed5390682e872e52d3f38ce9d1bef4648c"
-  integrity sha512-WAwHBINyrpqywkUH0nTnNgI5ina5TFn85HKS0pbPDfxFfhyR/aNQEn4hGi1P1JyT//I0t4OgXUlofzWILRvS5w==
+"@babel/helper-environment-visitor@^7.22.20":
+  version "7.22.20"
+  resolved "https://registry.yarnpkg.com/@babel/helper-environment-visitor/-/helper-environment-visitor-7.22.20.tgz#96159db61d34a29dba454c959f5ae4a649ba9167"
+  integrity sha512-zfedSIzFhat/gFhWfHtgWvlec0nqB9YEIVrpuwjruLlXfUSnA8cJB0miHKwqDnQ7d32aKo2xt88/xZptwxbfhA==
+
+"@babel/helper-function-name@^7.23.0":
+  version "7.23.0"
+  resolved "https://registry.yarnpkg.com/@babel/helper-function-name/-/helper-function-name-7.23.0.tgz#1f9a3cdbd5b2698a670c30d2735f9af95ed52759"
+  integrity sha512-OErEqsrxjZTJciZ4Oo+eoZqeW9UIiOcuYKRJA4ZAgV9myA+pOXhhmpfNCKjEH/auVfEYVFJ6y1Tc4r0eIApqiw==
   dependencies:
-    "@babel/template" "^7.18.10"
-    "@babel/types" "^7.19.0"
+    "@babel/template" "^7.22.15"
+    "@babel/types" "^7.23.0"
 
-"@babel/helper-hoist-variables@^7.18.6":
-  version "7.18.6"
-  resolved "https://registry.yarnpkg.com/@babel/helper-hoist-variables/-/helper-hoist-variables-7.18.6.tgz#d4d2c8fb4baeaa5c68b99cc8245c56554f926678"
-  integrity sha512-UlJQPkFqFULIcyW5sbzgbkxn2FKRgwWiRexcuaR8RNJRy8+LLveqPjwZV/bwrLZCN0eUHD/x8D0heK1ozuoo6Q==
+"@babel/helper-hoist-variables@^7.22.5":
+  version "7.22.5"
+  resolved "https://registry.yarnpkg.com/@babel/helper-hoist-variables/-/helper-hoist-variables-7.22.5.tgz#c01a007dac05c085914e8fb652b339db50d823bb"
+  integrity sha512-wGjk9QZVzvknA6yKIUURb8zY3grXCcOZt+/7Wcy8O2uctxhplmUPkOdlgoNhmdVee2c92JXbf1xpMtVNbfoxRw==
   dependencies:
-    "@babel/types" "^7.18.6"
+    "@babel/types" "^7.22.5"
 
 "@babel/helper-module-imports@^7.18.6":
   version "7.18.6"
@@ -130,16 +153,33 @@
   dependencies:
     "@babel/types" "^7.18.6"
 
+"@babel/helper-split-export-declaration@^7.22.6":
+  version "7.22.6"
+  resolved "https://registry.yarnpkg.com/@babel/helper-split-export-declaration/-/helper-split-export-declaration-7.22.6.tgz#322c61b7310c0997fe4c323955667f18fcefb91c"
+  integrity sha512-AsUnxuLhRYsisFiaJwvp1QF+I3KjD5FOxut14q/GzovUe6orHLesW2C7d754kRm53h5gqrz6sFl6sxc4BVtE/g==
+  dependencies:
+    "@babel/types" "^7.22.5"
+
 "@babel/helper-string-parser@^7.19.4":
   version "7.19.4"
   resolved "https://registry.yarnpkg.com/@babel/helper-string-parser/-/helper-string-parser-7.19.4.tgz#38d3acb654b4701a9b77fb0615a96f775c3a9e63"
   integrity sha512-nHtDoQcuqFmwYNYPz3Rah5ph2p8PFeFCsZk9A/48dPc/rGocJ5J3hAAZ7pb76VWX3fZKu+uEr/FhH5jLx7umrw==
 
+"@babel/helper-string-parser@^7.22.5":
+  version "7.22.5"
+  resolved "https://registry.yarnpkg.com/@babel/helper-string-parser/-/helper-string-parser-7.22.5.tgz#533f36457a25814cf1df6488523ad547d784a99f"
+  integrity sha512-mM4COjgZox8U+JcXQwPijIZLElkgEpO5rsERVDJTc2qfCDfERyob6k5WegS14SX18IIjv+XD+GrqNumY5JRCDw==
+
 "@babel/helper-validator-identifier@^7.18.6", "@babel/helper-validator-identifier@^7.19.1":
   version "7.19.1"
   resolved "https://registry.yarnpkg.com/@babel/helper-validator-identifier/-/helper-validator-identifier-7.19.1.tgz#7eea834cf32901ffdc1a7ee555e2f9c27e249ca2"
   integrity sha512-awrNfaMtnHUr653GgGEs++LlAvW6w+DcPrOliSMXWCKo597CwL5Acf/wWdNkf/tfEQE3mjkeD1YOVZOUV/od1w==
 
+"@babel/helper-validator-identifier@^7.22.20":
+  version "7.22.20"
+  resolved "https://registry.yarnpkg.com/@babel/helper-validator-identifier/-/helper-validator-identifier-7.22.20.tgz#c4ae002c61d2879e724581d96665583dbc1dc0e0"
+  integrity sha512-Y4OZ+ytlatR8AI+8KZfKuL5urKp7qey08ha31L8b3BwewJAoJamTzyvxPR/5D+KkdJCGPq/+8TukHBlY10FX9A==
+
 "@babel/helper-validator-option@^7.18.6":
   version "7.18.6"
   resolved "https://registry.yarnpkg.com/@babel/helper-validator-option/-/helper-validator-option-7.18.6.tgz#bf0d2b5a509b1f336099e4ff36e1a63aa5db4db8"
@@ -163,11 +203,25 @@
     chalk "^2.0.0"
     js-tokens "^4.0.0"
 
-"@babel/parser@^7.20.13", "@babel/parser@^7.20.7":
+"@babel/highlight@^7.22.13":
+  version "7.22.20"
+  resolved "https://registry.yarnpkg.com/@babel/highlight/-/highlight-7.22.20.tgz#4ca92b71d80554b01427815e06f2df965b9c1f54"
+  integrity sha512-dkdMCN3py0+ksCgYmGG8jKeGA/8Tk+gJwSYYlFGxG5lmhfKNoAy004YpLxpS1W2J8m/EK2Ew+yOs9pVRwO89mg==
+  dependencies:
+    "@babel/helper-validator-identifier" "^7.22.20"
+    chalk "^2.4.2"
+    js-tokens "^4.0.0"
+
+"@babel/parser@^7.20.7":
   version "7.20.13"
   resolved "https://registry.yarnpkg.com/@babel/parser/-/parser-7.20.13.tgz#ddf1eb5a813588d2fb1692b70c6fce75b945c088"
   integrity sha512-gFDLKMfpiXCsjt4za2JA9oTMn70CeseCehb11kRZgvd7+F67Hih3OHOK24cRrWECJ/ljfPGac6ygXAs/C8kIvw==
 
+"@babel/parser@^7.22.15", "@babel/parser@^7.23.0":
+  version "7.23.0"
+  resolved "https://registry.yarnpkg.com/@babel/parser/-/parser-7.23.0.tgz#da950e622420bf96ca0d0f2909cdddac3acd8719"
+  integrity sha512-vvPKKdMemU85V9WE/l5wZEmImpCtLqbnTvqDS2U1fJ96KrxoW7KrXhNsNCblQlg8Ck4b85yxdTyelsMUgFUXiw==
+
 "@babel/plugin-syntax-jsx@^7.18.6":
   version "7.18.6"
   resolved "https://registry.yarnpkg.com/@babel/plugin-syntax-jsx/-/plugin-syntax-jsx-7.18.6.tgz#a8feef63b010150abd97f1649ec296e849943ca0"
@@ -207,7 +261,7 @@
     "@babel/plugin-syntax-jsx" "^7.18.6"
     "@babel/types" "^7.20.7"
 
-"@babel/template@^7.18.10", "@babel/template@^7.20.7":
+"@babel/template@^7.20.7":
   version "7.20.7"
   resolved "https://registry.yarnpkg.com/@babel/template/-/template-7.20.7.tgz#a15090c2839a83b02aa996c0b4994005841fd5a8"
   integrity sha512-8SegXApWe6VoNw0r9JHpSteLKTpTiLZ4rMlGIm9JQ18KiCtyQiAMEazujAHrUS5flrcqYZa75ukev3P6QmUwUw==
@@ -216,23 +270,32 @@
     "@babel/parser" "^7.20.7"
     "@babel/types" "^7.20.7"
 
-"@babel/traverse@^7.20.10", "@babel/traverse@^7.20.12", "@babel/traverse@^7.20.13":
-  version "7.20.13"
-  resolved "https://registry.yarnpkg.com/@babel/traverse/-/traverse-7.20.13.tgz#817c1ba13d11accca89478bd5481b2d168d07473"
-  integrity sha512-kMJXfF0T6DIS9E8cgdLCSAL+cuCK+YEZHWiLK0SXpTo8YRj5lpJu3CDNKiIBCne4m9hhTIqUg6SYTAI39tAiVQ==
+"@babel/template@^7.22.15":
+  version "7.22.15"
+  resolved "https://registry.yarnpkg.com/@babel/template/-/template-7.22.15.tgz#09576efc3830f0430f4548ef971dde1350ef2f38"
+  integrity sha512-QPErUVm4uyJa60rkI73qneDacvdvzxshT3kksGqlGWYdOTIUOwJ7RDUL8sGqslY1uXWSL6xMFKEXDS3ox2uF0w==
   dependencies:
-    "@babel/code-frame" "^7.18.6"
-    "@babel/generator" "^7.20.7"
-    "@babel/helper-environment-visitor" "^7.18.9"
-    "@babel/helper-function-name" "^7.19.0"
-    "@babel/helper-hoist-variables" "^7.18.6"
-    "@babel/helper-split-export-declaration" "^7.18.6"
-    "@babel/parser" "^7.20.13"
-    "@babel/types" "^7.20.7"
+    "@babel/code-frame" "^7.22.13"
+    "@babel/parser" "^7.22.15"
+    "@babel/types" "^7.22.15"
+
+"@babel/traverse@^7.20.10", "@babel/traverse@^7.20.12", "@babel/traverse@^7.20.13":
+  version "7.23.2"
+  resolved "https://registry.yarnpkg.com/@babel/traverse/-/traverse-7.23.2.tgz#329c7a06735e144a506bdb2cad0268b7f46f4ad8"
+  integrity sha512-azpe59SQ48qG6nu2CzcMLbxUudtN+dOM9kDbUqGq3HXUJRlo7i8fvPoxQUzYgLZ4cMVmuZgm8vvBpNeRhd6XSw==
+  dependencies:
+    "@babel/code-frame" "^7.22.13"
+    "@babel/generator" "^7.23.0"
+    "@babel/helper-environment-visitor" "^7.22.20"
+    "@babel/helper-function-name" "^7.23.0"
+    "@babel/helper-hoist-variables" "^7.22.5"
+    "@babel/helper-split-export-declaration" "^7.22.6"
+    "@babel/parser" "^7.23.0"
+    "@babel/types" "^7.23.0"
     debug "^4.1.0"
     globals "^11.1.0"
 
-"@babel/types@^7.18.6", "@babel/types@^7.19.0", "@babel/types@^7.20.2", "@babel/types@^7.20.7":
+"@babel/types@^7.18.6", "@babel/types@^7.20.2", "@babel/types@^7.20.7":
   version "7.20.7"
   resolved "https://registry.yarnpkg.com/@babel/types/-/types-7.20.7.tgz#54ec75e252318423fc07fb644dc6a58a64c09b7f"
   integrity sha512-69OnhBxSSgK0OzTJai4kyPDiKTIe3j+ctaHdIGVbRahTLAT7L3R9oeXHC2aVSuGYt3cVnoAMDmOCgJ2yaiLMvg==
@@ -241,6 +304,15 @@
     "@babel/helper-validator-identifier" "^7.19.1"
     to-fast-properties "^2.0.0"
 
+"@babel/types@^7.22.15", "@babel/types@^7.22.5", "@babel/types@^7.23.0":
+  version "7.23.0"
+  resolved "https://registry.yarnpkg.com/@babel/types/-/types-7.23.0.tgz#8c1f020c9df0e737e4e247c0619f58c68458aaeb"
+  integrity sha512-0oIyUfKoI3mSqMvsxBdclDwxXKXAUA8v/apZbc+iSyARYou1o8ZGDxbUYyLFoW2arqS2jDGqJuZvv1d/io1axg==
+  dependencies:
+    "@babel/helper-string-parser" "^7.22.5"
+    "@babel/helper-validator-identifier" "^7.22.20"
+    to-fast-properties "^2.0.0"
+
 "@esbuild/linux-loong64@0.14.54":
   version "0.14.54"
   resolved "https://registry.yarnpkg.com/@esbuild/linux-loong64/-/linux-loong64-0.14.54.tgz#de2a4be678bd4d0d1ffbb86e6de779cde5999028"
@@ -268,6 +340,11 @@
   resolved "https://registry.yarnpkg.com/@jridgewell/resolve-uri/-/resolve-uri-3.1.0.tgz#2203b118c157721addfe69d47b70465463066d78"
   integrity sha512-F2msla3tad+Mfht5cJq7LSXcdudKTWCVYUgw6pLFOOHSTtZlj6SWNYAp+AhuqLmWdBO2X5hPrLcu8cVP8fy28w==
 
+"@jridgewell/resolve-uri@^3.1.0":
+  version "3.1.1"
+  resolved "https://registry.yarnpkg.com/@jridgewell/resolve-uri/-/resolve-uri-3.1.1.tgz#c08679063f279615a3326583ba3a90d1d82cc721"
+  integrity sha512-dSYZh7HhCDtCKm4QakX0xFpsRDqjjtZf/kjI/v3T3Nwt5r8/qz/M19F9ySyOqU94SXBmeG9ttTul+YnR4LOxFA==
+
 "@jridgewell/set-array@^1.0.0", "@jridgewell/set-array@^1.0.1":
   version "1.1.2"
   resolved "https://registry.yarnpkg.com/@jridgewell/set-array/-/set-array-1.1.2.tgz#7c6cf998d6d20b914c0a55a91ae928ff25965e72"
@@ -278,6 +355,19 @@
   resolved "https://registry.yarnpkg.com/@jridgewell/sourcemap-codec/-/sourcemap-codec-1.4.14.tgz#add4c98d341472a289190b424efbdb096991bb24"
   integrity sha512-XPSJHWmi394fuUuzDnGz1wiKqWfo1yXecHQMRf2l6hztTO+nPru658AyDngaBe7isIxEkRsPR3FZh+s7iVa4Uw==
 
+"@jridgewell/sourcemap-codec@^1.4.14":
+  version "1.4.15"
+  resolved "https://registry.yarnpkg.com/@jridgewell/sourcemap-codec/-/sourcemap-codec-1.4.15.tgz#d7c6e6755c78567a951e04ab52ef0fd26de59f32"
+  integrity sha512-eF2rxCRulEKXHTRiDrDy6erMYWqNw4LPdQ8UQA4huuxaQsVeRPFl2oM8oDGxMFhJUWZf9McpLtJasDDZb/Bpeg==
+
+"@jridgewell/trace-mapping@^0.3.17":
+  version "0.3.20"
+  resolved "https://registry.yarnpkg.com/@jridgewell/trace-mapping/-/trace-mapping-0.3.20.tgz#72e45707cf240fa6b081d0366f8265b0cd10197f"
+  integrity sha512-R8LcPeWZol2zR8mmH3JeKQ6QRCFb7XgUhV9ZlGhHLGyg4wpPiPZNQOOWhFZhxKw8u//yTbNGI42Bx/3paXEQ+Q==
+  dependencies:
+    "@jridgewell/resolve-uri" "^3.1.0"
+    "@jridgewell/sourcemap-codec" "^1.4.14"
+
 "@jridgewell/trace-mapping@^0.3.9":
   version "0.3.17"
   resolved "https://registry.yarnpkg.com/@jridgewell/trace-mapping/-/trace-mapping-0.3.17.tgz#793041277af9073b0951a7fe0f0d8c4c98c36985"
@@ -410,7 +500,7 @@ caniuse-lite@^1.0.30001400:
   resolved "https://registry.yarnpkg.com/caniuse-lite/-/caniuse-lite-1.0.30001448.tgz#ca7550b1587c92a392a2b377cd9c508b3b4395bf"
   integrity sha512-tq2YI+MJnooG96XpbTRYkBxLxklZPOdLmNIOdIhvf7SNJan6u5vCKum8iT7ZfCt70m1GPkuC7P3TtX6UuhupuA==
 
-chalk@^2.0.0:
+chalk@^2.0.0, chalk@^2.4.2:
   version "2.4.2"
   resolved "https://registry.yarnpkg.com/chalk/-/chalk-2.4.2.tgz#cd42541677a54333cf541a49108c1432b44c9424"
   integrity sha512-Mti+f9lpJNcwF4tWV8/OrTTtF1gZi+f8FqlyAdouralcFWFQWF2+NgCHShjkCb+IFBLq9buZwE1xckQU4peSuQ==
@@ -673,10 +763,10 @@ ms@2.1.2:
   resolved "https://registry.yarnpkg.com/ms/-/ms-2.1.2.tgz#d09d1f357b443f493382a8eb3ccd183872ae6009"
   integrity sha512-sGkPx+VjMtmA6MX27oA4FBFELFCZZ4S4XqeGOXCv68tT+jb3vk/RyaKWP0PTKyWtmLSM0b+adUTEvbs1PEaH2w==
 
-nanoid@^3.3.4:
-  version "3.3.4"
-  resolved "https://registry.yarnpkg.com/nanoid/-/nanoid-3.3.4.tgz#730b67e3cd09e2deacf03c027c81c9d9dbc5e8ab"
-  integrity sha512-MqBkQh/OHTS2egovRtLk45wEyNXwF+cokD+1YPf9u5VfJiRdAiRwB2froX5Co9Rh20xs4siNPm8naNotSD6RBw==
+nanoid@^3.3.6:
+  version "3.3.6"
+  resolved "https://registry.yarnpkg.com/nanoid/-/nanoid-3.3.6.tgz#443380c856d6e9f9824267d960b4236ad583ea4c"
+  integrity sha512-BGcqMMJuToF7i1rt+2PWSNVnWIkGCU78jBG3RxO/bZlnZPK2Cmi2QaffxGO/2RvWi9sL+FAiRiXMgsyxQ1DIDA==
 
 node-releases@^2.0.6:
   version "2.0.8"
@@ -704,11 +794,11 @@ picomatch@^2.2.2:
   integrity sha512-JU3teHTNjmE2VCGFzuY8EXzCDVwEqB2a8fsIvwaStHhAWJEeVd1o1QD80CU6+ZdEXXSLbSsuLwJjkCBWqRQUVA==
 
 postcss@^8.4.13:
-  version "8.4.21"
-  resolved "https://registry.yarnpkg.com/postcss/-/postcss-8.4.21.tgz#c639b719a57efc3187b13a1d765675485f4134f4"
-  integrity sha512-tP7u/Sn/dVxK2NnruI4H9BG+x+Wxz6oeZ1cJ8P6G/PZY0IKk4k/63TDsQf2kQq3+qoJeLm2kIBUNlZe3zgb4Zg==
+  version "8.4.31"
+  resolved "https://registry.yarnpkg.com/postcss/-/postcss-8.4.31.tgz#92b451050a9f914da6755af352bdc0192508656d"
+  integrity sha512-PS08Iboia9mts/2ygV3eLpY5ghnUcfLV/EXTOW1E2qYxJKGGBUtNjN76FYHnMs36RmARn41bC0AZmn+rR0OVpQ==
   dependencies:
-    nanoid "^3.3.4"
+    nanoid "^3.3.6"
     picocolors "^1.0.0"
     source-map-js "^1.0.2"
 
diff --git a/client/src/client.ts b/client/src/client.ts
index 59904303..8e08108a 100644
--- a/client/src/client.ts
+++ b/client/src/client.ts
@@ -35,7 +35,7 @@ export default class Client extends LanguageClient {
         Client._channel.appendLine(message);
     }
 
-    public saveHighlights(uri: String, parsedRange: vscode.Range[], processingRange: vscode.Range[], processedRange: vscode.Range[]) {
+    public saveHighlights(uri: String, processingRange: vscode.Range[], processedRange: vscode.Range[]) {
         this._decorations.set(uri, processedRange);
     }
 
diff --git a/client/src/extension.ts b/client/src/extension.ts
index 842a867e..d6296328 100644
--- a/client/src/extension.ts
+++ b/client/src/extension.ts
@@ -233,9 +233,8 @@ Path: \`${coqTM.getVsCoqTopPath()}\`
             client.onNotification("vscoq/updateHighlights", (notification) => {
             
                 client.saveHighlights(
-                    notification.uri, 
-                    notification.parsedRange, 
-                    notification.processingRange, 
+                    notification.uri,
+                    notification.processingRange,
                     notification.processedRange
                 );
             
diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts
index 1c02842d..391271e7 100644
--- a/client/src/protocol/types.ts
+++ b/client/src/protocol/types.ts
@@ -54,7 +54,6 @@ export interface ProofViewNotification {
 export interface UpdateHightlightsNotification {
     uri: Uri; 
     parsedRange: Range[];
-    processingRange: Range[];
     processedRange: Range[];
 }
 
diff --git a/client/src/utilities/versioning.ts b/client/src/utilities/versioning.ts
index 5bdfa23d..44ae09fe 100644
--- a/client/src/utilities/versioning.ts
+++ b/client/src/utilities/versioning.ts
@@ -27,9 +27,11 @@ type VersionReq = {
     [index: string]: string
 };
 
+/*  Version requirements for the client. Syntax is client version : minimum server version */
 const versionRequirements : VersionReq = {
     '2.0.0': '2.0.0', 
-    '2.0.1': '2.0.0'
+    '2.0.1': '2.0.0', 
+    '2.0.2': '2.0.0'
 };
 
 //We will add version ranges as we start releasing
diff --git a/docs/developers.md b/docs/developers.md
index c0e86770..36084725 100644
--- a/docs/developers.md
+++ b/docs/developers.md
@@ -103,6 +103,8 @@ To release a new version of VsCoq:
     - flake.nix
     - client/package.json
     - language-server/vscoqtop/lspManager.ml
+
+1.a Don't forget to add the version requirements in `client/src/utilities/versioning.ts`
   
 2. Create a signed tag for the release with the new version number 
 ```shell
diff --git a/flake.nix b/flake.nix
index 7eea371d..71857533 100644
--- a/flake.nix
+++ b/flake.nix
@@ -31,7 +31,7 @@
       ocamlPackages.buildDunePackage {
         duneVersion = "3";
         pname = "vscoq-language-server";
-        version = "2.0.1";
+        version = "2.0.2";
         src = ./language-server;
         buildInputs = [
           coq
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 067417a7..c2ebbb37 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -52,10 +52,8 @@ let inject_em_events events = List.map inject_em_event events
 type events = event Sel.Event.t list
 
 type exec_overview = {
-  parsed : Range.t list;
-  checked : Range.t list;
-  checked_by_delegate : Range.t list;
-  legacy_highlight : Range.t list;
+  processing : Range.t list;
+  processed : Range.t list;
 }
 
 let merge_ranges doc (r1,l) r2 =
@@ -81,20 +79,11 @@ let executed_ranges doc execution_state loc =
     compress_ranges (Document.raw_document doc) @@ List.map (Document.range_of_id doc) l
   in
   let ids_before_loc = List.map (fun s -> s.Document.id) @@ Document.sentences_before doc loc in
-  let ids = List.map (fun s -> s.Document.id) @@ Document.sentences doc in
-  let executed_ids = List.filter (ExecutionManager.is_executed execution_state) ids in
-  let remotely_executed_ids = List.filter (ExecutionManager.is_remotely_executed execution_state) ids in
-  let parsed_ids = List.filter (fun x -> not (List.mem x executed_ids || List.mem x remotely_executed_ids)) ids in
-  let legacy_ids = List.filter (fun x -> ExecutionManager.is_executed execution_state x || ExecutionManager.is_remotely_executed execution_state x) ids_before_loc in
-  log @@ Printf.sprintf "highlight: legacy: %s" (String.concat " " (List.map Stateid.to_string legacy_ids));
-  log @@ Printf.sprintf "highlight: parsed: %s" (String.concat " " (List.map Stateid.to_string parsed_ids));
-  log @@ Printf.sprintf "highlight: parsed + checked: %s" (String.concat " " (List.map Stateid.to_string executed_ids));
-  log @@ Printf.sprintf "highlight: parsed + checked_by_delegate: %s" (String.concat " " (List.map Stateid.to_string remotely_executed_ids));
+  let processed_ids = List.filter (fun x -> ExecutionManager.is_executed execution_state x || ExecutionManager.is_remotely_executed execution_state x) ids_before_loc in
+  log @@ Printf.sprintf "highlight: processed: %s" (String.concat " " (List.map Stateid.to_string processed_ids));
   { 
-    parsed = ranges_of parsed_ids;
-    checked = ranges_of executed_ids;
-    checked_by_delegate = ranges_of remotely_executed_ids;
-    legacy_highlight = ranges_of legacy_ids; 
+    processing = [];
+    processed = ranges_of processed_ids; 
   }
 
 let executed_ranges st =
diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
index e10c2a34..5d3d4d43 100644
--- a/language-server/dm/documentManager.mli
+++ b/language-server/dm/documentManager.mli
@@ -65,10 +65,8 @@ val reset : state -> state * events
 (** resets Coq *)
 
 type exec_overview = {
-  parsed : Range.t list;
-  checked : Range.t list;
-  checked_by_delegate : Range.t list;
-  legacy_highlight : Range.t list;
+  processing : Range.t list;
+  processed : Range.t list;
 }
 
 val executed_ranges : state -> exec_overview
diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml
index 25705f0f..1c7219a0 100644
--- a/language-server/dm/executionManager.ml
+++ b/language-server/dm/executionManager.ml
@@ -154,7 +154,7 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast =
     Sys.(set_signal sigint (Signal_handle(fun _ -> raise Break)));
     let result =
       try Ok(Vernacinterp.interp_entry ~st ast,[])
-      with e when CErrors.noncritical e ->
+      with e -> (* we also catch anomalies *)
         let e, info = Exninfo.capture e in
         Error (e, info) in
     Sys.(set_signal sigint Signal_ignore);
diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
index 555d65c3..b14f9a3b 100644
--- a/language-server/protocol/extProtocol.ml
+++ b/language-server/protocol/extProtocol.ml
@@ -86,7 +86,6 @@ module Notification = struct
 
       type t = {
         uri : DocumentUri.t;
-        parsedRange : Range.t list;
         processingRange : Range.t list;
         processedRange : Range.t list;
       } [@@deriving yojson]
diff --git a/language-server/tests/dm_tests.ml b/language-server/tests/dm_tests.ml
index d2d283ba..df0878e9 100644
--- a/language-server/tests/dm_tests.ml
+++ b/language-server/tests/dm_tests.ml
@@ -101,7 +101,7 @@ let%test_unit "exec.init" =
   let todo = Sel.Todo.(add empty init_events) in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_events todo st in
-  let ranges = (DocumentManager.executed_ranges st).checked in
+  let ranges = (DocumentManager.executed_ranges st).processed in
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.character) ranges in
   [%test_eq: int list] positions [ 0 ];
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.end_.character) ranges in
@@ -115,7 +115,7 @@ let%test_unit "exec.require_error" =
   let todo = Sel.Todo.(add empty init_events) in
   let todo = Sel.Todo.(add todo events) in
   let st = handle_events todo st in
-  let ranges = (DocumentManager.executed_ranges st).checked in
+  let ranges = (DocumentManager.executed_ranges st).processed in
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.character) ranges in
   [%test_eq: int list] positions [ 19 ]
 
@@ -262,7 +262,7 @@ let%test_unit "exec.insert" =
   let st = insert_text st ~loc:0 ~text:"Definition z := 0. " in
   let st = DocumentManager.validate_document st in
   let st, events = DocumentManager.interpret_to_end st in
-  let ranges = (DocumentManager.executed_ranges st).checked in
+  let ranges = (DocumentManager.executed_ranges st).processed in
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.char) ranges in
   check_no_diag st;
   [%test_eq: int list] positions [ 0; 22 ]
diff --git a/language-server/vscoq-language-server.opam b/language-server/vscoq-language-server.opam
index 9dd87164..ba508be1 100644
--- a/language-server/vscoq-language-server.opam
+++ b/language-server/vscoq-language-server.opam
@@ -26,6 +26,7 @@ depends: [
   "sexplib"
   "ppx_yojson_conv"
   "ppx_import"
+  "result" { >= "1.5" }
   "lsp" { >= "1.15"}
   "sel" {>= "0.4.0"}
 ]
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index 0a14082e..970e4bec 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -44,7 +44,7 @@ let conf_request_id = max_int
 
 let server_info = InitializeResult.create_serverInfo
   ~name:"vscoq-language-server"
-  ~version:"2.0.1"
+  ~version:"2.0.2"
   ()
 
 type lsp_event = 
@@ -180,13 +180,12 @@ let publish_diagnostics uri doc =
   output_notification (Std diag_notification)
 
 let send_highlights uri doc =
-  let { Dm.DocumentManager.parsed; checked; checked_by_delegate; legacy_highlight } =
+  let { Dm.DocumentManager.processing;  processed } =
     Dm.DocumentManager.executed_ranges doc in
   let notification = Notification.Server.UpdateHighlights {
     uri;
-    parsedRange = parsed;
-    processingRange = checked;
-    processedRange = legacy_highlight;
+    processingRange = processing;
+    processedRange = processed;
   }
   in
   output_json @@ Jsonrpc.Notification.yojson_of_t @@ Notification.Server.to_jsonrpc notification
@@ -234,21 +233,24 @@ let textDocumentDidOpen params =
 let textDocumentDidChange params =
   let Lsp.Types.DidChangeTextDocumentParams.{ textDocument; contentChanges } = params in
   let uri = textDocument.uri in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  let mk_text_edit TextDocumentContentChangeEvent.{ range; text } =
-    Option.get range, text
-  in
-  let text_edits = List.map mk_text_edit contentChanges in
-  let st = Dm.DocumentManager.apply_text_edits st text_edits in
-  let (st, events) = 
-    if !check_mode <> Settings.Mode.Manual then 
-      Dm.DocumentManager.interpret_in_background st 
-    else 
-      (st, [])
-  in
-  Hashtbl.replace states (DocumentUri.to_path uri) st;
-  update_view uri st;
-  inject_dm_events (uri, events)
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+    | None -> log @@ "[textDocumentDidChange] ignoring event on non-existing document"; []
+    | Some st ->
+      let mk_text_edit TextDocumentContentChangeEvent.{ range; text } =
+        Option.get range, text
+      in
+      let text_edits = List.map mk_text_edit contentChanges in
+      let st = Dm.DocumentManager.apply_text_edits st text_edits in
+      let (st, events) = 
+        if !check_mode <> Settings.Mode.Manual then 
+          Dm.DocumentManager.interpret_in_background st 
+        else 
+          (st, [])
+      in
+      Hashtbl.replace states (DocumentUri.to_path uri) st;
+      update_view uri st;
+      inject_dm_events (uri, events)
+
 
 let textDocumentDidSave params =
   [] (* TODO handle properly *)
@@ -259,14 +261,17 @@ let textDocumentDidClose params =
 let textDocumentHover id params = 
   let Lsp.Types.HoverParams.{ textDocument; position } = params in
   let open Yojson.Safe.Util in
-  let st = Hashtbl.find states (DocumentUri.to_path textDocument.uri) in 
-  match Dm.DocumentManager.hover st position with
-  | Some contents -> Ok (Some (Hover.create ~contents:(`MarkupContent contents) ()))
-  | _ -> Ok None (* FIXME handle error case properly *)
+  match Hashtbl.find_opt states (DocumentUri.to_path textDocument.uri) with
+  | None -> log @@ "[textDocumentHover] ignoring event on non existing document"; Ok None (* FIXME handle error case properly *)
+  | Some st ->
+    match Dm.DocumentManager.hover st position with
+    | Some contents -> Ok (Some (Hover.create ~contents:(`MarkupContent contents) ()))
+    | _ -> Ok None (* FIXME handle error case properly *)
 
 let progress_hook uri () =
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  update_view uri st
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "ignoring non existant document"
+  | Some st -> update_view uri st
 
 let mk_proof_view_event uri position = 
   Sel.now ~priority:Dm.PriorityManager.proof_view (SendProofView (uri, position))
@@ -278,44 +283,50 @@ let mk_move_cursor_event uri range =
 let coqtopInterpretToPoint params =
   let Notification.Client.InterpretToPointParams.{ textDocument; position } = params in
   let uri = textDocument.uri in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  let (st, events) = Dm.DocumentManager.interpret_to_position ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous) ~stateful:(!check_mode = Settings.Mode.Manual) st position in
-  Hashtbl.replace states (DocumentUri.to_path uri) st;
-  update_view uri st;
-  let sel_events = inject_dm_events (uri, events) in
-  sel_events @ [ mk_proof_view_event uri (Some position)]
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[interpretToPoint] ignoring event on non existant document"; []
+  | Some st ->
+    let (st, events) = Dm.DocumentManager.interpret_to_position ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous) ~stateful:(!check_mode = Settings.Mode.Manual) st position in
+    Hashtbl.replace states (DocumentUri.to_path uri) st;
+    update_view uri st;
+    let sel_events = inject_dm_events (uri, events) in
+    sel_events @ [ mk_proof_view_event uri (Some position)]
  
 let coqtopStepBackward params =
   let Notification.Client.StepBackwardParams.{ textDocument = { uri } } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  let (st, events) = Dm.DocumentManager.interpret_to_previous ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous) st in
-  let range = Dm.DocumentManager.observe_id_range st in
-  Hashtbl.replace states (DocumentUri.to_path uri) st;
-  update_view uri st; 
-  if !check_mode = Settings.Mode.Manual then
-    match range with 
-    | None ->
-      inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] (* how can this do anything? isn't observe_id None? *)
-    | Some range -> 
-      [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] 
-  else 
-    inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] (* isn't observe_id none in continuous mode? If so, how does this do anything? *)
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[stepBackward] ignoring event on non existant document"; []
+  | Some st ->
+    let (st, events) = Dm.DocumentManager.interpret_to_previous ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous) st in
+    let range = Dm.DocumentManager.observe_id_range st in
+    Hashtbl.replace states (DocumentUri.to_path uri) st;
+    update_view uri st; 
+    if !check_mode = Settings.Mode.Manual then
+      match range with 
+      | None ->
+        inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] (* how can this do anything? isn't observe_id None? *)
+      | Some range -> 
+        [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] 
+    else 
+      inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] (* isn't observe_id none in continuous mode? If so, how does this do anything? *)
 
 let coqtopStepForward params =
   let Notification.Client.StepForwardParams.{ textDocument = { uri } } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  let (st, events) = Dm.DocumentManager.interpret_to_next ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous)  st in
-  let range = Dm.DocumentManager.observe_id_range st in
-  Hashtbl.replace states (DocumentUri.to_path uri) st;
-  update_view uri st; 
-  if !check_mode = Settings.Mode.Manual then
-    match range with 
-    | None ->
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "ignoring event on non existant document"; []
+  | Some st ->
+    let (st, events) = Dm.DocumentManager.interpret_to_next ~skip_proofs:(!check_mode = Settings.Mode.SemiContinuous) st in
+    let range = Dm.DocumentManager.observe_id_range st in
+    Hashtbl.replace states (DocumentUri.to_path uri) st;
+    update_view uri st; 
+    if !check_mode = Settings.Mode.Manual then
+      match range with 
+      | None ->
+        inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
+      | Some range -> 
+        [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] 
+    else 
       inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
-    | Some range -> 
-      [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] 
-  else 
-    inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]
   
   let make_CompletionItem i item : CompletionItem.t = 
     let (label, insertText, typ, path) = Dm.CompletionItems.pp_completion_item item in
@@ -336,74 +347,88 @@ let textDocumentCompletion id params =
     return_completion ~isIncomplete:false ~items:[], []
   else
   let Lsp.Types.CompletionParams.{ textDocument = { uri }; position } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  match Dm.DocumentManager.get_completions st position with
-  | Ok completionItems -> 
-    let items = List.mapi make_CompletionItem completionItems in
-    return_completion ~isIncomplete:false ~items, []
-  | Error e -> 
-    let message = e in
-    Error(message), []
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[textDocumentCompletion]ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some st -> 
+    match Dm.DocumentManager.get_completions st position with
+    | Ok completionItems -> 
+      let items = List.mapi make_CompletionItem completionItems in
+      return_completion ~isIncomplete:false ~items, []
+    | Error e -> 
+      let message = e in
+      Error(message), []
 
 let coqtopResetCoq id params =
   let Request.Client.ResetParams.{ textDocument = { uri } } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  let st, events = Dm.DocumentManager.reset st in
-  let (st, events') =
-    if !check_mode <> Settings.Mode.Manual then
-      Dm.DocumentManager.interpret_in_background st
-    else
-      (st, [])
-  in
-  Hashtbl.replace states (DocumentUri.to_path uri) st;
-  update_view uri st;
-  Ok(()), (uri,events@events') |> inject_dm_events
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[resetCoq] ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some st -> 
+    let st, events = Dm.DocumentManager.reset st in
+    let (st, events') =
+      if !check_mode <> Settings.Mode.Manual then
+        Dm.DocumentManager.interpret_in_background st
+      else
+        (st, [])
+    in
+    Hashtbl.replace states (DocumentUri.to_path uri) st;
+    update_view uri st;
+    Ok(()), (uri,events@events') |> inject_dm_events
 
 let coqtopInterpretToEnd params =
   let Notification.Client.InterpretToEndParams.{ textDocument = { uri } } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  let (st, events) = Dm.DocumentManager.interpret_to_end ~skip_proofs:false st in
-  Hashtbl.replace states (DocumentUri.to_path uri) st;
-  update_view uri st;
-  inject_dm_events (uri,events) @ [ mk_proof_view_event uri None]
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[interpretToEnd] ignoring event on non existant document"; []
+  | Some st ->
+    let (st, events) = Dm.DocumentManager.interpret_to_end ~skip_proofs:false st in
+    Hashtbl.replace states (DocumentUri.to_path uri) st;
+    update_view uri st;
+    inject_dm_events (uri,events) @ [ mk_proof_view_event uri None]
 
 let coqtopLocate id params = 
   let Request.Client.LocateParams.{ textDocument = { uri }; position; pattern } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  Dm.DocumentManager.locate st position ~pattern, []
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[locate] ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some st ->
+    Dm.DocumentManager.locate st position ~pattern, []
 
 let coqtopPrint id params = 
   let Request.Client.PrintParams.{ textDocument = { uri }; position; pattern } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  Dm.DocumentManager.print st position ~pattern, []
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[print] ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some st -> Dm.DocumentManager.print st position ~pattern, []
 
 let coqtopAbout id params =
   let Request.Client.AboutParams.{ textDocument = { uri }; position; pattern } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  Dm.DocumentManager.about st position ~pattern, []
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[about] ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some st -> Dm.DocumentManager.about st position ~pattern, []
 
 let coqtopCheck id params =
   let Request.Client.CheckParams.{ textDocument = { uri }; position; pattern } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  Dm.DocumentManager.check st position ~pattern, []
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[check] ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some st -> Dm.DocumentManager.check st position ~pattern, []
 
 let coqtopSearch id params =
   let Request.Client.SearchParams.{ textDocument = { uri }; id; position; pattern } = params in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  try
-    let notifications = Dm.DocumentManager.search st ~id position pattern in
-    Ok(()), inject_notifications notifications
-  with e ->
-    let e, info = Exninfo.capture e in
-    let message = Pp.string_of_ppcmds @@ CErrors.iprint (e, info) in
-    Error(message), []
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[search] ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some st ->
+    try
+      let notifications = Dm.DocumentManager.search st ~id position pattern in
+      Ok(()), inject_notifications notifications
+    with e ->
+      let e, info = Exninfo.capture e in
+      let message = Pp.string_of_ppcmds @@ CErrors.iprint (e, info) in
+      Error(message), []
 
 let sendDocumentState id params = 
   let Request.Client.DocumentStateParams.{ textDocument } = params in
   let uri = textDocument.uri in
-  let st = Hashtbl.find states (DocumentUri.to_path uri) in
-  let document = Dm.DocumentManager.Internal.string_of_state st in
-  Ok Request.Client.DocumentStateResult.{ document }, []
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[documentState] ignoring event on non existant document"; Error("Document does not exist"), []
+  | Some st -> let document = Dm.DocumentManager.Internal.string_of_state st in
+    Ok Request.Client.DocumentStateResult.{ document }, []
 
 let workspaceDidChangeConfiguration params = 
   let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in
@@ -536,14 +561,17 @@ let handle_event = function
   | LogEvent e ->
     Dm.Log.handle_event e; []
   | SendProofView (uri, position) -> 
-    let st = Hashtbl.find states (DocumentUri.to_path uri) in
-    let proof = Dm.DocumentManager.get_proof st !diff_mode position in
-    let messages = Dm.DocumentManager.get_messages st position in
-    let messages =
-      if !full_messages then messages
-      else List.filter (fun (sev,_) -> sev == DiagnosticSeverity.Information) messages
-    in
-    send_proof_view Notification.Server.ProofViewParams.{ proof; messages }; []
+    begin match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+    | None -> log @@ "ignoring event on non existant document"; []
+    | Some st ->
+      let proof = Dm.DocumentManager.get_proof st !diff_mode position in
+      let messages = Dm.DocumentManager.get_messages st position in
+      let messages =
+        if !full_messages then messages
+        else List.filter (fun (sev,_) -> sev == DiagnosticSeverity.Information) messages
+      in
+      send_proof_view Notification.Server.ProofViewParams.{ proof; messages }; []
+    end
   | SendMoveCursor (uri, range) -> 
     send_move_cursor uri range; []