Remove outdated documentation.

DESIGN.md

@@ -40,22 +40,6 @@ out of the box.
 
 # Main event handlers
 
-## Standard LSP Events
-
-### onInitialize
-
-Raised once, when the extension is initialized by the client.
-
-The servers reads the workspace configuration (.fst.config.json) if any,
-and sets up its state.
-
-* `const documentStates: Map<string, IDEState>`: A map from the URI of each open document
-   to the IDE state for it.
-
-* `const workspaceConfigs: Map<string, FStarConfig>`: A parsed .fst.config.json file, if any,
-   for all open workspace folders.
-
-
 ### onDidOpen
 
 server.ts launches two F* processes per open document:
@@ -65,14 +49,6 @@ server.ts launches two F* processes per open document:
 * `fstar_lax_ide`: This is used to handle on-the-fly checking, symbol resolution etc.
    Fragments of a document are only lax-checked by this F* process.
 
-### onDidChangeContent
-
-`fstar_lax_ide` is called to check the suffix of the document that has changed
-
-### onDidSave
-
-`fstar_ide` is called to fully check the suffix of the document that has not yet been checked.
-
 ### onHover
 
 `fstar_lax_ide` is called to resolve the type of the symbol under the cursor.
@@ -83,11 +59,7 @@ server.ts launches two F* processes per open document:
 
 ### onDocumentRangeFormatting
 
-Re-formatting a document selection is a synchronous event in LSP.
-However, interactions with `fstar_lax_ide` and `fstar_ide` are asychronous.
-
-Since re-formatting is a purely syntactic task and does not rely on any specific
-F* typechecker state, for this event, we spawn a new process fstar.exe synchronously, 
+We spawn a new process fstar.exe,
 and send it the `format` message with the content of the current selection, returning
 its result as the reformatted content.
 

README.md

@@ -3,29 +3,20 @@
 This VS Code extension provides support for interactively editing and
 checking F* files incrementally.
 
-It is adapted from the lsp-sample provided by VS Code:
-https://github.com/microsoft/vscode-extension-samples/tree/main/lsp-sample
-
-The vsfstar extension was also a source of inspiration and initial guidance:
-https://github.com/artagnon/vsfstar
-
 ## Installation
 
-An initial release is available on the VSCode marketplace: https://marketplace.visualstudio.com/items?itemName=FStarLang.fstar-vscode-assistant
+An release is available on the VSCode marketplace: https://marketplace.visualstudio.com/items?itemName=FStarLang.fstar-vscode-assistant
 
 You need to have a working F* installation, where `fstar.exe` and `z3` are in your path.
 
-Use the latest release of F* : https://github.com/FStarLang/FStar/releases/tag/v2023.04.25
-
+Use the latest release of F*: https://github.com/FStarLang/FStar/releases/tag/v2024.01.13
 
 If you have installed F* or Z3 using opam, make sure you start VS Code from inside the opam environment after running `eval $(opam env)`.
 If you are using WSL, the WSL plugin for VS Code will run your `bashrc`, and it is enough to put the `eval $(opam env)` there.
 (When only Z3 is missing, you will get a message like `ERROR: F* flycheck process exited with code 1`.)
 
-
 The command `fstar.exe --ide A.fst` should print the following protocol-info (Look at the full strig, it ends with ""full-buffer","format","restart-solver", "cancel"]}".
 
-
 ```json
 {"kind":"protocol-info","version":2,"features":["autocomplete","autocomplete/context","compute","compute/reify","compute/pure-subterms","describe-protocol","describe-repl","exit","lookup","lookup/context","lookup/documentation","lookup/definition","peek","pop","push","search","segment","vfs-add","tactic-ranges","interrupt","progress","full-buffer","format","restart-solver", "cancel"]}
 ```
@@ -144,15 +135,13 @@ highlighted with "squigglies" in the document.
 
 You can hover on an identifer to see its type.
 
-Note, the first time you hover on an identifer, you may see a message "Loading symbol: ..."
-
-If F* can resolve the symbol, the next time you hover on it, you should see its fully qualified name and type.
+If F* can resolve the symbol, you should see its fully qualified name and type.
 
-You can also jump to the definition, using the menu option or by pressing F12.
+You can also jump to the definition, using ctrl+click or by pressing F12.
 
 ### Proof state dumps for tactic execution
 
-If you are using tactics, you can hover on tactic line to see the last proof state dumped at that line
+If you are using tactics, you can hover on tactic line to see the last proof state dumped at that line.
 
 ### Completions
 
@@ -207,7 +196,7 @@ If you have a .fst.config.json file in a folder, you can open the folder as a wo
 and all F* files in that workspace using the .fst.config.json file as the configuration
 for launching `fstar.exe`. Here is a sample .fst.config.json file:
 
-```
+```json
 { "fstar_exe":"fstar.exe",
   "options":["--cache_dir", ".cache.boot", "--no_location_info", "--warn_error", "-271-272-241-319-274"],
   "include_dirs":["../ulib", "basic", "basic/boot", "extraction", "fstar", "parser", "prettyprint", "prettyprint/boot", "reflection", "smtencoding", "syntax", "tactics", "tosyntax", "typechecker", "tests", "tests/boot"] }
@@ -254,8 +243,6 @@ Then, `Project.fst.config.json` applies to `Main.fst` and `A.fst`,
 while `B.fst.config.json` applies to `B.fst`.
 
 
-
-
 ### Working with the vscode remote ssh extension
 
 This extension (by default) works well with the
@@ -339,8 +326,6 @@ Also, a disclaimer: This is my first non-trivial VSCode extension and I may well
 conventions that extension users may expect. Any contributions or suggestions to bring it more in
 line with existing conventions are most welcome.
 
-Also, I have been using this extension myself only for the past couple of weeks, while developing it. 
-
 ## Running it in development mode
 
 - Run `npm install` in this folder. This installs all necessary npm
@@ -350,21 +335,9 @@ Also, I have been using this extension myself only for the past couple of weeks,
 
 - Open VS Code on this folder.
 
-- Press Ctrl+Shift+B to start compiling the client and server in
-  [watch
-  mode](https://code.visualstudio.com/docs/editor/tasks#:~:text=The%20first%20entry%20executes,the%20HelloWorld.js%20file.).
-
-- Switch to the Run and Debug View in the Sidebar (Ctrl+Shift+D).
-
-- Select `Launch Client` from the drop down (if it is not already).
+- Press F5 to build the extension and run it in a new vscode window with the built extension.
 
-- Press ▷ to run the launch config (F5).
+## Acknowledgements
 
-- In the [Extension Development
-  Host](https://code.visualstudio.com/api/get-started/your-first-extension#:~:text=Then%2C%20inside%20the%20editor%2C%20press%20F5.%20This%20will%20compile%20and%20run%20the%20extension%20in%20a%20new%20Extension%20Development%20Host%20window.)
-  instance of VSCode, open a document with a `.fst` or `.fsti` filename extension.
-
-  - You should see some syntax highlighting
-  - And, as you type, you should see F* checking your code and providing diagnostics interactively
-
-- You might also want to read DESIGN.md, if you want to contribute.
+The vsfstar extension was also a source of inspiration and initial guidance:
+https://github.com/artagnon/vsfstar