fix highlighting bugs, minor visuals in usage

Author: fhackett

astro.config.mjs

@@ -11,17 +11,26 @@ export default defineConfig({
     shikiConfig: {
       theme: 'dracula',
       langs: [
-      // important: a language's dependencies must be loaded first, or explosion
-      {
-        id: 'mpcal',
-        scopeName: 'source.tlaplus.mpcal',
-        grammar: JSON.parse(readFileSync('highlighting/mpcal.tmLanguage.json'))
-      }, {
-        id: 'tlaplus',
-        scopeName: 'source.tlaplus',
-        grammar: JSON.parse(readFileSync('./highlighting/tlaplus.tmLanguage.json')),
-        aliases: ['tla']
-      }],
+        // important: a language's dependencies must be loaded first, or explosion
+        {
+          id: 'tlaplus',
+          scopeName: 'source.tlaplus',
+          grammar: JSON.parse(readFileSync('./highlighting/tlaplus.tmLanguage.json')),
+          aliases: ['tla'],
+        },
+        {
+          id: 'pluscal',
+          scopeName: 'source.tlaplus.pluscal',
+          grammar: JSON.parse(readFileSync('./highlighting/pluscal.tmLanguage.json')),
+          embeddedLangs: ['tlaplus'],
+        },
+        {
+          id: 'mpcal',
+          scopeName: 'source.tlaplus.mpcal',
+          grammar: JSON.parse(readFileSync('./highlighting/mpcal.tmLanguage.json')),
+          embeddedLangs: ['tlaplus', 'pluscal'],
+        },
+      ],
       wrap: true
     }
   }

highlighting/tlaplus.tmLanguage.json

@@ -105,42 +105,6 @@
 			"begin": "\\\\\\*",
 			"end": "$"
 		},
-		"comment-block": {
-			"name": "comment.block.tlaplus",
-			"begin": "\\(\\*",
-			"end": "\\*\\)",
-			"patterns": [
-				{
-					"begin": "(\\-\\-)(mpcal)(\\s+)(\\w+)(\\s*)({)",
-					"end": "}",
-					"beginCaptures": {
-						"2": {
-							"name": "keyword.other.mpcal"
-						}
-					},
-					"name": "meta.embedded.block.mpcal",
-					"patterns": [{
-						"include": "source.tlaplus.mpcal"
-					}]
-				},
-				{
-					"begin": "(\\-\\-)(algorithm|fair\\s+algorithm)(\\s+)(\\w+)(\\s*)({)",
-					"end": "}",
-					"beginCaptures": {
-						"2": {
-							"name": "keyword.other.pluscal" 
-						}
-					},
-					"name": "meta.embedded.block.pluscal",
-					"patterns": [{
-						"include": "source.tlaplus.pluscal"
-					}]
-				},
-				{
-					"include": "#comment-block"
-				}
-			]
-		},
 		"operators-4-char": {
 			"name": "keyword.operator.tlaplus",
 			"match": "(\\(\\\\X\\)|-\\+-\\>)"

src/pages/usage.mdx

@@ -129,33 +129,34 @@ In this section, we'll go over how to verify a load balancer. We'll get PGo's ex
    ```
 
 3. Open the load balancer specification in the TLA+ toolbox (by going to File > Open Spec > Add New Spec... > Browse...).
-   <div class="flex flex-row">
+   <div class="flex flex-row flex-wrap">
     <Figure src={img_add_new_spec} alt="Add New Spec..." client:load />
     <Figure src={img_browse} alt="Browse..." client:load />
    </div>
 
 4. Press `Ctrl-t` to compile PlusCal to TLA+ (output in the same file).
 
 5. On the left pane, right click on models, select New Models..., and name the new model. The created model is opened on the right pane.
-   <div class="flex flex-row">
+   <div class="flex flex-row flex-wrap">
     <Figure src={img_new_model} alt="New model..." client:load />
     <Figure src={img_new_model_dialog} alt="New model dialog..." client:load />
    </div>
 
-6. In What is the model? on the lower right side, double click on each item and fill in the following values.
-   ```
-   |   Item      | Value |
-   | ----------- | ----- |
-   | GET_PAGE    |     1 |
-   | NUM_CLIENTS |     1 |
-   | NUM_SERVERS |     1 |
-   | BUFFER_SIZE |     1 |
-   | WEB_PAGE    |     1 |
-   ```
+6. In "What is the model?" on the lower right side, double click on each item and fill in the following values.
+
+   <div class="max-w-prose">
+    |   Item      | Value |
+    | ----------- | ----- |
+    | GET_PAGE    |     1 |
+    | NUM_CLIENTS |     1 |
+    | NUM_SERVERS |     1 |
+    | BUFFER_SIZE |     1 |
+    | WEB_PAGE    |     1 |
+   </div>
 
    You can vary the values as you see fit.
 
-   <div class="flex flex-row">
+   <div class="flex flex-row flex-wrap">
     <Figure src={img_value_filling} alt="Value filling..." client:load />
     <Figure src={img_what_is_the_model} alt="What is the model?" client:load />
    </div>