Improvements to playground editor

2025-06-27 21:31:35 -07:00
parent 5743eb39ea
commit cee1519b8e
7 changed files with 74 additions and 19 deletions
--- a/newt-vscode/language-configuration.json
+++ b/newt-vscode/language-configuration.json
@@ -33,7 +33,7 @@
  ],
  "onEnterRules": [
    {
-      "beforeText": "\\b(where|of|case)$",
+      "beforeText": "\\b(where|of|do)\\s*$",
      "action": { "indent": "indent" }
    },
    {
--- a/newt-vscode/src/abbrev.ts
+++ b/newt-vscode/src/abbrev.ts
@@ -7,4 +7,9 @@ export const ABBREV: Record<string, string> = {
  "\\circ": "∘",
  "\\1": "₁",
  "\\2": "₂",
+  "\\<": "⟨",
+  "\\>": "⟩",
+  "\\_0": "₀",
+  "\\_1": "₁",
+  "\\bN": "ℕ"
 };