From 1fe870bdbcb2b11833f938da7a6059b383492eb7 Mon Sep 17 00:00:00 2001
From: cannorin <cannorin@users.noreply.github.com>
Date: Tue, 9 Sep 2025 06:39:02 +0900
Subject: [PATCH] kripke: add math keys

---
 .../kripke/components/formula-input.svelte    | 43 +++++++++++++++----
 1 file changed, 35 insertions(+), 8 deletions(-)

diff --git a/apps/web/src/routes/kripke/components/formula-input.svelte b/apps/web/src/routes/kripke/components/formula-input.svelte
index 9960c6f..8670652 100644
--- a/apps/web/src/routes/kripke/components/formula-input.svelte
+++ b/apps/web/src/routes/kripke/components/formula-input.svelte
@@ -1,4 +1,5 @@
 <script lang="ts">
+import Katex from "$lib/components/katex.svelte";
 import { type Formula, prettyPrint, tryParse } from "@cannorin/kripke";
 import { formulaHistory } from "../lib/store";
 
@@ -18,6 +19,7 @@ let history = $derived(
     .slice(0, 10)
     .map(([a, _ac]) => a),
 );
+let inputElement: HTMLInputElement;
 
 $effect(() => {
   const fml = tryParse(input);
@@ -39,11 +41,36 @@ $effect(() => {
   </datalist>
 {/if}
 
-<input
-  id="formula"
-  list="formula-history"
-  class={["rounded border border-foreground ring-0 focus:outline-none focus:ring-0 p-2 w-full", error && "border-primary"]}
-  type="text"
-  placeholder="Enter modal formula"
-  disabled={disabled}
-  bind:value={input} />
+{#snippet mathKey(latexCommand: string, actualText?: string)}
+  <button onclick={(e) => {
+    e.preventDefault();
+    input += actualText ?? latexCommand;
+    inputElement.focus();
+  }}>
+    <Katex math={latexCommand} />
+  </button>
+{/snippet}
+
+<div class="rounded border border-foreground w-full">
+  <div class="border-0 border-b border-muted px-2 py-1 flex justify-between">
+    {@render mathKey("\\top", "⊤")}
+    {@render mathKey("\\bot", "⊥")}
+    {@render mathKey("\\neg", "¬")}
+    {@render mathKey("\\Box", "□")}
+    {@render mathKey("\\Diamond", "◇")}
+    {@render mathKey("\\land", "∧")}
+    {@render mathKey("\\lor", "∨")}
+    {@render mathKey("\\to", "→")}
+    {@render mathKey("\\leftrightarrow", "↔")}
+  </div>
+
+  <input
+    id="formula"
+    list="formula-history"
+    class={["ring-0 rounded focus:outline-none p-2 focus:ring-0 w-full", error && "border-primary"]}
+    type="text"
+    placeholder="Enter modal formula"
+    disabled={disabled}
+    bind:value={input}
+    bind:this={inputElement} />
+</div>