Henrik Böving
GitHub
commit
38e02c5f65
|
|
@ -25,6 +25,14 @@ jobs:
|
|||
run: |
|
||||
lake build
|
||||
|
||||
- name: Checkout and compile LeanInk
|
||||
run: |
|
||||
cd ../
|
||||
git clone https://github.com/hargonix/LeanInk
|
||||
cd LeanInk
|
||||
git checkout doc-gen
|
||||
lake build
|
||||
|
||||
- name: Checkout and compile mathlib4
|
||||
run: |
|
||||
cd ../
|
||||
|
|
@ -40,7 +48,7 @@ jobs:
|
|||
deploy="false"
|
||||
fi
|
||||
cd ../
|
||||
./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "$deploy"
|
||||
./doc-gen4/deploy_docs.sh "mathlib4" "doc-gen4" "$deploy" "LeanInk"
|
||||
env:
|
||||
MATHLIB4_DOCS_KEY: ${{ secrets.MATHLIB4_DOCS_KEY }}
|
||||
github_repo: ${{ github.repository }}
|
||||
|
|
|
|||
|
|
@ -7,3 +7,4 @@ import DocGen4.Process
|
|||
import DocGen4.Load
|
||||
import DocGen4.IncludeStr
|
||||
import DocGen4.Output
|
||||
import DocGen4.LeanInk
|
||||
|
|
|
|||
|
|
@ -0,0 +1,7 @@
|
|||
/-
|
||||
Copyright (c) 2022 Henrik Böving. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Henrik Böving
|
||||
-/
|
||||
import DocGen4.LeanInk.Process
|
||||
import DocGen4.LeanInk.Output
|
||||
|
|
@ -0,0 +1,222 @@
|
|||
/-
|
||||
Copyright (c) 2022 Henrik Böving. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Henrik Böving, Xubai Wang
|
||||
-/
|
||||
import DocGen4.Output.Base
|
||||
import DocGen4.Output.ToHtmlFormat
|
||||
import DocGen4.LeanInk.Process
|
||||
import Lean.Data.Json
|
||||
import LeanInk.Annotation.Alectryon
|
||||
|
||||
namespace LeanInk.Annotation.Alectryon
|
||||
|
||||
open DocGen4 Output
|
||||
open scoped DocGen4.Jsx
|
||||
|
||||
structure AlectryonContext where
|
||||
counter : Nat
|
||||
|
||||
abbrev AlectryonM := StateT AlectryonContext HtmlM
|
||||
|
||||
def getNextButtonLabel : AlectryonM String := do
|
||||
let val ← get
|
||||
let newCounter := val.counter + 1
|
||||
set { val with counter := newCounter }
|
||||
pure s!"plain-lean4-lean-chk{val.counter}"
|
||||
|
||||
def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
|
||||
pure
|
||||
<div class="alectryon-type-info-wrapper">
|
||||
<small class="alectryon-type-info">
|
||||
<div class="alectryon-goals">
|
||||
<blockquote class="alectryon-goal">
|
||||
<div class="goal-hyps">
|
||||
<span class="hyp-type">
|
||||
<var>{tyi.name}<//var>
|
||||
<b>: <//b>
|
||||
<span>{tyi.type}<//span>
|
||||
<//span>
|
||||
<//div>
|
||||
<//blockquote>
|
||||
<//div>
|
||||
<//small>
|
||||
<//div>
|
||||
|
||||
def Token.processSemantic (t : Token) : Html :=
|
||||
match t.semanticType with
|
||||
| some "Name.Attribute" => <span class="na">{t.raw}<//span>
|
||||
| some "Name.Variable" => <span class="nv">{t.raw}<//span>
|
||||
| some "Keyword" => <span class="k">{t.raw}<//span>
|
||||
| _ => Html.text t.raw
|
||||
|
||||
def Token.toHtml (t : Token) : AlectryonM Html := do
|
||||
-- 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
|
||||
|
||||
parts := parts.push t.processSemantic
|
||||
|
||||
pure
|
||||
-- TODO: Show rest of token
|
||||
<span class="alectryon-token">
|
||||
[parts]
|
||||
<//span>
|
||||
|
||||
def Contents.toHtml : Contents → AlectryonM Html
|
||||
| .string value =>
|
||||
pure
|
||||
<span class="alectryon-wsp">
|
||||
{value}
|
||||
<//span>
|
||||
| .experimentalTokens values => do
|
||||
let values ← values.mapM Token.toHtml
|
||||
pure
|
||||
<span class="alectryon-wsp">
|
||||
[values]
|
||||
<//span>
|
||||
|
||||
def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
|
||||
let mut hypParts := #[<var>[h.names.intersperse ", " |>.map Html.text |>.toArray]<//var>]
|
||||
if h.body != "" then
|
||||
hypParts := hypParts.push
|
||||
<span class="hyp-body">
|
||||
<b>:= <//b>
|
||||
<span>{h.body}<//span>
|
||||
<//span>
|
||||
hypParts := hypParts.push
|
||||
<span class="hyp-type">
|
||||
<b>: <//b>
|
||||
<span >{h.type}<//span>
|
||||
<//span>
|
||||
|
||||
pure
|
||||
<span>
|
||||
[hypParts]
|
||||
<//span>
|
||||
|
||||
def Goal.toHtml (g : Goal) : AlectryonM Html := do
|
||||
let mut hypotheses := #[]
|
||||
for hyp in g.hypotheses do
|
||||
let rendered ← hyp.toHtml
|
||||
hypotheses := hypotheses.push rendered
|
||||
hypotheses := hypotheses.push <br/>
|
||||
pure
|
||||
<blockquote class="alectryon-goal">
|
||||
<div class="goal-hyps">
|
||||
[hypotheses]
|
||||
<//div>
|
||||
<span class="goal-separator">
|
||||
<hr><span class="goal-name">{g.name}<//span><//hr>
|
||||
<//span>
|
||||
<div class="goal-conclusion">
|
||||
{g.conclusion}
|
||||
<//div>
|
||||
<//blockquote>
|
||||
|
||||
def Message.toHtml (m : Message) : AlectryonM Html := do
|
||||
pure
|
||||
<blockquote class="alectryon-message">
|
||||
-- TODO: This might have to be done in a fancier way
|
||||
{m.contents}
|
||||
<//blockquote>
|
||||
|
||||
def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
|
||||
let messages :=
|
||||
if s.messages.size > 0 then
|
||||
#[
|
||||
<div class="alectryon-messages">
|
||||
[←s.messages.mapM Message.toHtml]
|
||||
<//div>
|
||||
]
|
||||
else
|
||||
#[]
|
||||
|
||||
let goals :=
|
||||
if s.goals.size > 0 then
|
||||
-- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
|
||||
#[
|
||||
<div class="alectryon-goals">
|
||||
[←s.goals.mapM Goal.toHtml]
|
||||
<//div>
|
||||
]
|
||||
else
|
||||
#[]
|
||||
|
||||
let buttonLabel ← getNextButtonLabel
|
||||
|
||||
pure
|
||||
<span class="alectryon-sentence">
|
||||
<input class="alectryon-toggle" id={buttonLabel} style="display: none" type="checkbox"/>
|
||||
<label class="alectryon-input" for={buttonLabel}>
|
||||
{←s.contents.toHtml}
|
||||
<//label>
|
||||
<small class="alectryon-output">
|
||||
[messages]
|
||||
[goals]
|
||||
<//small>
|
||||
<//span>
|
||||
|
||||
def Text.toHtml (t : Text) : AlectryonM Html := t.contents.toHtml
|
||||
|
||||
def Fragment.toHtml : Fragment → AlectryonM Html
|
||||
| .text value => value.toHtml
|
||||
| .sentence value => value.toHtml
|
||||
|
||||
def baseHtml (content : Array Html) : AlectryonM Html := do
|
||||
let banner :=
|
||||
<div «class»="alectryon-banner">
|
||||
Built with <a href="https://github.com/leanprover/doc-gen4">doc-gen4<//a>, running Lean4.
|
||||
Bubbles (<span class="alectryon-bubble"><//span>) indicate interactive fragments: hover for details, tap to reveal contents.
|
||||
Use <kbd>Ctrl+↑<//kbd> <kbd>Ctrl+↓<//kbd> to navigate, <kbd>Ctrl+🖱️<//kbd> to focus.
|
||||
On Mac, use <kbd>Cmd<//kbd> instead of <kbd>Ctrl<//kbd>.
|
||||
</div>
|
||||
|
||||
pure
|
||||
<html lang="en" class="alectryon-standalone">
|
||||
<head>
|
||||
<meta charset="UTF-8"/>
|
||||
<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/pygments.css"}/>
|
||||
<link rel="stylesheet" href={s!"{←getRoot}src/docutils_basic.css"}/>
|
||||
<link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>
|
||||
|
||||
<script defer="true" src={s!"{←getRoot}src/alectryon.js"}></script>
|
||||
</head>
|
||||
<body>
|
||||
<article class="alectryon-root alectryon-centered">
|
||||
{banner}
|
||||
<pre class="alectryon-io highlight">
|
||||
[content]
|
||||
</pre>
|
||||
</article>
|
||||
</body>
|
||||
</html>
|
||||
|
||||
def renderFragments (fs : Array Fragment) : AlectryonM Html :=
|
||||
fs.mapM Fragment.toHtml >>= baseHtml
|
||||
|
||||
end LeanInk.Annotation.Alectryon
|
||||
|
||||
namespace DocGen4.Output.LeanInk
|
||||
|
||||
open Lean
|
||||
open LeanInk.Annotation.Alectryon
|
||||
open scoped DocGen4.Jsx
|
||||
|
||||
def moduleToHtml (module : Process.Module) (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : HtmlT IO Html := withReader (setCurrentName module.name) do
|
||||
let json ← runInk inkPath sourceFilePath
|
||||
let fragments := fromJson? json
|
||||
match fragments with
|
||||
| .ok fragments =>
|
||||
let render := StateT.run (LeanInk.Annotation.Alectryon.renderFragments fragments) { counter := 0 }
|
||||
let ctx ← read
|
||||
let (html, _) := ReaderT.run render ctx
|
||||
pure html
|
||||
| .error err => throw $ IO.userError s!"Error while parsing LeanInk Output: {err}"
|
||||
|
||||
end DocGen4.Output.LeanInk
|
||||
|
|
@ -0,0 +1,40 @@
|
|||
/-
|
||||
Copyright (c) 2022 Henrik Böving. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Henrik Böving
|
||||
-/
|
||||
import Lean.Data.Json
|
||||
|
||||
namespace DocGen4.Output.LeanInk
|
||||
|
||||
open Lean
|
||||
open IO
|
||||
|
||||
def runInk (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : IO Json := do
|
||||
let arguments := #[
|
||||
"analyze", sourceFilePath.toString,
|
||||
"--lake", "lakefile.lean",
|
||||
"--x-enable-type-info",
|
||||
"--x-enable-docStrings",
|
||||
"--x-enable-semantic-token"
|
||||
]
|
||||
let inkProcess ← Process.spawn {
|
||||
stdin := Process.Stdio.null
|
||||
stdout := Process.Stdio.piped
|
||||
stderr := Process.Stdio.piped
|
||||
cmd := inkPath.toString
|
||||
args := arguments
|
||||
}
|
||||
match (←inkProcess.wait) with
|
||||
| 0 =>
|
||||
let outputFilePath := sourceFilePath.withExtension "lean.leanInk"
|
||||
let output ← FS.readFile outputFilePath
|
||||
FS.removeFile outputFilePath
|
||||
match Json.parse output with
|
||||
| .ok out => pure out
|
||||
| .error err =>
|
||||
throw $ IO.userError s!"LeanInk returned invalid JSON for file: {sourceFilePath}:\n{err}"
|
||||
| code =>
|
||||
throw $ IO.userError s!"LeanInk exited with code {code} for file: {sourceFilePath}:\n{←inkProcess.stderr.readToEnd}"
|
||||
|
||||
end DocGen4.Output.LeanInk
|
||||
|
|
@ -13,6 +13,7 @@ import DocGen4.Output.NotFound
|
|||
import DocGen4.Output.Find
|
||||
import DocGen4.Output.Semantic
|
||||
import DocGen4.Output.SourceLinker
|
||||
import DocGen4.LeanInk.Output
|
||||
|
||||
namespace DocGen4
|
||||
|
||||
|
|
@ -22,15 +23,27 @@ open Lean IO System Output Process
|
|||
The main entrypoint for outputting the documentation HTML based on an
|
||||
`AnalyzerResult`.
|
||||
-/
|
||||
def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
|
||||
let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
|
||||
def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) (inkPath : Option System.FilePath) : IO Unit := do
|
||||
let config := {
|
||||
depthToRoot := 0,
|
||||
result := result,
|
||||
currentName := none,
|
||||
sourceLinker := ←sourceLinker ws leanHash
|
||||
leanInkEnabled := inkPath.isSome
|
||||
}
|
||||
let basePath := FilePath.mk "." / "build" / "doc"
|
||||
let srcBasePath := basePath / "src"
|
||||
let indexHtml := ReaderT.run index config
|
||||
let findHtml := ReaderT.run find { config with depthToRoot := 1 }
|
||||
let notFoundHtml := ReaderT.run notFound config
|
||||
-- Rendering the entire lean compiler takes time....
|
||||
--let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath
|
||||
let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath
|
||||
|
||||
FS.createDirAll basePath
|
||||
FS.createDirAll (basePath / "find")
|
||||
FS.createDirAll (basePath / "semantic")
|
||||
FS.createDirAll srcBasePath
|
||||
|
||||
let mut declList := #[]
|
||||
for (_, mod) in result.moduleInfo.toArray do
|
||||
|
|
@ -66,16 +79,31 @@ def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String
|
|||
FS.writeFile (basePath / "how-about.js") howAboutJs
|
||||
FS.writeFile (basePath / "search.js") searchJs
|
||||
FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs
|
||||
FS.writeFile (srcBasePath / "alectryon.css") alectryonCss
|
||||
FS.writeFile (srcBasePath / "alectryon.js") alectryonJs
|
||||
FS.writeFile (srcBasePath / "docutils_basic.css") docUtilsCss
|
||||
FS.writeFile (srcBasePath / "pygments.css") pygmentsCss
|
||||
|
||||
for (module, content) in result.moduleInfo.toArray do
|
||||
let fileDir := moduleNameToDirectory basePath module
|
||||
let filePath := moduleNameToFile basePath module
|
||||
for (modName, module) in result.moduleInfo.toArray do
|
||||
let fileDir := moduleNameToDirectory basePath modName
|
||||
let filePath := moduleNameToFile basePath modName
|
||||
-- path: 'basePath/module/components/till/last.html'
|
||||
-- The last component is the file name, so we drop it from the depth to root.
|
||||
let config := { config with depthToRoot := module.components.dropLast.length }
|
||||
let moduleHtml := ReaderT.run (moduleToHtml content) config
|
||||
let config := { config with depthToRoot := modName.components.dropLast.length }
|
||||
let moduleHtml := ReaderT.run (moduleToHtml module) config
|
||||
FS.createDirAll $ fileDir
|
||||
FS.writeFile filePath moduleHtml.toString
|
||||
if let some inkPath := inkPath then
|
||||
if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
|
||||
IO.println s!"Inking: {modName.toString}"
|
||||
-- path: 'basePath/src/module/components/till/last.html'
|
||||
-- The last component is the file name, however we are in src/ here so dont drop it this time
|
||||
let config := { config with depthToRoot := modName.components.length }
|
||||
let srcHtml ← ReaderT.run (LeanInk.moduleToHtml module inkPath inputPath) config
|
||||
let srcDir := moduleNameToDirectory srcBasePath modName
|
||||
let srcPath := moduleNameToFile srcBasePath modName
|
||||
FS.createDirAll srcDir
|
||||
FS.writeFile srcPath srcHtml.toString
|
||||
|
||||
end DocGen4
|
||||
|
||||
|
|
|
|||
|
|
@ -33,6 +33,10 @@ structure SiteContext where
|
|||
A function to link declaration names to their source URLs, usually Github ones.
|
||||
-/
|
||||
sourceLinker : Name → Option DeclarationRange → String
|
||||
/--
|
||||
Whether LeanInk is enabled
|
||||
-/
|
||||
leanInkEnabled : Bool
|
||||
|
||||
def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name}
|
||||
|
||||
|
|
@ -52,6 +56,7 @@ def getRoot : HtmlM String := do
|
|||
def getResult : HtmlM AnalyzerResult := do pure (←read).result
|
||||
def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName
|
||||
def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range
|
||||
def leanInkEnabled? : HtmlM Bool := do pure (←read).leanInkEnabled
|
||||
|
||||
/--
|
||||
If a template is meant to be extended because it for example only provides the
|
||||
|
|
@ -73,6 +78,13 @@ Returns the HTML doc-gen4 link to a module name.
|
|||
def moduleToHtmlLink (module : Name) : HtmlM Html := do
|
||||
pure <a href={←moduleNameToLink module}>{module.toString}</a>
|
||||
|
||||
/--
|
||||
Returns the LeanInk link to a module name.
|
||||
-/
|
||||
def moduleNameToInkLink (n : Name) : HtmlM String := do
|
||||
let parts := "src" :: n.components.map Name.toString
|
||||
pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
|
||||
|
||||
/--
|
||||
Returns the path to the HTML file that contains information about a module.
|
||||
-/
|
||||
|
|
@ -87,7 +99,6 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
|
|||
let parts := n.components.dropLast.map Name.toString
|
||||
basePath / parts.foldl (· / ·) (FilePath.mk ".")
|
||||
|
||||
|
||||
section Static
|
||||
/-!
|
||||
The following section contains all the statically included files that
|
||||
|
|
@ -100,6 +111,11 @@ are used in documentation generation, notably JS and CSS ones.
|
|||
def searchJs : String := include_str "../../static/search.js"
|
||||
def findJs : String := include_str "../../static/find/find.js"
|
||||
def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
|
||||
|
||||
def alectryonCss : String := include_str "../../static/alectryon/alectryon.css"
|
||||
def alectryonJs : String := include_str "../../static/alectryon/alectryon.js"
|
||||
def docUtilsCss : String := include_str "../../static/alectryon/docutils_basic.css"
|
||||
def pygmentsCss : String := include_str "../../static/alectryon/pygments.css"
|
||||
end Static
|
||||
|
||||
/--
|
||||
|
|
@ -114,15 +130,21 @@ def declNameToLink (name : Name) : HtmlM String := do
|
|||
Returns the HTML doc-gen4 link to a declaration name.
|
||||
-/
|
||||
def declNameToHtmlLink (name : Name) : HtmlM Html := do
|
||||
let link ← declNameToLink name
|
||||
pure <a href={←declNameToLink name}>{name.toString}</a>
|
||||
|
||||
/--
|
||||
Returns the LeanInk link to a declaration name.
|
||||
-/
|
||||
def declNameToInkLink (name : Name) : HtmlM String := do
|
||||
let res ← getResult
|
||||
let module := res.moduleNames[res.name2ModIdx.find! name]
|
||||
pure $ (←moduleNameToInkLink module) ++ "#" ++ name.toString
|
||||
|
||||
/--
|
||||
Returns the HTML doc-gen4 link to a declaration name with "break_within"
|
||||
set as class.
|
||||
-/
|
||||
def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
|
||||
let link ← declNameToLink name
|
||||
pure <a class="break_within" href={←declNameToLink name}>{name.toString}</a>
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -114,6 +114,15 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
|
|||
#[Html.element "div" false #[("class", "attributes")] #[attrStr]]
|
||||
else
|
||||
#[]
|
||||
let leanInkHtml :=
|
||||
if ←leanInkEnabled? then
|
||||
#[
|
||||
<div class="ink_link">
|
||||
<a href={←declNameToInkLink doc.getName}>ink</a>
|
||||
</div>
|
||||
]
|
||||
else
|
||||
#[]
|
||||
|
||||
pure
|
||||
<div class="decl" id={doc.getName.toString}>
|
||||
|
|
@ -121,6 +130,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
|
|||
<div class="gh_link">
|
||||
<a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
|
||||
</div>
|
||||
[leanInkHtml]
|
||||
[attrsHtml]
|
||||
{←docInfoHeader doc}
|
||||
[docInfoHtml]
|
||||
|
|
|
|||
|
|
@ -89,6 +89,7 @@ syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
|
|||
|
||||
syntax "<" rawIdent jsxAttr* "/>" : jsxElement
|
||||
syntax "<" rawIdent jsxAttr* ">" jsxChild* "</" rawIdent ">" : jsxElement
|
||||
syntax "<" rawIdent jsxAttr* ">" jsxChild* "<//" rawIdent ">" : jsxElement
|
||||
|
||||
syntax jsxText : jsxChild
|
||||
syntax "{" term "}" : jsxChild
|
||||
|
|
@ -115,12 +116,9 @@ def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
|
|||
| _ => Macro.throwUnsupported
|
||||
return as
|
||||
|
||||
macro_rules
|
||||
| `(<$n $attrs* />) => do
|
||||
`(Html.element $(quote (toString n.getId)) true $(← translateAttrs attrs) #[])
|
||||
| `(<$n $attrs* >$children*</$m>) => do
|
||||
private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × Syntax):= do
|
||||
unless n.getId == m.getId do
|
||||
withRef m <| Macro.throwError s!"expected </{n.getId}>"
|
||||
withRef m <| Macro.throwError s!"Leading and trailing part of tags don't match: '{n}', '{m}'"
|
||||
let mut cs ← `(#[])
|
||||
for child in children do
|
||||
cs ← match child with
|
||||
|
|
@ -131,7 +129,17 @@ macro_rules
|
|||
| `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html))
|
||||
| _ => Macro.throwUnsupported
|
||||
let tag := toString n.getId
|
||||
`(Html.element $(quote tag) false $(← translateAttrs attrs) $cs)
|
||||
pure $ (tag, cs)
|
||||
|
||||
macro_rules
|
||||
| `(<$n $attrs* />) => do
|
||||
`(Html.element $(quote (toString n.getId)) true $(← translateAttrs attrs) #[])
|
||||
| `(<$n $attrs* >$children*</$m>) => do
|
||||
let (tag, children) ← htmlHelper n children m
|
||||
`(Html.element $(quote tag) false $(← translateAttrs attrs) $children)
|
||||
| `(<$n $attrs* >$children*<//$m>) => do
|
||||
let (tag, children) ← htmlHelper n children m
|
||||
`(Html.element $(quote tag) true $(← translateAttrs attrs) $children)
|
||||
|
||||
end Jsx
|
||||
|
||||
|
|
|
|||
13
Main.lean
13
Main.lean
|
|
@ -5,6 +5,7 @@ import Cli
|
|||
open DocGen4 Lean Cli
|
||||
|
||||
def runDocGenCmd (p : Parsed) : IO UInt32 := do
|
||||
IO.println s!"{p}"
|
||||
let modules : List String := p.variableArgsAs! String |>.toList
|
||||
let res ← lakeSetup modules
|
||||
match res with
|
||||
|
|
@ -12,7 +13,14 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do
|
|||
IO.println s!"Loading modules from: {←searchPathRef.get}"
|
||||
let doc ← load $ modules.map Name.mkSimple
|
||||
IO.println "Outputting HTML"
|
||||
htmlOutput doc ws leanHash
|
||||
match p.flag? "ink" with
|
||||
| some ink =>
|
||||
let inkPath := System.FilePath.mk ink.value
|
||||
if ←inkPath.pathExists then
|
||||
htmlOutput doc ws leanHash inkPath
|
||||
else
|
||||
throw $ IO.userError "Invalid path to LeanInk binary provided"
|
||||
| none => htmlOutput doc ws leanHash none
|
||||
pure 0
|
||||
| Except.error rc => pure rc
|
||||
|
||||
|
|
@ -20,6 +28,9 @@ def docGenCmd : Cmd := `[Cli|
|
|||
"doc-gen4" VIA runDocGenCmd; ["0.0.1"]
|
||||
"A documentation generator for Lean 4."
|
||||
|
||||
FLAGS:
|
||||
ink : String; "Path to a LeanInk binary to use for rendering the Lean sources."
|
||||
|
||||
ARGS:
|
||||
...modules : String; "The modules to generate the HTML for"
|
||||
]
|
||||
|
|
|
|||
|
|
@ -10,6 +10,10 @@ $ /path/to/doc-gen4 Module
|
|||
where `Module` is one or more of the top level modules you want to document.
|
||||
The tool will then proceed to compile the project using lake (if that hasn't happened yet),
|
||||
analyze it and put the result in `./build/doc`.
|
||||
|
||||
You can optionally provide the path to a `LeanInk` binary using the `--ink` flag which will make
|
||||
the tool produce `Alectryon` style rendered output along the usual documentation.
|
||||
|
||||
You could e.g. host the files locally with the built-in Python webserver:
|
||||
```sh
|
||||
$ cd build/doc && python -m http.server
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ fi
|
|||
|
||||
# generate the docs
|
||||
cd $1
|
||||
../$2/build/bin/doc-gen4 Mathlib
|
||||
../$2/build/bin/doc-gen4 --ink ../$4/build/bin/leanInk Mathlib
|
||||
|
||||
if [ "$3" = "true" ]; then
|
||||
cd ..
|
||||
|
|
|
|||
|
|
@ -24,4 +24,4 @@ require lake from git
|
|||
"https://github.com/leanprover/lake" @ "12e2463b35829368a59d18a5504dd2f73ac1621d"
|
||||
|
||||
require leanInk from git
|
||||
"https://github.com/leanprover/LeanInk" @ "0a160d91458c1873937449a7c78d25b34b8686df"
|
||||
"https://github.com/hargonix/LeanInk" @ "doc-gen"
|
||||
|
|
|
|||
|
|
@ -0,0 +1,777 @@
|
|||
@charset "UTF-8";
|
||||
/*
|
||||
Copyright © 2019 Clément Pit-Claudel
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of this software and associated documentation files (the "Software"), to deal
|
||||
in the Software without restriction, including without limitation the rights
|
||||
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in all
|
||||
copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
|
||||
SOFTWARE.
|
||||
*/
|
||||
|
||||
/*******************************/
|
||||
/* CSS reset for .alectryon-io */
|
||||
/*******************************/
|
||||
|
||||
.alectryon-io blockquote {
|
||||
line-height: inherit;
|
||||
}
|
||||
|
||||
.alectryon-io blockquote:after {
|
||||
display: none;
|
||||
}
|
||||
|
||||
.alectryon-io label {
|
||||
display: inline;
|
||||
font-size: inherit;
|
||||
margin: 0;
|
||||
}
|
||||
|
||||
.alectryon-io a {
|
||||
text-decoration: none !important;
|
||||
font-style: oblique !important;
|
||||
color: unset;
|
||||
}
|
||||
|
||||
/* Undo <small> and <blockquote>, added to improve RSS rendering. */
|
||||
|
||||
.alectryon-io small.alectryon-output,
|
||||
.alectryon-io small.alectryon-type-info {
|
||||
font-size: inherit;
|
||||
}
|
||||
|
||||
.alectryon-io blockquote.alectryon-goal,
|
||||
.alectryon-io blockquote.alectryon-message {
|
||||
font-weight: normal;
|
||||
font-size: inherit;
|
||||
}
|
||||
|
||||
/***************/
|
||||
/* Main styles */
|
||||
/***************/
|
||||
|
||||
.alectryon-coqdoc .doc .code,
|
||||
.alectryon-coqdoc .doc .comment,
|
||||
.alectryon-coqdoc .doc .inlinecode,
|
||||
.alectryon-mref,
|
||||
.alectryon-block, .alectryon-io,
|
||||
.alectryon-toggle-label, .alectryon-banner {
|
||||
font-family: "Source Code Pro", Consolas, "Ubuntu Mono", Menlo, "DejaVu Sans Mono", monospace, monospace !important;
|
||||
font-size: 0.875em;
|
||||
font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
|
||||
line-height: initial;
|
||||
}
|
||||
|
||||
.alectryon-io, .alectryon-block, .alectryon-toggle-label, .alectryon-banner {
|
||||
overflow: visible;
|
||||
overflow-wrap: break-word;
|
||||
position: relative;
|
||||
white-space: pre-wrap;
|
||||
}
|
||||
|
||||
/*
|
||||
CoqIDE doesn't turn off the unicode bidirectional algorithm (and PG simply
|
||||
respects the user's `bidi-display-reordering` setting), so don't turn it off
|
||||
here either. But beware unexpected results like `Definition test_אב := 0.`
|
||||
|
||||
.alectryon-io span {
|
||||
direction: ltr;
|
||||
unicode-bidi: bidi-override;
|
||||
}
|
||||
|
||||
In any case, make an exception for comments:
|
||||
|
||||
.highlight .c {
|
||||
direction: embed;
|
||||
unicode-bidi: initial;
|
||||
}
|
||||
*/
|
||||
|
||||
.alectryon-mref,
|
||||
.alectryon-mref-marker {
|
||||
align-self: center;
|
||||
box-sizing: border-box;
|
||||
display: inline-block;
|
||||
font-size: 80%;
|
||||
font-weight: bold;
|
||||
line-height: 1;
|
||||
box-shadow: 0 0 0 1pt black;
|
||||
padding: 1pt 0.3em;
|
||||
text-decoration: none;
|
||||
}
|
||||
|
||||
.alectryon-block .alectryon-mref-marker,
|
||||
.alectryon-io .alectryon-mref-marker {
|
||||
user-select: none;
|
||||
margin: -0.25em 0 -0.25em 0.5em;
|
||||
}
|
||||
|
||||
.alectryon-inline .alectryon-mref-marker {
|
||||
margin: -0.25em 0.15em -0.25em 0.625em; /* 625 = 0.5em / 80% */
|
||||
}
|
||||
|
||||
.alectryon-mref {
|
||||
color: inherit;
|
||||
margin: -0.5em 0.25em;
|
||||
}
|
||||
|
||||
.alectryon-goal:target .goal-separator .alectryon-mref-marker,
|
||||
:target > .alectryon-mref-marker {
|
||||
animation: blink 0.2s step-start 0s 3 normal none;
|
||||
background-color: #fcaf3e;
|
||||
position: relative;
|
||||
}
|
||||
|
||||
@keyframes blink {
|
||||
50% {
|
||||
box-shadow: 0 0 0 3pt #fcaf3e, 0 0 0 4pt black;
|
||||
z-index: 10;
|
||||
}
|
||||
}
|
||||
|
||||
.alectryon-toggle,
|
||||
.alectryon-io .alectryon-extra-goal-toggle {
|
||||
display: none;
|
||||
}
|
||||
|
||||
.alectryon-bubble,
|
||||
.alectryon-io label,
|
||||
.alectryon-toggle-label {
|
||||
cursor: pointer;
|
||||
}
|
||||
|
||||
.alectryon-toggle-label {
|
||||
display: block;
|
||||
font-size: 0.8em;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-input {
|
||||
padding: 0.1em 0; /* Enlarge the hitbox slightly to fill interline gaps */
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-token {
|
||||
white-space: pre-wrap;
|
||||
display: inline;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-sentence.alectryon-target .alectryon-input {
|
||||
/* FIXME if keywords were ‘bolder’ we wouldn't need !important */
|
||||
font-weight: bold !important; /* Use !important to avoid a * selector */
|
||||
}
|
||||
|
||||
.alectryon-bubble:before,
|
||||
.alectryon-toggle-label:before,
|
||||
.alectryon-io label.alectryon-input:after,
|
||||
.alectryon-io .alectryon-goal > label:before {
|
||||
border: 1px solid #babdb6;
|
||||
border-radius: 1em;
|
||||
box-sizing: border-box;
|
||||
content: '';
|
||||
display: inline-block;
|
||||
font-weight: bold;
|
||||
height: 0.25em;
|
||||
margin-bottom: 0.15em;
|
||||
vertical-align: middle;
|
||||
width: 0.75em;
|
||||
}
|
||||
|
||||
.alectryon-toggle-label:before,
|
||||
.alectryon-io .alectryon-goal > label:before {
|
||||
margin-right: 0.25em;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-goal > label:before {
|
||||
margin-top: 0.125em;
|
||||
}
|
||||
|
||||
.alectryon-io label.alectryon-input {
|
||||
padding-right: 1em; /* Prevent line wraps before the checkbox bubble */
|
||||
}
|
||||
|
||||
.alectryon-io label.alectryon-input:after {
|
||||
margin-left: 0.25em;
|
||||
margin-right: -1em; /* Compensate for the anti-wrapping space */
|
||||
}
|
||||
|
||||
.alectryon-failed {
|
||||
/* Underlines are broken in Chrome (they reset at each element boundary)… */
|
||||
/* text-decoration: red wavy underline; */
|
||||
/* … but it isn't too noticeable with dots */
|
||||
text-decoration: red dotted underline;
|
||||
text-decoration-skip-ink: none;
|
||||
/* Chrome prints background images in low resolution, yielding a blurry underline */
|
||||
/* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */
|
||||
}
|
||||
|
||||
/* Wrapping :hover rules in a media query ensures that tapping a Coq sentence
|
||||
doesn't trigger its :hover state (otherwise, on mobile, tapping a sentence to
|
||||
hide its output causes it to remain visible (its :hover state gets triggered.
|
||||
We only do it for the default style though, since other styles don't put the
|
||||
output over the main text, so showing too much is not an issue. */
|
||||
@media (any-hover: hover) {
|
||||
.alectryon-bubble:hover:before,
|
||||
.alectryon-toggle-label:hover:before,
|
||||
.alectryon-io label.alectryon-input:hover:after {
|
||||
background: #eeeeec;
|
||||
}
|
||||
|
||||
.alectryon-io label.alectryon-input:hover {
|
||||
text-decoration: underline dotted #babdb6;
|
||||
text-shadow: 0 0 1px rgb(46, 52, 54, 0.3); /* #2e3436 + opacity */
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-sentence:hover .alectryon-output,
|
||||
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper,
|
||||
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper {
|
||||
z-index: 2; /* Place hovered goals above .alectryon-sentence.alectryon-target ones */
|
||||
}
|
||||
}
|
||||
|
||||
.alectryon-toggle:checked + .alectryon-toggle-label:before,
|
||||
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked + label.alectryon-input:after,
|
||||
.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal > label:before {
|
||||
background-color: #babdb6;
|
||||
border-color: #babdb6;
|
||||
}
|
||||
|
||||
/* Disable clicks on sentences when the document-wide toggle is set. */
|
||||
.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input {
|
||||
cursor: unset;
|
||||
pointer-events: none;
|
||||
}
|
||||
|
||||
/* Hide individual checkboxes when the document-wide toggle is set. */
|
||||
.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input:after {
|
||||
display: none;
|
||||
}
|
||||
|
||||
/* .alectryon-output is displayed by toggles, :hover, and .alectryon-target rules */
|
||||
.alectryon-io .alectryon-output {
|
||||
box-sizing: border-box;
|
||||
display: none;
|
||||
left: 0;
|
||||
right: 0;
|
||||
position: absolute;
|
||||
padding: 0.25em 0;
|
||||
overflow: visible; /* Let box-shadows overflow */
|
||||
z-index: 1; /* Default to an index lower than that used by :hover */
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-type-info-wrapper {
|
||||
position: absolute;
|
||||
display: inline-block;
|
||||
width: 100%;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-type-info-wrapper.full-width {
|
||||
left: 0;
|
||||
min-width: 100%;
|
||||
max-width: 100%;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-type-info .goal-separator {
|
||||
height: unset;
|
||||
margin-top: 0em;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info {
|
||||
box-sizing: border-box;
|
||||
bottom: 100%;
|
||||
position: absolute;
|
||||
/*padding: 0.25em 0;*/
|
||||
visibility: hidden;
|
||||
overflow: visible; /* Let box-shadows overflow */
|
||||
z-index: 1; /* Default to an index lower than that used by :hover */
|
||||
white-space: pre-wrap !important;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-type-info-wrapper .alectryon-type-info .alectryon-goal.alectryon-docstring {
|
||||
white-space: pre-wrap !important;
|
||||
}
|
||||
|
||||
@media (any-hover: hover) { /* See note above about this @media query */
|
||||
.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) {
|
||||
display: block;
|
||||
}
|
||||
|
||||
.alectryon-io.output-hidden .alectryon-sentence:hover .alectryon-output:not(:hover) {
|
||||
display: none !important;
|
||||
}
|
||||
|
||||
.alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
|
||||
.alectryon-io.type-info-hidden .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
|
||||
/*visibility: hidden !important;*/
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info,
|
||||
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
|
||||
visibility: visible;
|
||||
transition-delay: 0.5s;
|
||||
}
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output {
|
||||
display: block;
|
||||
}
|
||||
|
||||
/* Indicate active (hovered or targeted) goals with a shadow. */
|
||||
.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
|
||||
.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-messages,
|
||||
.alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
|
||||
.alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-goals,
|
||||
.alectryon-io .alectryon-token:hover .alectryon-type-info-wrapper .alectryon-type-info {
|
||||
box-shadow: 2px 2px 2px gray;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-hyps {
|
||||
display: none;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-extra-goals .alectryon-extra-goal-toggle:not(:checked) + .alectryon-goal label.goal-separator hr {
|
||||
/* Dashes indicate that the hypotheses are hidden */
|
||||
border-top-style: dashed;
|
||||
}
|
||||
|
||||
|
||||
/* Show just a small preview of the other goals; this is undone by the
|
||||
"extra-goal" toggle and by :hover and .alectryon-target in windowed mode. */
|
||||
.alectryon-io .alectryon-extra-goals .alectryon-goal .goal-conclusion {
|
||||
max-height: 5.2em;
|
||||
overflow-y: auto;
|
||||
/* Combining ‘overflow-y: auto’ with ‘display: inline-block’ causes extra space
|
||||
to be added below the box. ‘vertical-align: middle’ gets rid of it. */
|
||||
vertical-align: middle;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-goals,
|
||||
.alectryon-io .alectryon-messages {
|
||||
background: #f6f7f6;
|
||||
/*border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */
|
||||
display: block;
|
||||
padding: 0.25em;
|
||||
}
|
||||
|
||||
.alectryon-message::before {
|
||||
content: '';
|
||||
float: right;
|
||||
/* etc/svg/square-bubble-xl.svg */
|
||||
background: url("data:image/svg+xml,%3Csvg width='14' height='14' viewBox='0 0 3.704 3.704' xmlns='http://www.w3.org/2000/svg'%3E%3Cg fill-rule='evenodd' stroke='%23000' stroke-width='.264'%3E%3Cpath d='M.794.934h2.115M.794 1.463h1.455M.794 1.992h1.852'/%3E%3C/g%3E%3Cpath d='M.132.14v2.646h.794v.661l.926-.661h1.72V.14z' fill='none' stroke='%23000' stroke-width='.265'/%3E%3C/svg%3E") top right no-repeat;
|
||||
height: 14px;
|
||||
width: 14px;
|
||||
}
|
||||
|
||||
.alectryon-toggle:checked + label + .alectryon-container {
|
||||
width: unset;
|
||||
}
|
||||
|
||||
/* Show goals when a toggle is set */
|
||||
.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output,
|
||||
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output {
|
||||
display: block;
|
||||
position: static;
|
||||
width: unset;
|
||||
background: unset; /* Override the backgrounds set in floating in windowed mode */
|
||||
padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */
|
||||
}
|
||||
|
||||
.alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps,
|
||||
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output .goal-hyps {
|
||||
/* Overridden back in windowed style */
|
||||
flex-flow: row wrap;
|
||||
justify-content: flex-start;
|
||||
}
|
||||
|
||||
.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
|
||||
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
|
||||
display: block;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-hyps {
|
||||
display: flex;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion {
|
||||
max-height: unset;
|
||||
overflow-y: unset;
|
||||
}
|
||||
|
||||
.alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence > .alectryon-toggle ~ .alectryon-wsp,
|
||||
.alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-wsp {
|
||||
display: none;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-messages,
|
||||
.alectryon-io .alectryon-message,
|
||||
.alectryon-io .alectryon-goals,
|
||||
.alectryon-io .alectryon-goal,
|
||||
.alectryon-io .goal-hyps > span,
|
||||
.alectryon-io .goal-conclusion {
|
||||
border-radius: 0.15em;
|
||||
}
|
||||
|
||||
.alectryon-io .alectryon-goal,
|
||||
.alectryon-io .alectryon-message {
|
||||
align-items: center;
|
||||
background: #f6f7f6;
|
||||
border: 0em;
|
||||
display: block;
|
||||
flex-direction: column;
|
||||
margin: 0.25em;
|
||||
padding: 0.5em;
|
||||
position: relative;
|
||||
}
|
||||
|
||||
.alectryon-io .goal-hyps {
|
||||
align-content: space-around;
|
||||
align-items: baseline;
|
||||
display: flex;
|
||||
flex-flow: column nowrap; /* re-stated in windowed mode */
|
||||
justify-content: space-around;
|
||||
/* LATER use a ‘gap’ property instead of margins once supported */
|
||||
margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */
|
||||
padding-bottom: 0.35em; /* 0.5em-0.15em to cancel the 0.5em of .goal-separator */
|
||||
}
|
||||
|
||||
.alectryon-io .goal-hyps > br {
|
||||
display: none; /* Only for RSS readers */
|
||||
}
|
||||
|
||||
.alectryon-io .goal-hyps > span,
|
||||
.alectryon-io .goal-conclusion {
|
||||
/*background: #eeeeec;*/
|
||||
display: inline-block;
|
||||
padding: 0.15em 0.35em;
|
||||
}
|
||||
|
||||
.alectryon-io .goal-hyps > span {
|
||||
align-items: baseline;
|
||||
display: inline-flex;
|
||||
margin: 0.15em 0.25em;
|
||||
}
|
||||
|
||||
.alectryon-block var,
|
||||
.alectryon-inline var,
|
||||
.alectryon-io .goal-hyps > span > var {
|
||||
font-weight: 600;
|
||||
font-style: unset;
|
||||
}
|
||||
|
||||
.alectryon-io .goal-hyps > span > var {
|
||||
/* Shrink the list of names, but let it grow as long as space is available. */
|
||||
flex-basis: min-content;
|
||||
flex-grow: 1;
|
||||
}
|
||||
|
||||
.alectryon-io .goal-hyps > span b {
|
||||
font-weight: 600;
|
||||
margin: 0 0 0 0.5em;
|
||||
white-space: pre;
|
||||
}
|
||||
|
||||
.alectryon-io .hyp-body,
|
||||
.alectryon-io .hyp-type {
|
||||
display: flex;
|
||||
align-items: baseline;
|
||||
}
|
||||
|
||||
.alectryon-io .goal-separator {
|
||||
align-items: center;
|
||||
display: flex;
|
||||
flex-direction: row;
|
||||
height: 1em; /* Fixed height to ignore goal name and markers */
|
||||
margin-top: -0.5em; /* Compensated in .goal-hyps when shown */
|
||||
}
|
||||
|
||||
.alectryon-io .goal-separator hr {
|
||||
border: none;
|
||||
border-top: thin solid #555753;
|
||||
display: block;
|
||||
flex-grow: 1;
|
||||
margin: 0;
|
||||
}
|
||||
|
||||
.alectryon-io .goal-separator .goal-name {
|
||||
font-size: 0.75em;
|
||||
margin-left: 0.5em;
|
||||
}
|
||||
|
||||
/**********/
|
||||
/* Banner */
|
||||
/**********/
|
||||
|
||||
.alectryon-banner {
|
||||
background: #eeeeec;
|
||||
border: 1px solid #babcbd;
|
||||
font-size: 0.75em;
|
||||
padding: 0.25em;
|
||||
text-align: center;
|
||||
margin: 1em 0;
|
||||
}
|
||||
|
||||
.alectryon-banner a {
|
||||
cursor: pointer;
|
||||
text-decoration: underline;
|
||||
}
|
||||
|
||||
.alectryon-banner kbd {
|
||||
background: #d3d7cf;
|
||||
border-radius: 0.15em;
|
||||
border: 1px solid #babdb6;
|
||||
box-sizing: border-box;
|
||||
display: inline-block;
|
||||
font-family: inherit;
|
||||
font-size: 0.9em;
|
||||
height: 1.3em;
|
||||
line-height: 1.2em;
|
||||
margin: -0.25em 0;
|
||||
padding: 0 0.25em;
|
||||
vertical-align: middle;
|
||||
}
|
||||
|
||||
/**********/
|
||||
/* Toggle */
|
||||
/**********/
|
||||
|
||||
.alectryon-toggle-label {
|
||||
margin: 1rem 0;
|
||||
}
|
||||
|
||||
/******************/
|
||||
/* Floating style */
|
||||
/******************/
|
||||
|
||||
/* If there's space, display goals to the right of the code, not below it. */
|
||||
@media (min-width: 80rem) {
|
||||
/* Unlike the windowed case, we don't want to move output blocks to the side
|
||||
when they are both :checked and -targeted, since it gets confusing as
|
||||
things jump around; hence the commented-output part of the selector,
|
||||
which would otherwise increase specificity */
|
||||
.alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output,
|
||||
.alectryon-floating .alectryon-sentence:hover .alectryon-output {
|
||||
top: 0;
|
||||
left: 100%;
|
||||
right: -100%;
|
||||
padding: 0 0.5em;
|
||||
position: absolute;
|
||||
}
|
||||
|
||||
.alectryon-floating .alectryon-output {
|
||||
min-height: 100%;
|
||||
}
|
||||
|
||||
.alectryon-floating .alectryon-sentence:hover .alectryon-output {
|
||||
background: white; /* Ensure that short goals hide long ones */
|
||||
}
|
||||
|
||||
/* This odd margin-bottom property prevents the sticky div from bumping
|
||||
against the bottom of its container (.alectryon-output). The alternative
|
||||
would be enlarging .alectryon-output, but that would cause overflows,
|
||||
enlarging scrollbars and yielding scrolling towards the bottom of the
|
||||
page. Doing things this way instead makes it possible to restrict
|
||||
.alectryon-output to a reasonable size (100%, through top = bottom = 0).
|
||||
See also https://stackoverflow.com/questions/43909940/. */
|
||||
/* See note on specificity above */
|
||||
.alectryon-floating .alectryon-sentence.alectryon-target /* > .alectryon-toggle ~ */ .alectryon-output > div,
|
||||
.alectryon-floating .alectryon-sentence:hover .alectryon-output > div {
|
||||
margin-bottom: -200%;
|
||||
position: sticky;
|
||||
top: 0;
|
||||
}
|
||||
|
||||
.alectryon-floating .alectryon-toggle:checked + label + .alectryon-container .alectryon-sentence .alectryon-output > div,
|
||||
.alectryon-floating .alectryon-io .alectryon-sentence > .alectryon-toggle:checked ~ .alectryon-output > div {
|
||||
margin-bottom: unset; /* Undo the margin */
|
||||
}
|
||||
|
||||
/* Float underneath the current fragment
|
||||
@media (max-width: 80rem) {
|
||||
.alectryon-floating .alectryon-output {
|
||||
top: 100%;
|
||||
}
|
||||
} */
|
||||
}
|
||||
|
||||
/********************/
|
||||
/* Multi-pane style */
|
||||
/********************/
|
||||
|
||||
.alectryon-windowed {
|
||||
border: 0 solid #2e3436;
|
||||
box-sizing: border-box;
|
||||
}
|
||||
|
||||
.alectryon-windowed .alectryon-sentence:hover .alectryon-output {
|
||||
background: white; /* Ensure that short goals hide long ones */
|
||||
}
|
||||
|
||||
.alectryon-windowed .alectryon-output {
|
||||
position: fixed; /* Overwritten by the ‘:checked’ rules */
|
||||
}
|
||||
|
||||
/* See note about specificity below */
|
||||
.alectryon-windowed .alectryon-sentence:hover .alectryon-output,
|
||||
.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
|
||||
padding: 0.5em;
|
||||
overflow-y: auto; /* Windowed contents may need to scroll */
|
||||
}
|
||||
|
||||
.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-messages,
|
||||
.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-messages,
|
||||
.alectryon-windowed .alectryon-io .alectryon-sentence:hover .alectryon-output:not(:hover) .alectryon-goals,
|
||||
.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .alectryon-goals {
|
||||
box-shadow: none; /* A shadow is unnecessary here and incompatible with overflow-y set to auto */
|
||||
}
|
||||
|
||||
.alectryon-windowed .alectryon-io .alectryon-sentence.alectryon-target .alectryon-output .goal-hyps {
|
||||
/* Restated to override the :checked style */
|
||||
flex-flow: column nowrap;
|
||||
justify-content: space-around;
|
||||
}
|
||||
|
||||
|
||||
.alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-extra-goals .alectryon-goal .goal-conclusion
|
||||
/* Like .alectryon-io .alectryon-extra-goal-toggle:checked + .alectryon-goal .goal-conclusion */ {
|
||||
max-height: unset;
|
||||
overflow-y: unset;
|
||||
}
|
||||
|
||||
.alectryon-windowed .alectryon-output > div {
|
||||
display: flex; /* Put messages after goals */
|
||||
flex-direction: column-reverse;
|
||||
}
|
||||
|
||||
/*********************/
|
||||
/* Standalone styles */
|
||||
/*********************/
|
||||
|
||||
.alectryon-standalone {
|
||||
font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
|
||||
line-height: 1.5;
|
||||
}
|
||||
|
||||
@media screen and (min-width: 50rem) {
|
||||
html.alectryon-standalone {
|
||||
/* Prevent flickering when hovering a block causes scrollbars to appear. */
|
||||
margin-left: calc(100vw - 100%);
|
||||
margin-right: 0;
|
||||
}
|
||||
}
|
||||
|
||||
/* Coqdoc */
|
||||
|
||||
.alectryon-coqdoc .doc .code,
|
||||
.alectryon-coqdoc .doc .inlinecode,
|
||||
.alectryon-coqdoc .doc .comment {
|
||||
display: inline;
|
||||
}
|
||||
|
||||
.alectryon-coqdoc .doc .comment {
|
||||
color: #eeeeec;
|
||||
}
|
||||
|
||||
.alectryon-coqdoc .doc .paragraph {
|
||||
height: 0.75em;
|
||||
}
|
||||
|
||||
/* Centered, Floating */
|
||||
|
||||
.alectryon-standalone .alectryon-centered,
|
||||
.alectryon-standalone .alectryon-floating {
|
||||
max-width: 50rem;
|
||||
margin: auto;
|
||||
}
|
||||
|
||||
@media (min-width: 80rem) {
|
||||
.alectryon-standalone .alectryon-floating {
|
||||
max-width: 80rem;
|
||||
}
|
||||
|
||||
.alectryon-standalone .alectryon-floating > * {
|
||||
width: 50%;
|
||||
margin-left: 0;
|
||||
}
|
||||
}
|
||||
|
||||
/* Windowed */
|
||||
|
||||
.alectryon-standalone .alectryon-windowed {
|
||||
display: block;
|
||||
margin: 0;
|
||||
overflow-y: auto;
|
||||
position: absolute;
|
||||
padding: 0 1em;
|
||||
}
|
||||
|
||||
.alectryon-standalone .alectryon-windowed > * {
|
||||
/* Override properties of docutils_basic.css */
|
||||
margin-left: 0;
|
||||
max-width: unset;
|
||||
}
|
||||
|
||||
.alectryon-standalone .alectryon-windowed .alectryon-io {
|
||||
box-sizing: border-box;
|
||||
width: 100%;
|
||||
}
|
||||
|
||||
/* No need to predicate the ‘:hover’ rules below on ‘:not(:checked)’, since ‘left’,
|
||||
‘right’, ‘top’, and ‘bottom’ will be inactived by the :checked rules setting
|
||||
‘position’ to ‘static’ */
|
||||
|
||||
|
||||
/* Specificity: We want the output to stay inline when hovered while unfolded
|
||||
(:checked), but we want it to move when it's targeted (i.e. when the user
|
||||
is browsing goals one by one using the keyboard, in which case we want to
|
||||
goals to appear in consistent locations). The selectors below ensure
|
||||
that :hover < :checked < -targeted in terms of specificity. */
|
||||
/* LATER: Reimplement this stuff with CSS variables */
|
||||
.alectryon-windowed .alectryon-sentence.alectryon-target > .alectryon-toggle ~ .alectryon-output {
|
||||
position: fixed;
|
||||
}
|
||||
|
||||
@media screen and (min-width: 60rem) {
|
||||
.alectryon-standalone .alectryon-windowed {
|
||||
border-right-width: thin;
|
||||
bottom: 0;
|
||||
left: 0;
|
||||
right: 50%;
|
||||
top: 0;
|
||||
}
|
||||
|
||||
.alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
|
||||
.alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
|
||||
bottom: 0;
|
||||
left: 50%;
|
||||
right: 0;
|
||||
top: 0;
|
||||
}
|
||||
}
|
||||
|
||||
@media screen and (max-width: 60rem) {
|
||||
.alectryon-standalone .alectryon-windowed {
|
||||
border-bottom-width: 1px;
|
||||
bottom: 40%;
|
||||
left: 0;
|
||||
right: 0;
|
||||
top: 0;
|
||||
}
|
||||
|
||||
.alectryon-standalone .alectryon-windowed .alectryon-sentence:hover .alectryon-output,
|
||||
.alectryon-standalone .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-output {
|
||||
bottom: 0;
|
||||
left: 0;
|
||||
right: 0;
|
||||
top: 60%;
|
||||
}
|
||||
}
|
||||
|
|
@ -0,0 +1,172 @@
|
|||
var Alectryon;
|
||||
(function(Alectryon) {
|
||||
(function (slideshow) {
|
||||
function anchor(sentence) { return "#" + sentence.id; }
|
||||
|
||||
function current_sentence() { return slideshow.sentences[slideshow.pos]; }
|
||||
|
||||
function unhighlight() {
|
||||
var sentence = current_sentence();
|
||||
if (sentence) sentence.classList.remove("alectryon-target");
|
||||
slideshow.pos = -1;
|
||||
}
|
||||
|
||||
function highlight(sentence) {
|
||||
sentence.classList.add("alectryon-target");
|
||||
}
|
||||
|
||||
function scroll(sentence) {
|
||||
// Put the top of the current fragment close to the top of the
|
||||
// screen, but scroll it out of view if showing it requires pushing
|
||||
// the sentence past half of the screen. If sentence is already in
|
||||
// a reasonable position, don't move.
|
||||
var parent = sentence.parentElement;
|
||||
/* We want to scroll the whole document, so start at root… */
|
||||
while (parent && !parent.classList.contains("alectryon-root"))
|
||||
parent = parent.parentElement;
|
||||
/* … and work up from there to find a scrollable element.
|
||||
parent.scrollHeight can be greater than parent.clientHeight
|
||||
without showing scrollbars, so we add a 10px buffer. */
|
||||
while (parent && parent.scrollHeight <= parent.clientHeight + 10)
|
||||
parent = parent.parentElement;
|
||||
/* <body> and <html> elements can have their client rect overflow
|
||||
* the window if their height is unset, so scroll the window
|
||||
* instead */
|
||||
if (parent && (parent.nodeName == "BODY" || parent.nodeName == "HTML"))
|
||||
parent = null;
|
||||
|
||||
var rect = function(e) { return e.getBoundingClientRect(); };
|
||||
var parent_box = parent ? rect(parent) : { y: 0, height: window.innerHeight },
|
||||
sentence_y = rect(sentence).y - parent_box.y,
|
||||
fragment_y = rect(sentence.parentElement).y - parent_box.y;
|
||||
|
||||
// The assertion below sometimes fails for the first element in a block.
|
||||
// console.assert(sentence_y >= fragment_y);
|
||||
|
||||
if (sentence_y < 0.1 * parent_box.height ||
|
||||
sentence_y > 0.7 * parent_box.height) {
|
||||
(parent || window).scrollBy(
|
||||
0, Math.max(sentence_y - 0.5 * parent_box.height,
|
||||
fragment_y - 0.1 * parent_box.height));
|
||||
}
|
||||
}
|
||||
|
||||
function highlighted(pos) {
|
||||
return slideshow.pos == pos;
|
||||
}
|
||||
|
||||
function navigate(pos, inhibitScroll) {
|
||||
unhighlight();
|
||||
slideshow.pos = Math.min(Math.max(pos, 0), slideshow.sentences.length - 1);
|
||||
var sentence = current_sentence();
|
||||
highlight(sentence);
|
||||
if (!inhibitScroll)
|
||||
scroll(sentence);
|
||||
}
|
||||
|
||||
var keys = {
|
||||
PAGE_UP: 33,
|
||||
PAGE_DOWN: 34,
|
||||
ARROW_UP: 38,
|
||||
ARROW_DOWN: 40,
|
||||
h: 72, l: 76, p: 80, n: 78
|
||||
};
|
||||
|
||||
function onkeydown(e) {
|
||||
e = e || window.event;
|
||||
if (e.ctrlKey || e.metaKey) {
|
||||
if (e.keyCode == keys.ARROW_UP)
|
||||
slideshow.previous();
|
||||
else if (e.keyCode == keys.ARROW_DOWN)
|
||||
slideshow.next();
|
||||
else
|
||||
return;
|
||||
} else {
|
||||
// if (e.keyCode == keys.PAGE_UP || e.keyCode == keys.p || e.keyCode == keys.h)
|
||||
// slideshow.previous();
|
||||
// else if (e.keyCode == keys.PAGE_DOWN || e.keyCode == keys.n || e.keyCode == keys.l)
|
||||
// slideshow.next();
|
||||
// else
|
||||
return;
|
||||
}
|
||||
e.preventDefault();
|
||||
}
|
||||
|
||||
function start() {
|
||||
slideshow.navigate(0);
|
||||
}
|
||||
|
||||
function toggleHighlight(idx) {
|
||||
if (highlighted(idx))
|
||||
unhighlight();
|
||||
else
|
||||
navigate(idx, true);
|
||||
}
|
||||
|
||||
function handleClick(evt) {
|
||||
if (evt.ctrlKey || evt.metaKey) {
|
||||
var sentence = evt.currentTarget;
|
||||
|
||||
// Ensure that the goal is shown on the side, not inline
|
||||
var checkbox = sentence.getElementsByClassName("alectryon-toggle")[0];
|
||||
if (checkbox)
|
||||
checkbox.checked = false;
|
||||
|
||||
toggleHighlight(sentence.alectryon_index);
|
||||
evt.preventDefault();
|
||||
}
|
||||
}
|
||||
|
||||
function init() {
|
||||
document.onkeydown = onkeydown;
|
||||
slideshow.pos = -1;
|
||||
slideshow.sentences = Array.from(document.getElementsByClassName("alectryon-sentence"));
|
||||
slideshow.sentences.forEach(function (s, idx) {
|
||||
s.addEventListener('click', handleClick, false);
|
||||
s.alectryon_index = idx;
|
||||
});
|
||||
}
|
||||
|
||||
slideshow.start = start;
|
||||
slideshow.end = unhighlight;
|
||||
slideshow.navigate = navigate;
|
||||
slideshow.next = function() { navigate(slideshow.pos + 1); };
|
||||
slideshow.previous = function() { navigate(slideshow.pos + -1); };
|
||||
window.addEventListener('DOMContentLoaded', init);
|
||||
})(Alectryon.slideshow || (Alectryon.slideshow = {}));
|
||||
|
||||
(function (styles) {
|
||||
var styleNames = ["centered", "floating", "windowed"];
|
||||
|
||||
function className(style) {
|
||||
return "alectryon-" + style;
|
||||
}
|
||||
|
||||
function setStyle(style) {
|
||||
var root = document.getElementsByClassName("alectryon-root")[0];
|
||||
styleNames.forEach(function (s) {
|
||||
root.classList.remove(className(s)); });
|
||||
root.classList.add(className(style));
|
||||
}
|
||||
|
||||
function init() {
|
||||
var banner = document.getElementsByClassName("alectryon-banner")[0];
|
||||
if (banner) {
|
||||
banner.append(" Style: ");
|
||||
styleNames.forEach(function (styleName, idx) {
|
||||
var s = styleName;
|
||||
var a = document.createElement("a");
|
||||
a.onclick = function() { setStyle(s); };
|
||||
a.append(styleName);
|
||||
if (idx > 0) banner.append("; ");
|
||||
banner.appendChild(a);
|
||||
});
|
||||
banner.append(".");
|
||||
}
|
||||
}
|
||||
|
||||
window.addEventListener('DOMContentLoaded', init);
|
||||
|
||||
styles.setStyle = setStyle;
|
||||
})(Alectryon.styles || (Alectryon.styles = {}));
|
||||
})(Alectryon || (Alectryon = {}));
|
||||
|
|
@ -0,0 +1,593 @@
|
|||
/******************************************************************************
|
||||
The MIT License (MIT)
|
||||
|
||||
Copyright (c) 2014 Matthias Eisen
|
||||
Further changes Copyright (c) 2020, 2021 Clément Pit-Claudel
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of this software and associated documentation files (the "Software"), to deal
|
||||
in the Software without restriction, including without limitation the rights
|
||||
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in
|
||||
all copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
||||
THE SOFTWARE.
|
||||
******************************************************************************/
|
||||
|
||||
kbd,
|
||||
pre,
|
||||
samp,
|
||||
tt,
|
||||
body code, /* Increase specificity to override IBM's stylesheet */
|
||||
body code.highlight,
|
||||
.docutils.literal {
|
||||
font-family: 'Iosevka Slab Web', 'Iosevka Web', 'Iosevka Slab', 'Iosevka', 'Fira Code', monospace;
|
||||
font-feature-settings: "COQX" 1 /* Coq ligatures */, "XV00" 1 /* Legacy */, "calt" 1 /* Fallback */;
|
||||
}
|
||||
|
||||
body {
|
||||
color: #111;
|
||||
font-family: 'IBM Plex Serif', 'PT Serif', 'Merriweather', 'DejaVu Serif', serif;
|
||||
line-height: 1.5;
|
||||
}
|
||||
|
||||
main, div.document {
|
||||
margin: 0 auto;
|
||||
max-width: 720px;
|
||||
}
|
||||
|
||||
|
||||
/* ========== Headings ========== */
|
||||
|
||||
h1, h2, h3, h4, h5, h6 {
|
||||
font-weight: normal;
|
||||
margin-top: 1.5em;
|
||||
}
|
||||
|
||||
h1.section-subtitle,
|
||||
h2.section-subtitle,
|
||||
h3.section-subtitle,
|
||||
h4.section-subtitle,
|
||||
h5.section-subtitle,
|
||||
h6.section-subtitle {
|
||||
margin-top: 0.4em;
|
||||
}
|
||||
|
||||
h1.title {
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
h2.subtitle {
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
span.section-subtitle {
|
||||
font-size: 80%,
|
||||
}
|
||||
|
||||
/* //-------- Headings ---------- */
|
||||
|
||||
|
||||
/* ========== Images ========== */
|
||||
|
||||
img,
|
||||
.figure,
|
||||
object {
|
||||
display: block;
|
||||
margin-left: auto;
|
||||
margin-right: auto;
|
||||
}
|
||||
|
||||
div.figure {
|
||||
margin-left: 2em;
|
||||
margin-right: 2em;
|
||||
}
|
||||
|
||||
img.align-left, .figure.align-left, object.align-left {
|
||||
clear: left;
|
||||
float: left;
|
||||
margin-right: 1em;
|
||||
}
|
||||
|
||||
img.align-right, .figure.align-right, object.align-right {
|
||||
clear: right;
|
||||
float: right;
|
||||
margin-left: 1em;
|
||||
}
|
||||
|
||||
img.align-center, .figure.align-center, object.align-center {
|
||||
display: block;
|
||||
margin-left: auto;
|
||||
margin-right: auto;
|
||||
}
|
||||
|
||||
/* reset inner alignment in figures */
|
||||
div.align-right {
|
||||
text-align: inherit;
|
||||
}
|
||||
|
||||
object[type="image/svg+xml"],
|
||||
object[type="application/x-shockwave-flash"] {
|
||||
overflow: hidden;
|
||||
}
|
||||
|
||||
/* //-------- Images ---------- */
|
||||
|
||||
|
||||
|
||||
/* ========== Literal Blocks ========== */
|
||||
|
||||
.docutils.literal {
|
||||
background-color: #eee;
|
||||
padding: 0 0.2em;
|
||||
border-radius: 0.1em;
|
||||
}
|
||||
|
||||
pre.address {
|
||||
margin-bottom: 0;
|
||||
margin-top: 0;
|
||||
font: inherit;
|
||||
}
|
||||
|
||||
pre.literal-block {
|
||||
border-left: solid 5px #ccc;
|
||||
padding: 1em;
|
||||
}
|
||||
|
||||
pre.literal-block, pre.doctest-block, pre.math, pre.code {
|
||||
}
|
||||
|
||||
span.interpreted {
|
||||
}
|
||||
|
||||
span.pre {
|
||||
white-space: pre;
|
||||
}
|
||||
|
||||
pre.code .ln {
|
||||
color: grey;
|
||||
}
|
||||
pre.code, code {
|
||||
border-style: none;
|
||||
/* ! padding: 1em 0; */ /* Removed because that large hitbox bleeds over links on other lines */
|
||||
}
|
||||
pre.code .comment, code .comment {
|
||||
color: #888;
|
||||
}
|
||||
pre.code .keyword, code .keyword {
|
||||
font-weight: bold;
|
||||
color: #080;
|
||||
}
|
||||
pre.code .literal.string, code .literal.string {
|
||||
color: #d20;
|
||||
background-color: #fff0f0;
|
||||
}
|
||||
pre.code .literal.number, code .literal.number {
|
||||
color: #00d;
|
||||
}
|
||||
pre.code .name.builtin, code .name.builtin {
|
||||
color: #038;
|
||||
color: #820;
|
||||
}
|
||||
pre.code .name.namespace, code .name.namespace {
|
||||
color: #b06;
|
||||
}
|
||||
pre.code .deleted, code .deleted {
|
||||
background-color: #fdd;
|
||||
}
|
||||
pre.code .inserted, code .inserted {
|
||||
background-color: #dfd;
|
||||
}
|
||||
|
||||
|
||||
/* //-------- Literal Blocks --------- */
|
||||
|
||||
|
||||
/* ========== Tables ========== */
|
||||
|
||||
table {
|
||||
border-spacing: 0;
|
||||
border-collapse: collapse;
|
||||
border-style: none;
|
||||
border-top: solid thin #111;
|
||||
border-bottom: solid thin #111;
|
||||
}
|
||||
|
||||
td,
|
||||
th {
|
||||
border: none;
|
||||
padding: 0.5em;
|
||||
vertical-align: top;
|
||||
}
|
||||
|
||||
th {
|
||||
border-top: solid thin #111;
|
||||
border-bottom: solid thin #111;
|
||||
background-color: #ddd;
|
||||
}
|
||||
|
||||
|
||||
table.field-list,
|
||||
table.footnote,
|
||||
table.citation,
|
||||
table.option-list {
|
||||
border: none;
|
||||
}
|
||||
table.docinfo {
|
||||
margin: 2em 4em;
|
||||
}
|
||||
|
||||
table.docutils {
|
||||
margin: 1em 0;
|
||||
}
|
||||
|
||||
table.docutils th.field-name,
|
||||
table.docinfo th.docinfo-name {
|
||||
border: none;
|
||||
background: none;
|
||||
font-weight: bold ;
|
||||
text-align: left ;
|
||||
white-space: nowrap ;
|
||||
padding-left: 0;
|
||||
vertical-align: middle;
|
||||
}
|
||||
|
||||
table.docutils.booktabs {
|
||||
border: none;
|
||||
border-top: medium solid;
|
||||
border-bottom: medium solid;
|
||||
border-collapse: collapse;
|
||||
}
|
||||
|
||||
table.docutils.booktabs * {
|
||||
border: none;
|
||||
}
|
||||
table.docutils.booktabs th {
|
||||
border-bottom: thin solid;
|
||||
text-align: left;
|
||||
}
|
||||
|
||||
span.option {
|
||||
white-space: nowrap;
|
||||
}
|
||||
|
||||
table caption {
|
||||
margin-bottom: 2px;
|
||||
}
|
||||
|
||||
/* //-------- Tables ---------- */
|
||||
|
||||
|
||||
/* ========== Lists ========== */
|
||||
|
||||
ol.simple, ul.simple {
|
||||
margin-bottom: 1em;
|
||||
}
|
||||
|
||||
ol.arabic {
|
||||
list-style: decimal;
|
||||
}
|
||||
|
||||
ol.loweralpha {
|
||||
list-style: lower-alpha;
|
||||
}
|
||||
|
||||
ol.upperalpha {
|
||||
list-style: upper-alpha;
|
||||
}
|
||||
|
||||
ol.lowerroman {
|
||||
list-style: lower-roman;
|
||||
}
|
||||
|
||||
ol.upperroman {
|
||||
list-style: upper-roman;
|
||||
}
|
||||
|
||||
dl.docutils dd {
|
||||
margin-bottom: 0.5em;
|
||||
}
|
||||
|
||||
|
||||
dl.docutils dt {
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
/* //-------- Lists ---------- */
|
||||
|
||||
|
||||
/* ========== Sidebar ========== */
|
||||
|
||||
div.sidebar {
|
||||
margin: 0 0 0.5em 1em ;
|
||||
border-left: solid medium #111;
|
||||
padding: 1em ;
|
||||
width: 40% ;
|
||||
float: right ;
|
||||
clear: right;
|
||||
}
|
||||
|
||||
div.sidebar {
|
||||
font-size: 0.9rem;
|
||||
}
|
||||
|
||||
p.sidebar-title {
|
||||
font-size: 1rem;
|
||||
font-weight: bold ;
|
||||
}
|
||||
|
||||
p.sidebar-subtitle {
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
/* //-------- Sidebar ---------- */
|
||||
|
||||
|
||||
/* ========== Topic ========== */
|
||||
|
||||
div.topic {
|
||||
border-left: thin solid #111;
|
||||
padding-left: 1em;
|
||||
}
|
||||
|
||||
div.topic p {
|
||||
padding: 0;
|
||||
}
|
||||
|
||||
p.topic-title {
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
/* //-------- Topic ---------- */
|
||||
|
||||
|
||||
/* ========== Header ========== */
|
||||
|
||||
div.header {
|
||||
font-family: "Century Gothic", CenturyGothic, Geneva, AppleGothic, sans-serif;
|
||||
font-size: 0.9rem;
|
||||
margin: 2em auto 4em auto;
|
||||
max-width: 960px;
|
||||
clear: both;
|
||||
}
|
||||
|
||||
hr.header {
|
||||
border: 0;
|
||||
height: 1px;
|
||||
margin-top: 1em;
|
||||
background-color: #111;
|
||||
}
|
||||
|
||||
/* //-------- Header ---------- */
|
||||
|
||||
|
||||
/* ========== Footer ========== */
|
||||
|
||||
div.footer {
|
||||
font-family: "Century Gothic", CenturyGothic, Geneva, AppleGothic, sans-serif;
|
||||
font-size: 0.9rem;
|
||||
margin: 6em auto 2em auto;
|
||||
max-width: 960px;
|
||||
clear: both;
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
hr.footer {
|
||||
border: 0;
|
||||
height: 1px;
|
||||
margin-bottom: 2em;
|
||||
background-color: #111;
|
||||
}
|
||||
|
||||
/* //-------- Footer ---------- */
|
||||
|
||||
|
||||
/* ========== Admonitions ========== */
|
||||
|
||||
div.admonition,
|
||||
div.attention,
|
||||
div.caution,
|
||||
div.danger,
|
||||
div.error,
|
||||
div.hint,
|
||||
div.important,
|
||||
div.note,
|
||||
div.tip,
|
||||
div.warning {
|
||||
border: solid thin #111;
|
||||
padding: 0 1em;
|
||||
}
|
||||
|
||||
div.error,
|
||||
div.danger {
|
||||
border-color: #a94442;
|
||||
background-color: #f2dede;
|
||||
}
|
||||
|
||||
div.hint,
|
||||
div.tip {
|
||||
border-color: #31708f;
|
||||
background-color: #d9edf7;
|
||||
}
|
||||
|
||||
div.attention,
|
||||
div.caution,
|
||||
div.warning {
|
||||
border-color: #8a6d3b;
|
||||
background-color: #fcf8e3;
|
||||
}
|
||||
|
||||
div.hint p.admonition-title,
|
||||
div.tip p.admonition-title {
|
||||
color: #31708f;
|
||||
font-weight: bold ;
|
||||
}
|
||||
|
||||
div.note p.admonition-title,
|
||||
div.admonition p.admonition-title,
|
||||
div.important p.admonition-title {
|
||||
font-weight: bold ;
|
||||
}
|
||||
|
||||
div.attention p.admonition-title,
|
||||
div.caution p.admonition-title,
|
||||
div.warning p.admonition-title {
|
||||
color: #8a6d3b;
|
||||
font-weight: bold ;
|
||||
}
|
||||
|
||||
div.danger p.admonition-title,
|
||||
div.error p.admonition-title,
|
||||
.code .error {
|
||||
color: #a94442;
|
||||
font-weight: bold ;
|
||||
}
|
||||
|
||||
/* //-------- Admonitions ---------- */
|
||||
|
||||
|
||||
/* ========== Table of Contents ========== */
|
||||
|
||||
div.contents {
|
||||
margin: 2em 0;
|
||||
border: none;
|
||||
}
|
||||
|
||||
ul.auto-toc {
|
||||
list-style-type: none;
|
||||
}
|
||||
|
||||
a.toc-backref {
|
||||
text-decoration: none ;
|
||||
color: #111;
|
||||
}
|
||||
|
||||
/* //-------- Table of Contents ---------- */
|
||||
|
||||
|
||||
|
||||
/* ========== Line Blocks========== */
|
||||
|
||||
div.line-block {
|
||||
display: block ;
|
||||
margin-top: 1em ;
|
||||
margin-bottom: 1em;
|
||||
}
|
||||
|
||||
div.line-block div.line-block {
|
||||
margin-top: 0 ;
|
||||
margin-bottom: 0 ;
|
||||
margin-left: 1.5em;
|
||||
}
|
||||
|
||||
/* //-------- Line Blocks---------- */
|
||||
|
||||
|
||||
/* ========== System Messages ========== */
|
||||
|
||||
div.system-messages {
|
||||
margin: 5em;
|
||||
}
|
||||
|
||||
div.system-messages h1 {
|
||||
color: red;
|
||||
}
|
||||
|
||||
div.system-message {
|
||||
border: medium outset ;
|
||||
padding: 1em;
|
||||
}
|
||||
|
||||
div.system-message p.system-message-title {
|
||||
color: red ;
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
/* //-------- System Messages---------- */
|
||||
|
||||
|
||||
/* ========== Helpers ========== */
|
||||
|
||||
.hidden {
|
||||
display: none;
|
||||
}
|
||||
|
||||
.align-left {
|
||||
text-align: left;
|
||||
}
|
||||
|
||||
.align-center {
|
||||
clear: both ;
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
.align-right {
|
||||
text-align: right;
|
||||
}
|
||||
|
||||
/* //-------- Helpers---------- */
|
||||
|
||||
|
||||
p.caption {
|
||||
font-style: italic;
|
||||
text-align: center;
|
||||
}
|
||||
|
||||
p.credits {
|
||||
font-style: italic ;
|
||||
font-size: smaller }
|
||||
|
||||
p.label {
|
||||
white-space: nowrap }
|
||||
|
||||
p.rubric {
|
||||
font-weight: bold ;
|
||||
font-size: larger ;
|
||||
color: maroon ;
|
||||
text-align: center }
|
||||
|
||||
p.attribution {
|
||||
text-align: right ;
|
||||
margin-left: 50% }
|
||||
|
||||
blockquote.epigraph {
|
||||
margin: 2em 5em;
|
||||
}
|
||||
|
||||
div.abstract {
|
||||
margin: 2em 5em }
|
||||
|
||||
div.abstract {
|
||||
font-weight: bold ;
|
||||
text-align: center }
|
||||
|
||||
div.dedication {
|
||||
margin: 2em 5em ;
|
||||
text-align: center ;
|
||||
font-style: italic }
|
||||
|
||||
div.dedication {
|
||||
font-weight: bold ;
|
||||
font-style: normal }
|
||||
|
||||
|
||||
span.classifier {
|
||||
font-style: oblique }
|
||||
|
||||
span.classifier-delimiter {
|
||||
font-weight: bold }
|
||||
|
||||
span.problematic {
|
||||
color: red }
|
||||
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,82 @@
|
|||
/* Pygments stylesheet generated by Alectryon (style=None) */
|
||||
/* Most of the following are unused as of now */
|
||||
td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
|
||||
span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; }
|
||||
td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
|
||||
span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; }
|
||||
.highlight .hll, .code .hll { background-color: #ffffcc }
|
||||
.highlight .c, .code .c { color: #555753; font-style: italic } /* Comment */
|
||||
.highlight .err, .code .err { color: #a40000; border: 1px solid #cc0000 } /* Error */
|
||||
.highlight .g, .code .g { color: #000000 } /* Generic */
|
||||
.highlight .k, .code .k { color: #8f5902 } /* Keyword */
|
||||
.highlight .l, .code .l { color: #2e3436 } /* Literal */
|
||||
.highlight .n, .code .n { color: #000000 } /* Name */
|
||||
.highlight .o, .code .o { color: #000000 } /* Operator */
|
||||
.highlight .x, .code .x { color: #2e3436 } /* Other */
|
||||
.highlight .p, .code .p { color: #000000 } /* Punctuation */
|
||||
.highlight .ch, .code .ch { color: #555753; font-weight: bold; font-style: italic } /* Comment.Hashbang */
|
||||
.highlight .cm, .code .cm { color: #555753; font-style: italic } /* Comment.Multiline */
|
||||
.highlight .cp, .code .cp { color: #3465a4; font-style: italic } /* Comment.Preproc */
|
||||
.highlight .cpf, .code .cpf { color: #555753; font-style: italic } /* Comment.PreprocFile */
|
||||
.highlight .c1, .code .c1 { color: #555753; font-style: italic } /* Comment.Single */
|
||||
.highlight .cs, .code .cs { color: #3465a4; font-weight: bold; font-style: italic } /* Comment.Special */
|
||||
.highlight .gd, .code .gd { color: #a40000 } /* Generic.Deleted */
|
||||
.highlight .ge, .code .ge { color: #000000; font-style: italic } /* Generic.Emph */
|
||||
.highlight .gr, .code .gr { color: #a40000 } /* Generic.Error */
|
||||
.highlight .gh, .code .gh { color: #a40000; font-weight: bold } /* Generic.Heading */
|
||||
.highlight .gi, .code .gi { color: #4e9a06 } /* Generic.Inserted */
|
||||
.highlight .go, .code .go { color: #000000; font-style: italic } /* Generic.Output */
|
||||
.highlight .gp, .code .gp { color: #8f5902 } /* Generic.Prompt */
|
||||
.highlight .gs, .code .gs { color: #000000; font-weight: bold } /* Generic.Strong */
|
||||
.highlight .gu, .code .gu { color: #000000; font-weight: bold } /* Generic.Subheading */
|
||||
.highlight .gt, .code .gt { color: #000000; font-style: italic } /* Generic.Traceback */
|
||||
.highlight .kc, .code .kc { color: #204a87; font-weight: bold } /* Keyword.Constant */
|
||||
.highlight .kd, .code .kd { color: #4e9a06; font-weight: bold } /* Keyword.Declaration */
|
||||
.highlight .kn, .code .kn { color: #4e9a06; font-weight: bold } /* Keyword.Namespace */
|
||||
.highlight .kp, .code .kp { color: #204a87 } /* Keyword.Pseudo */
|
||||
.highlight .kr, .code .kr { color: #8f5902 } /* Keyword.Reserved */
|
||||
.highlight .kt, .code .kt { color: #204a87 } /* Keyword.Type */
|
||||
.highlight .ld, .code .ld { color: #2e3436 } /* Literal.Date */
|
||||
.highlight .m, .code .m { color: #2e3436 } /* Literal.Number */
|
||||
.highlight .s, .code .s { color: #ad7fa8 } /* Literal.String */
|
||||
.highlight .na, .code .na { color: #c4a000 } /* Name.Attribute */
|
||||
.highlight .nb, .code .nb { color: #75507b } /* Name.Builtin */
|
||||
.highlight .nc, .code .nc { color: #204a87 } /* Name.Class */
|
||||
.highlight .no, .code .no { color: #ce5c00 } /* Name.Constant */
|
||||
.highlight .nd, .code .nd { color: #3465a4; font-weight: bold } /* Name.Decorator */
|
||||
.highlight .ni, .code .ni { color: #c4a000; text-decoration: underline } /* Name.Entity */
|
||||
.highlight .ne, .code .ne { color: #cc0000 } /* Name.Exception */
|
||||
.highlight .nf, .code .nf { color: #a40000 } /* Name.Function */
|
||||
.highlight .nl, .code .nl { color: #3465a4; font-weight: bold } /* Name.Label */
|
||||
.highlight .nn, .code .nn { color: #000000 } /* Name.Namespace */
|
||||
.highlight .nx, .code .nx { color: #000000 } /* Name.Other */
|
||||
.highlight .py, .code .py { color: #000000 } /* Name.Property */
|
||||
.highlight .nt, .code .nt { color: #a40000 } /* Name.Tag */
|
||||
.highlight .nv, .code .nv { color: #ce5c00 } /* Name.Variable */
|
||||
.highlight .ow, .code .ow { color: #8f5902 } /* Operator.Word */
|
||||
.highlight .w, .code .w { color: #d3d7cf; text-decoration: underline } /* Text.Whitespace */
|
||||
.highlight .mb, .code .mb { color: #2e3436 } /* Literal.Number.Bin */
|
||||
.highlight .mf, .code .mf { color: #2e3436 } /* Literal.Number.Float */
|
||||
.highlight .mh, .code .mh { color: #2e3436 } /* Literal.Number.Hex */
|
||||
.highlight .mi, .code .mi { color: #2e3436 } /* Literal.Number.Integer */
|
||||
.highlight .mo, .code .mo { color: #2e3436 } /* Literal.Number.Oct */
|
||||
.highlight .sa, .code .sa { color: #ad7fa8 } /* Literal.String.Affix */
|
||||
.highlight .sb, .code .sb { color: #ad7fa8 } /* Literal.String.Backtick */
|
||||
.highlight .sc, .code .sc { color: #ad7fa8; font-weight: bold } /* Literal.String.Char */
|
||||
.highlight .dl, .code .dl { color: #ad7fa8 } /* Literal.String.Delimiter */
|
||||
.highlight .sd, .code .sd { color: #ad7fa8 } /* Literal.String.Doc */
|
||||
.highlight .s2, .code .s2 { color: #ad7fa8 } /* Literal.String.Double */
|
||||
.highlight .se, .code .se { color: #ad7fa8; font-weight: bold } /* Literal.String.Escape */
|
||||
.highlight .sh, .code .sh { color: #ad7fa8; text-decoration: underline } /* Literal.String.Heredoc */
|
||||
.highlight .si, .code .si { color: #ce5c00 } /* Literal.String.Interpol */
|
||||
.highlight .sx, .code .sx { color: #ad7fa8 } /* Literal.String.Other */
|
||||
.highlight .sr, .code .sr { color: #ad7fa8 } /* Literal.String.Regex */
|
||||
.highlight .s1, .code .s1 { color: #ad7fa8 } /* Literal.String.Single */
|
||||
.highlight .ss, .code .ss { color: #8f5902 } /* Literal.String.Symbol */
|
||||
.highlight .bp, .code .bp { color: #5c35cc } /* Name.Builtin.Pseudo */
|
||||
.highlight .fm, .code .fm { color: #a40000 } /* Name.Function.Magic */
|
||||
.highlight .vc, .code .vc { color: #ce5c00 } /* Name.Variable.Class */
|
||||
.highlight .vg, .code .vg { color: #ce5c00; text-decoration: underline } /* Name.Variable.Global */
|
||||
.highlight .vi, .code .vi { color: #ce5c00 } /* Name.Variable.Instance */
|
||||
.highlight .vm, .code .vm { color: #ce5c00 } /* Name.Variable.Magic */
|
||||
.highlight .il, .code .il { color: #2e3436 } /* Literal.Number.Integer.Long */
|
||||
Loading…
Reference in New Issue