Update Docs

Author: rcosta358

pages/annotations/external-refinements-for.md

@@ -8,9 +8,8 @@ description: Learn how to refine external libraries that cannot be annotated dir
 
 # @ExternalRefinementsFor
 
-External refinements let you add refinements to an existing class that you cannot modify.
-
-For this, the `@ExternalRefinementsFor` annotation is used to specify the qualified name of the class you want to refine in a separate interface. This makes it possible to refine external classes from the Java standard library, third-party dependencies, or shared APIs without modifying their source code.
+External refinements let you add refinements to existing classes and interfaces that you cannot directly annotate, such as ones from the Java standard library, third-party dependencies, or shared APIs, without actually modifying their source code.
+For this, the `@ExternalRefinementsFor` annotation is used to specify the qualified name of the class or interface you want to refine in a separate interface.
 
 ```java
 import liquidjava.specification.*;

pages/annotations/refinement-alias.md

@@ -24,4 +24,4 @@ public class MyClass {
 }
 ```
 
-This helps keep contracts shorter and easier to maintain by giving common constraints a domain-specific name.
+This helps keep contracts shorter and easier to maintain by giving common constraints a domain-specific name and reusing them in.

pages/annotations/refinements.md

@@ -46,7 +46,7 @@ Refinement predicates use a language similar to Java, where you can write boolea
 | Ghosts | `ghost(...args)` | `@Refinement("0 <= _ < size(this)") int index` |
 | Aliases | `Alias(...args)` | `@Refinement("Positive(_)") int c = 10` |
 | Literals | `true` `false` `0` `1.5` | `@Refinement("true") void print()` |
-| Enums | `EnumType.VAlue` | `@Refinement("_ == Status.Open") Status status` |
+| Enums | `EnumType.Value` | `@Refinement("_ == Status.Open") Status status` |
 | Static final fields | `Type.FIELD` | `@Refinement("_ <= Integer.MAX_VALUE") int value` |
 
 LiquidJava currently supports a small set of types in refinements:

pages/vscode-extension/status-bar-indicator.md

@@ -8,13 +8,14 @@ description: Check out the indicator that shows the current state of LiquidJava.
 
 # Status Bar Indicator
 
-The extension displays an indicator in the status bar in the bottom-left of the editor that shows the current LiquidJava state inside VS Code, with four possible states:
+The extension displays an indicator in the status bar in the bottom-left of the editor that shows the current LiquidJava state inside VS Code, with five possible states:
 
 | Status | Description |
 | --- | --- |
 | `loading` | The verification is in progress |
 | `passed` | The verification succeeded |
 | `failed` | The verification failed with one or more errors |
+| `crashed` | The verification crashed with an unexpected error |
 | `stopped` | The extension was stopped, failed to connect, or lost connection with the language server |
 
 ![Status Bar Indicator]({{ 'assets/images/status-bar-indicator.gif' | relative_url }})

pages/vscode-extension/webview/context-debugger.md

@@ -32,4 +32,4 @@ Clicking a variable in the context debugger highlights that variable in the edit
 
 ## Failed Refinements
 
-When a refinement or state refinement fails, the context debugger also shows the expected type in red after the turnstile (`⊢`). Hovering that expected type reveals the corresponding error message and clicking on it highlights the failure in the editor.
+When a refinement or state refinement fails, the context debugger also shows the expected type in red after the turnstile (`⊢`). Clicking this expected type makes the webview navigate to the corresponding error in the diagnostic explorer.

pages/vscode-extension/webview/diagnostic-explorer.md

@@ -13,5 +13,3 @@ The diagnostic explorer provides an interactive view of LiquidJava diagnostics w
 For refinement errors, LiquidJava performs expression simplification with traceable simplification steps. This makes it possible to progressively expand simplifications. Clicking a value can expand it into its origin expression, and clicking a variable can jump to its location in the editor. This makes simplification traceable instead of showing only the final reduced expression.
 
 ![Diagnostic Explorer]({{ 'assets/images/diagnostic-explorer.gif' | relative_url }})
-
-In refinement and state refinement errors, an expandable section displays the context variables (also called translation table). This table maps the internal variable names created during the typechecking to the original source code variables and placement in the code. When clicked, each entry highlights the corresponding part of the source code that corresponds to that variable.