Merge remote-tracking branch 'origin/master'

Signed-off-by: Y <git@younes.io>

Author: younes-io

languages/pluscal-snippets.json

@@ -35,17 +35,44 @@
         ],
         "description": "If block"
     },
+    "Elsif": {
+        "prefix": "elsif",
+        "body": [
+            "elsif ${1:condition} then",
+            "\t${0:body}"
+        ],
+        "description": "Elsif clause"
+    },
+    "Else": {
+        "prefix": "else",
+        "body": [
+            "else",
+            "\t${0:body}"
+        ],
+        "description": "Else clause"
+    },
     "If-Else": {
         "prefix": "ifel",
         "body": [
             "if ${1:condition} then",
             "\t${2:body}",
-            "elseif",
+            "else",
             "\t${0:body}",
             "end if;"
         ],
         "description": "If-else block"
     },
+    "If-Elsif": {
+        "prefix": "ifelsif",
+        "body": [
+            "if ${1:condition} then",
+            "\t${2:body}",
+            "elsif ${3:condition} then",
+            "\t${0:body}",
+            "end if;"
+        ],
+        "description": "If-elsif block"
+    },
     "With": {
         "prefix": "with",
         "body": [
@@ -73,6 +100,16 @@
             "begin",
             "\t${0:body}",
             "end process;"
-        ]
+        ],
+        "description": "Create new process"
+    },
+    "Procedure": {
+        "prefix": "procedure",
+        "body": [
+            "procedure ${1:name}(${2:params}) begin",
+            "\t${0:body}",
+            "end procedure;"
+        ],
+        "description": "Create new procedure"
     }
 }

package.json

@@ -578,6 +578,12 @@
                     "default": false,
                     "markdownDescription": "Enable filesystem tools (list_directory, read_file, write_file) in the MCP server. These tools allow reading and writing files within the workspace. Restart VSCode to apply changes. It is unlikely that you will want to enable this, because VSCode and Cursor already provide filesystem operations."
                 },
+                "tlaplus.mcp.enableKnowledgeBaseTools": {
+                    "type": "boolean",
+                    "scope": "window",
+                    "default": false,
+                    "markdownDescription": "Enable the knowledge-base *tools* in the MCP server in addition to the knowledge-base *resources*. The two tools tlaplus_mcp_knowledge_list and tlaplus_mcp_knowledge_get allow you to search and read TLA+ knowledge-base articles as MCP tools. Restart VSCode to apply the changes. You’ll rarely need to enable this option, since both VSCode and Cursor already support MCP resources."
+                },
                 "tlaplus.pdf.convertCommand": {
                     "default": "pdflatex",
                     "type": "string",

resources/knowledgebase/tla-animations.md

@@ -232,9 +232,18 @@ Legend == Group(<<
         ("font-size" :> "12px" @@ "fill" :> "#666"))
 >>, <<>>)
 
+\* Step number display
+StepNumber == 
+    Text(90 + Cardinality(Nodes) * NodeSpacing, 190, 
+         "Step " \o ToString(TLCGet("level")), 
+         ("text-anchor" :> "end" @@ 
+          "font-size" :> "12px" @@ 
+          "font-family" :> "monospace" @@ 
+          "fill" :> "#666"))
+
 \* Main animation view
 AnimView == 
-    Group(<<Legend>> \o [i \in 1..Len(NodeSeq) |-> NodeVis(NodeSeq[i])], <<>>)
+    Group(<<Legend, StepNumber>> \o [i \in 1..Len(NodeSeq) |-> NodeVis(NodeSeq[i])], <<>>)
 
 \* TLC animation export
 AnimAlias ==
@@ -625,6 +634,32 @@ When creating TLA+ animations composed of multiple SVG frames, **it is essential
 
 If the `viewBox` cannot be determined in advance, perform an initial pass to measure the maximum extents across all frames, then use those dimensions consistently for the final rendering.
 
+### 6. Always Display Step Numbers
+
+**Every animation frame must include a step number** to help track progression through the state space. The step number should appear in a consistent location across all frames, similar to how page numbers appear in documents.
+
+```tla
+\* Add step number in bottom-right corner
+StepNumber == 
+    Text(viewBoxWidth - 30, viewBoxHeight - 10, 
+         "Step " \o ToString(TLCGet("level")), 
+         ("text-anchor" :> "end" @@ 
+          "font-size" :> "12px" @@ 
+          "font-family" :> "monospace" @@ 
+          "fill" :> "#666"))
+
+\* Include in your AnimView
+AnimView == 
+    Group(<<YourMainVisualization, StepNumber>>, <<>>)
+```
+
+**Best practices for step numbers:**
+- Position consistently (typically bottom-right or top-right corner)
+- Use monospace font for alignment
+- Choose subtle color that doesn't interfere with main content
+- Include "Step" prefix for clarity
+- Ensure adequate padding from frame edges
+
 ## Troubleshooting
 
 ### Common Issues and Solutions
@@ -859,7 +894,13 @@ Empty ==
    Image(13, 20, 140, 140, "assets/battery-empty-symbolic-svgrepo-com.svg",
          IF batteryLevel < 0 THEN <<>> ELSE [hidden |-> "true"])
 
-AnimView == Group(<<Left, Right, Battery, Chargers, Empty>>, [i \in {} |-> {}])
+\* Step number in bottom-right corner
+StepNumber == 
+    Text(220, 190, "Step " \o ToString(TLCGet("level")), 
+         ("text-anchor" :> "end" @@ "font-size" :> "12px" @@ 
+          "font-family" :> "monospace" @@ "fill" :> "#666"))
+
+AnimView == Group(<<Left, Right, Battery, Chargers, Empty, StepNumber>>, [i \in {} |-> {}])
 
 AnimAlias ==
     [left |-> left, right |-> right, 
@@ -1011,8 +1052,14 @@ FlowArrows ==
                        "fill" :> "#6c757d"))
     IN Group(<<arrow1, arrow2>>, <<>>)
 
+\* Step number in bottom-right corner
+StepNumber == 
+    Text(550, 340, "Step " \o ToString(TLCGet("level")), 
+         ("text-anchor" :> "end" @@ "font-size" :> "12px" @@ 
+          "font-family" :> "monospace" @@ "fill" :> "#666"))
+
 AnimView == 
-    Group(<<ProducerLabel, BufferLabel, ConsumerLabel, BufferStatus, FlowArrows>> \o 
+    Group(<<ProducerLabel, BufferLabel, ConsumerLabel, BufferStatus, FlowArrows, StepNumber>> \o 
           Prod \o Buffer \o Conss, <<>>)
 
 AnimAlias ==
@@ -1412,5 +1459,6 @@ AnimAlias ==
 5. **Layout Calculations**: Mathematical positioning for organized displays
 6. **Grouped Elements**: Logical grouping of related visual components
 7. **Text Overlays**: State information displayed as text labels
+8. **Step Number Display**: Every frame includes `TLCGet("level")` for progression tracking
 
 These examples demonstrate the full range of TLA+ animation capabilities, from simple state indicators to complex distributed system visualizations.