From acc769e799c7191c1282755ec67be3041ee0fe3e Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sun, 26 Nov 2023 15:54:01 -0800
Subject: [PATCH] Add LaTeX support for rendering rules

---
 elm.json               |  2 +-
 src/Bergamot/Latex.elm |  2 +-
 src/Main.elm           | 25 ++++++++++++++++++++++---
 3 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/elm.json b/elm.json
index 319ec40..9bde88f 100644
--- a/elm.json
+++ b/elm.json
@@ -9,10 +9,10 @@
             "elm/browser": "1.0.2",
             "elm/core": "1.0.5",
             "elm/html": "1.0.0",
+            "elm/json": "1.1.3",
             "elm/parser": "1.1.0"
         },
         "indirect": {
-            "elm/json": "1.1.3",
             "elm/time": "1.0.0",
             "elm/url": "1.0.0",
             "elm/virtual-dom": "1.0.3"
diff --git a/src/Bergamot/Latex.elm b/src/Bergamot/Latex.elm
index 404ade4..470ff9e 100644
--- a/src/Bergamot/Latex.elm
+++ b/src/Bergamot/Latex.elm
@@ -31,4 +31,4 @@ unificationVarToLatex : UnificationVar -> String
 unificationVarToLatex (MkUnificationVar s) = s
 
 proofTreeToLatex : ProofTree -> String
-proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"
+proofTreeToLatex (MkProofTree node) = "\\cfrac{" ++ String.join "\\quad \\quad " (List.map proofTreeToLatex node.premises) ++ "}{" ++ termToLatex unificationVarToLatex node.conclusion ++ "}\\ \\texttt{" ++ node.name ++ "}"
diff --git a/src/Main.elm b/src/Main.elm
index 84a1fb6..53567a6 100644
--- a/src/Main.elm
+++ b/src/Main.elm
@@ -9,6 +9,7 @@ import Bergamot.Search exposing (..)
 import Bergamot.Rules exposing (..)
 import Bergamot.Parser exposing (..)
 import Bergamot.Latex exposing (..)
+import Json.Encode
 import Maybe
 import Tuple
 import Debug
@@ -42,11 +43,11 @@ view m = Html.div []
     [ Html.textarea [ onInput SetProgram ] []
     , Html.br [] []
     , Html.input [ type_ "text", onInput SetQuery ] []
-    , Html.pre [] [ Html.code [] [ Html.text (Maybe.withDefault "" (printRules m.program)) ] ]
-    , Html.pre [] [ Html.code [] [ Html.text (
+    , latex (Maybe.withDefault "" (printRules m.program))
+    , latex (
         proveQuery m.program m.query
         |> Maybe.map proofTreeToLatex
-        |> Maybe.withDefault "") ] ]
+        |> Maybe.withDefault "")
     ]
 
 update : Msg -> Model -> (Model, Cmd Msg)
@@ -65,3 +66,21 @@ main =
         , update = update
         , subscriptions = subscriptions
         }
+
+-- Latex support:
+-- Based on https://stackoverflow.com/questions/75492820/embedding-mathematical-equations-in-an-elm-spa
+
+latex : String -> Html Msg
+latex expr =
+  Html.node "katex-expression"
+    [ Html.Attributes.attribute "expression" expr
+    , Html.Attributes.attribute "katex-options" (Json.Encode.encode 0 options)
+    ]
+    []
+
+
+options : Json.Encode.Value
+options =
+    Json.Encode.object
+        [ ( "displayMode", Json.Encode.bool True )
+        ]