Add LaTeX support for rendering rules

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"

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 ++ "}"

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 )
+        ]