r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

style: Lean 4 compiler style in LeanInk

main
Henrik Böving 2023-01-01 19:53:21 +01:00
parent f74443a673
commit d5ef8006b7
2 changed files with 18 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
DocGen4/LeanInk/Output.lean
View File

@ -23,7 +23,7 @@ def getNextButtonLabel : AlectryonM String := do
let val ← get let val ← get
let newCounter := val.counter + 1 let newCounter := val.counter + 1
set { val with counter := newCounter } set { val with counter := newCounter }
pure s!"plain-lean4-lean-chk{val.counter}" return s!"plain-lean4-lean-chk{val.counter}"
def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
pure pure
@ -35,7 +35,7 @@ def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
<span class="hyp-type"> <span class="hyp-type">
<var>{tyi.name}</var> <var>{tyi.name}</var>
<b>: </b> <b>: </b>
<span>[←DocGen4.Output.infoFormatToHtml tyi.type.fst]</span> <span>[← DocGen4.Output.infoFormatToHtml tyi.type.fst]</span>
</span> </span>
</div> </div>
</blockquote> </blockquote>
@ -55,7 +55,7 @@ def Token.toHtml (t : Token) : AlectryonM Html := do
-- TODO: render docstring -- TODO: render docstring
let mut parts := #[] let mut parts := #[]
if let some tyi := t.typeinfo then if let some tyi := t.typeinfo then
parts := parts.push <| ←tyi.toHtml parts := parts.push <| ← tyi.toHtml
parts := parts.push t.processSemantic parts := parts.push t.processSemantic
@ -84,12 +84,12 @@ def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
hypParts := hypParts.push hypParts := hypParts.push
<span class="hyp-body"> <span class="hyp-body">
<b>:= </b> <b>:= </b>
<span>[←infoFormatToHtml h.body.fst]</span> <span>[← infoFormatToHtml h.body.fst]</span>
</span> </span>
hypParts := hypParts.push hypParts := hypParts.push
<span class="hyp-type"> <span class="hyp-type">
<b>: </b> <b>: </b>
<span >[←infoFormatToHtml h.type.fst]</span> <span >[← infoFormatToHtml h.type.fst]</span>
</span> </span>
pure pure
@ -106,7 +106,7 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do
let conclusionHtml ← let conclusionHtml ←
match g.conclusion with match g.conclusion with
| .typed info _ => infoFormatToHtml info | .typed info _ => infoFormatToHtml info
| .untyped str => pure <| #[Html.text str] | .untyped str => pure #[Html.text str]
pure pure
<blockquote class="alectryon-goal"> <blockquote class="alectryon-goal">
@ -133,7 +133,7 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
if s.messages.size > 0 then if s.messages.size > 0 then
#[ #[
<div class="alectryon-messages"> <div class="alectryon-messages">
[←s.messages.mapM Message.toHtml] [← s.messages.mapM Message.toHtml]
</div> </div>
] ]
else else
@ -144,7 +144,7 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
-- TODO: Alectryon has a "alectryon-extra-goals" here, implement it -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
#[ #[
<div class="alectryon-goals"> <div class="alectryon-goals">
[←s.goals.mapM Goal.toHtml] [← s.goals.mapM Goal.toHtml]
</div> </div>
] ]
else else
@ -156,7 +156,7 @@ def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
<span class="alectryon-sentence"> <span class="alectryon-sentence">
<input class="alectryon-toggle" id={buttonLabel} style="display: none" type="checkbox"/> <input class="alectryon-toggle" id={buttonLabel} style="display: none" type="checkbox"/>
<label class="alectryon-input" for={buttonLabel}> <label class="alectryon-input" for={buttonLabel}>
{←s.contents.toHtml} {← s.contents.toHtml}
</label> </label>
<small class="alectryon-output"> <small class="alectryon-output">
[messages] [messages]
@ -185,12 +185,12 @@ def baseHtml (content : Array Html) : AlectryonM Html := do
<meta charset="UTF-8"/> <meta charset="UTF-8"/>
<meta name="viewport" content="width=device-width, initial-scale=1"/> <meta name="viewport" content="width=device-width, initial-scale=1"/>
<link rel="stylesheet" href={s!"{←getRoot}src/alectryon.css"}/> <link rel="stylesheet" href={s!"{← getRoot}src/alectryon.css"}/>
<link rel="stylesheet" href={s!"{←getRoot}src/pygments.css"}/> <link rel="stylesheet" href={s!"{← getRoot}src/pygments.css"}/>
<link rel="stylesheet" href={s!"{←getRoot}src/docutils_basic.css"}/> <link rel="stylesheet" href={s!"{← getRoot}src/docutils_basic.css"}/>
<link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/> <link rel="shortcut icon" href={s!"{← getRoot}favicon.ico"}/>
<script defer="true" src={s!"{←getRoot}src/alectryon.js"}></script> <script defer="true" src={s!"{← getRoot}src/alectryon.js"}></script>
</head> </head>
<body> <body>
<article class="alectryon-root alectryon-centered"> <article class="alectryon-root alectryon-centered">
@ -210,6 +210,6 @@ def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List F
def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do
let fs ← annotationsToFragments as let fs ← annotationsToFragments as
let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 } let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 }
pure html return html
end LeanInk.Annotation.Alectryon end LeanInk.Annotation.Alectryon

6
DocGen4/LeanInk/Process.lean
View File

@ -21,7 +21,7 @@ def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.Analy
let srcPath := moduleNameToFile srcBasePath modName let srcPath := moduleNameToFile srcBasePath modName
IO.FS.createDirAll srcDir IO.FS.createDirAll srcDir
IO.FS.writeFile srcPath srcHtml.toString IO.FS.writeFile srcPath srcHtml.toString
pure 0 return 0
def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
let ctx ← readThe SiteContext let ctx ← readThe SiteContext
@ -33,10 +33,10 @@ def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
} }
def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do
execAuxM.run (←readThe SiteContext) (←readThe SiteBaseContext) |>.run config execAuxM.run (← readThe SiteContext) (← readThe SiteBaseContext) |>.run config
@[implemented_by enableInitializersExecution] @[implemented_by enableInitializersExecution]
private def enableInitializersExecutionWrapper : IO Unit := pure () private def enableInitializersExecutionWrapper : IO Unit := return ()
def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
let contents ← IO.FS.readFile sourceFilePath let contents ← IO.FS.readFile sourceFilePath