+
+
+
def Token.processSemantic (t : Token) : Html :=
match t.semanticType with
- | some "Name.Attribute" => {t.raw}/span>
- | some "Name.Variable" => {t.raw}/span>
- | some "Keyword" => {t.raw}/span>
+ | some "Name.Attribute" => {t.raw}
+ | some "Name.Variable" => {t.raw}
+ | some "Keyword" => {t.raw}
| _ => Html.text t.raw
def Token.toHtml (t : Token) : AlectryonM Html := do
@@ -63,39 +63,39 @@ def Token.toHtml (t : Token) : AlectryonM Html := do
-- TODO: Show rest of token
[parts]
- /span>
+
def Contents.toHtml : Contents → AlectryonM Html
| .string value =>
pure
{value}
- /span>
+
| .experimentalTokens values => do
let values ← values.mapM Token.toHtml
pure
[values]
- /span>
+
def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
- let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]/var>]
+ let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]]
if h.body != "" then
hypParts := hypParts.push
- := /b>
- {h.body}/span>
- /span>
+ :=
+ {h.body}
+
hypParts := hypParts.push
- : /b>
- {h.type}/span>
- /span>
+ :
+ {h.type}
+
pure
[hypParts]
- /span>
+
def Goal.toHtml (g : Goal) : AlectryonM Html := do
let mut hypotheses := #[]
@@ -107,21 +107,21 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do
[hypotheses]
- /div>
+
- {g.name}/span>/hr>
- /span>
+ {g.name}
+
{g.conclusion}
- /div>
- /blockquote>
+
+
def Message.toHtml (m : Message) : AlectryonM Html := do
pure
-- TODO: This might have to be done in a fancier way
{m.contents}
- /blockquote>
+
def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
let messages :=
@@ -129,7 +129,7 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
#[
[←s.messages.mapM Message.toHtml]
- /div>
+
]
else
#[]
@@ -140,7 +140,7 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
#[
[←s.goals.mapM Goal.toHtml]
- /div>
+
]
else
#[]
@@ -152,12 +152,12 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
[messages]
[goals]
- /small>
- /span>
+
+
def Text.toHtml (t : Text) : AlectryonM Html := t.contents.toHtml
@@ -168,10 +168,10 @@ def Fragment.toHtml : Fragment → AlectryonM Html
def baseHtml (content : Array Html) : AlectryonM Html := do
let banner :=