diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean index 91db9b6..04c8c7a 100644 --- a/DocGen4/LeanInk/Output.lean +++ b/DocGen4/LeanInk/Output.lean @@ -25,15 +25,50 @@ def getNextButtonLabel : AlectryonM String := do set { val with counter := newCounter } pure s!"plain-lean4-lean-chk{val.counter}" -def TypeInfo.toHtml : TypeInfo → AlectryonM Html := sorry +def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do + pure +
++ + {tyi.name} + : + {tyi.type} + /span> + /div> + /blockquote> + /div> + /small> + /div> def Token.toHtml (t : Token) : AlectryonM Html := do - -- TODO: Show rest of token - pure $ Html.text t.raw + -- Right now t.link is always none from LeanInk, ignore it + -- TODO: render docstring + let mut parts := #[] + if let some tyi := t.typeinfo then + parts := parts.push $ ←tyi.toHtml -def Contents.toHtml : Contents → AlectryonM (Array Html) - | .string value => pure #[Html.text value] - | .experimentalTokens values => values.mapM Token.toHtml + parts := parts.push $ Html.text t.raw + pure + -- 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>] @@ -108,7 +143,7 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do