kripke: add history (2)

This commit is contained in:
2025-02-22 13:25:15 +09:00
parent e78c755799
commit 82f96ecf88
2 changed files with 7 additions and 1 deletions

View File

@@ -32,7 +32,7 @@ $effect(() => {
</script> </script>
{#if history.length > 0} {#if history.length > 0}
<datalist id="formula"> <datalist id="formula-history">
{#each history as fml} {#each history as fml}
<option value={fml}></option> <option value={fml}></option>
{/each} {/each}
@@ -41,6 +41,7 @@ $effect(() => {
<input <input
id="formula" 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"]} class={["rounded border border-foreground ring-0 focus:outline-none focus:ring-0 p-2 w-full", error && "border-primary"]}
type="text" type="text"
placeholder="Enter modal formula" placeholder="Enter modal formula"

View File

@@ -10,11 +10,13 @@ import {
isomorphic, isomorphic,
latexSymbols, latexSymbols,
prettyPrint, prettyPrint,
unicodeSymbols,
} from "@cannorin/kripke"; } from "@cannorin/kripke";
import LuCheck from "lucide-svelte/icons/check"; import LuCheck from "lucide-svelte/icons/check";
import LuHeart from "lucide-svelte/icons/heart"; import LuHeart from "lucide-svelte/icons/heart";
import LuHeartCrack from "lucide-svelte/icons/heart-crack"; import LuHeartCrack from "lucide-svelte/icons/heart-crack";
import LuX from "lucide-svelte/icons/x"; import LuX from "lucide-svelte/icons/x";
import { formulaHistory } from "../lib/store";
import FormulaInput from "./formula-input.svelte"; import FormulaInput from "./formula-input.svelte";
import FrameInput from "./frame-input.svelte"; import FrameInput from "./frame-input.svelte";
@@ -91,6 +93,9 @@ let canCheck = $derived.by(() => {
async function check() { async function check() {
if (!canCheck || !formula) return; if (!canCheck || !formula) return;
const valid = await checkImpl(formula); const valid = await checkImpl(formula);
formulaHistory.update((h) =>
formula ? h.add(prettyPrint(formula, { symbols: unicodeSymbols })) : h,
);
moves.push({ type: "check", formulaStr, valid }); moves.push({ type: "check", formulaStr, valid });
moves = [...moves]; moves = [...moves];
formula = undefined; formula = undefined;