From 1f51169609a3a7c448558c3d3eb353fb355c7025 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 18 Jun 2024 12:11:53 +0200 Subject: [PATCH] chore: remove leanink --- DocGen4.lean | 1 - DocGen4/LeanInk.lean | 7 - DocGen4/LeanInk/Output.lean | 216 -------- DocGen4/LeanInk/Process.lean | 57 -- DocGen4/Output.lean | 27 +- DocGen4/Output/Base.lean | 25 - DocGen4/Output/Module.lean | 11 - Main.lean | 7 +- lake-manifest.json | 11 +- lakefile.lean | 9 +- static/alectryon/alectryon.css | 777 ---------------------------- static/alectryon/alectryon.js | 172 ------ static/alectryon/docutils_basic.css | 593 --------------------- static/alectryon/pygments.css | 82 --- 14 files changed, 7 insertions(+), 1988 deletions(-) delete mode 100644 DocGen4/LeanInk.lean delete mode 100644 DocGen4/LeanInk/Output.lean delete mode 100644 DocGen4/LeanInk/Process.lean delete mode 100644 static/alectryon/alectryon.css delete mode 100644 static/alectryon/alectryon.js delete mode 100644 static/alectryon/docutils_basic.css delete mode 100644 static/alectryon/pygments.css diff --git a/DocGen4.lean b/DocGen4.lean index 09a46416..70ad4a31 100644 --- a/DocGen4.lean +++ b/DocGen4.lean @@ -6,4 +6,3 @@ Authors: Henrik Böving import DocGen4.Process import DocGen4.Load import DocGen4.Output -import DocGen4.LeanInk diff --git a/DocGen4/LeanInk.lean b/DocGen4/LeanInk.lean deleted file mode 100644 index c4b326af..00000000 --- a/DocGen4/LeanInk.lean +++ /dev/null @@ -1,7 +0,0 @@ -/- -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 diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean deleted file mode 100644 index 8e7f7033..00000000 --- a/DocGen4/LeanInk/Output.lean +++ /dev/null @@ -1,216 +0,0 @@ -/- -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 Lean.Data.Json -import LeanInk.Annotation.Alectryon - -namespace LeanInk.Annotation.Alectryon - -open DocGen4 Output -open scoped DocGen4.Jsx - -structure AlectryonContext where - counter : Nat - -abbrev AlectryonT := StateT AlectryonContext -abbrev AlectryonM := AlectryonT HtmlM - -def getNextButtonLabel : AlectryonM String := do - let val ← get - let newCounter := val.counter + 1 - set { val with counter := newCounter } - return s!"plain-lean4-lean-chk{val.counter}" - -def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do - pure -
- -
-
-
- - {tyi.name} - : - [← DocGen4.Output.infoFormatToHtml tyi.type.fst] - -
-
-
- -
- -def Token.processSemantic (t : Token) : Html := - match t.semanticType with - | 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 - -- 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 - - [parts] - - -def Contents.toHtml : Contents → AlectryonM Html - | .string value => - pure - - {value} - - | .experimentalTokens values => do - let values ← values.mapM Token.toHtml - pure - - [values] - - -def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do - let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]] - if h.body.snd != "" then - hypParts := hypParts.push - - := - [← infoFormatToHtml h.body.fst] - - hypParts := hypParts.push - - : - [← infoFormatToHtml h.type.fst] - - - pure - - [hypParts] - - -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
- let conclusionHtml ← - match g.conclusion with - | .typed info _ => infoFormatToHtml info - | .untyped str => pure #[Html.text str] - - pure -
-
- [hypotheses] -
- -
{g.name} - -
- [conclusionHtml] -
-
- -def Message.toHtml (m : Message) : AlectryonM Html := do - pure -
- -- TODO: This might have to be done in a fancier way - {m.contents} -
- -def Sentence.toHtml (s : Sentence) : AlectryonM Html := do - let messages ← do - if s.messages.size > 0 then - pure #[ -
- [← s.messages.mapM Message.toHtml] -
- ] - else - pure #[] - - let goals ← - if s.goals.size > 0 then - -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it - pure #[ -
- [← s.goals.mapM Goal.toHtml] -
- ] - else - pure #[] - - let buttonLabel ← getNextButtonLabel - - pure - - - - - [messages] - [goals] - - - -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 := -
- Built with doc-gen4, running Lean4. - Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. - Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. - On Mac, use Cmd instead of Ctrl. -
- - pure - - - - - - - - - , - , - - - - -
- {banner} - 
-            [content]
-
-
- - - -def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List Fragment) := do - let config ← read - annotateFileWithCompounds [] config.inputFileContents as - --- TODO: rework monad mess -def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do - let fs ← annotationsToFragments as - let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 } - return html - -end LeanInk.Annotation.Alectryon diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean deleted file mode 100644 index 3a826f88..00000000 --- a/DocGen4/LeanInk/Process.lean +++ /dev/null @@ -1,57 +0,0 @@ -/- -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 -import LeanInk.Analysis -import LeanInk.Annotation -import DocGen4.LeanInk.Output -import DocGen4.Output.Base - -namespace DocGen4.Process.LeanInk - -open Lean -open DocGen4.Output - -def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do - let some modName ← getCurrentName | unreachable! - let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as - let srcDir := moduleNameToDirectory srcBasePath modName - let srcPath := moduleNameToFile srcBasePath modName - IO.FS.createDirAll srcDir - IO.FS.writeFile srcPath srcHtml.toString - return 0 - -def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do - let ctx ← readThe SiteContext - let baseCtx ← readThe SiteBaseContext - let outputFn := (docGenOutput · |>.run ctx baseCtx) - return ← LeanInk.Analysis.runAnalysis { - name := "doc-gen4" - genOutput := outputFn - } - -def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do - execAuxM.run (← readThe SiteContext) (← readThe SiteBaseContext) |>.run config - -@[implemented_by enableInitializersExecution] -private def enableInitializersExecutionWrapper : IO Unit := return () - -def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do - let contents ← IO.FS.readFile sourceFilePath - let config := { - inputFilePath := sourceFilePath - inputFileContents := contents - lakeFile := none - verbose := false - prettifyOutput := true - experimentalTypeInfo := true - experimentalDocString := true - experimentalSemanticType := true - } - enableInitializersExecutionWrapper - if (← execAux config) != 0 then - throw <| IO.userError s!"Analysis for \"{sourceFilePath}\" failed!" - -end DocGen4.Process.LeanInk diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index bb074f29..52c605b2 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -14,7 +14,6 @@ import DocGen4.Output.SourceLinker import DocGen4.Output.Search import DocGen4.Output.ToJson import DocGen4.Output.FoundationalTypes -import DocGen4.LeanInk.Process import Lean.Data.HashMap namespace DocGen4 @@ -66,34 +65,20 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do for (fileName, content) in findStatic do FS.writeFile (findBasePath / fileName) content - let alectryonStatic := #[ - ("alectryon.css", alectryonCss), - ("alectryon.js", alectryonJs), - ("docutils_basic.css", docUtilsCss), - ("pygments.css", pygmentsCss) - ] - - for (fileName, content) in alectryonStatic do - FS.writeFile (srcBasePath / fileName) content - def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do for (_, mod) in result.moduleInfo.toArray do let jsonDecls ← Module.toJson mod FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress -def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (sourceUrl? : Option String) (ink : Bool) : IO Unit := do +def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (sourceUrl? : Option String) : IO Unit := do let config : SiteContext := { result := result, sourceLinker := SourceLinker.sourceLinker sourceUrl? - leanInkEnabled := ink } FS.createDirAll basePath FS.createDirAll declarationsBasePath - let some p := (← IO.getEnv "LEAN_SRC_PATH") | throw <| IO.userError "LEAN_SRC_PATH not found in env" - let sourceSearchPath := System.SearchPath.parse p - discard <| htmlOutputDeclarationDatas result |>.run config baseConfig for (modName, module) in result.moduleInfo.toArray do @@ -108,12 +93,6 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) ( let moduleHtml := moduleToHtml module |>.run config baseConfig FS.createDirAll fileDir FS.writeFile filePath moduleHtml.toString - if ink then - if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then - -- 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 baseConfig := {baseConfig with depthToRoot := modName.components.length } - Process.LeanInk.runInk inputPath |>.run config baseConfig def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do return { @@ -145,9 +124,9 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do The main entrypoint for outputting the documentation HTML based on an `AnalyzerResult`. -/ -def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (sourceUrl? : Option String) (ink : Bool) : IO Unit := do +def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (sourceUrl? : Option String) : IO Unit := do let baseConfig ← getSimpleBaseContext hierarchy - htmlOutputResults baseConfig result sourceUrl? ink + htmlOutputResults baseConfig result sourceUrl? htmlOutputIndex baseConfig end DocGen4 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 5f24f1a7..1ea53c9a 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -46,10 +46,6 @@ 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 : SiteBaseContext) := {ctx with currentName := some name} @@ -85,7 +81,6 @@ def getHierarchy : BaseHtmlM Hierarchy := do return (← read).hierarchy def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName def getResult : HtmlM AnalyzerResult := do return (← read).result def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range -def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled /-- If a template is meant to be extended because it for example only provides the @@ -110,13 +105,6 @@ Returns the HTML doc-gen4 link to a module name. def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do return {module.toString} -/-- -Returns the LeanInk link to a module name. --/ -def moduleNameToInkLink (n : Name) : BaseHtmlM String := do - let parts := "src" :: n.components.map Name.toString - return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" - /-- Returns the path to the HTML file that contains information about a module. -/ @@ -150,10 +138,6 @@ are used in documentation generation, notably JS and CSS ones. 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 /-- @@ -170,14 +154,6 @@ Returns the HTML doc-gen4 link to a declaration name. def declNameToHtmlLink (name : Name) : HtmlM Html := do return {name.toString} -/-- -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 |>.toNat]! - return (← moduleNameToInkLink module) ++ "#" ++ name.toString - /-- Returns a name splitted into parts. Together with "break_within" CSS class this helps browser to break a name @@ -264,7 +240,6 @@ def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do , , , - , , , diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index f0ff9289..1da970e5 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -114,23 +114,12 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do #[Html.element "div" false #[("class", "attributes")] #[attrStr]] else #[] - let leanInkHtml ← do - if ← leanInkEnabled? then - pure #[ -
- ink -
- ] - else - pure #[] - pure
source
- [leanInkHtml] [attrsHtml] {← docInfoHeader doc} [docStringHtml] diff --git a/Main.lean b/Main.lean index 73d6a590..83eeadcc 100644 --- a/Main.lean +++ b/Main.lean @@ -15,7 +15,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do let sourceUri := p.positionalArg! "sourceUri" |>.as! String let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules let baseConfig ← getSimpleBaseContext hierarchy - htmlOutputResults baseConfig doc (some sourceUri) (p.hasFlag "ink") + htmlOutputResults baseConfig doc (some sourceUri) return 0 def runIndexCmd (_p : Parsed) : IO UInt32 := do @@ -27,7 +27,7 @@ def runIndexCmd (_p : Parsed) : IO UInt32 := do def runGenCoreCmd (_p : Parsed) : IO UInt32 := do let (doc, hierarchy) ← loadCore let baseConfig ← getSimpleBaseContext hierarchy - htmlOutputResults baseConfig doc none (ink := False) + htmlOutputResults baseConfig doc none return 0 def runDocGenCmd (_p : Parsed) : IO UInt32 := do @@ -39,9 +39,6 @@ def singleCmd := `[Cli| single VIA runSingleCmd; "Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated." - FLAGS: - ink; "Render the files with LeanInk in addition" - ARGS: module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules." sourceUri : String; "The sourceUri as computed by the Lake facet" diff --git a/lake-manifest.json b/lake-manifest.json index 4f478e95..68179f38 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -13,7 +13,7 @@ {"url": "https://github.com/fgdorais/lean4-unicode-basic", "type": "git", "subDir": null, - "rev": "ef8b0ae5d48e7d5f5d538bf8d66f6cdc7daba296", + "rev": "87791b59c53be80a9a000eb2bcbf61f60a27b334", "name": "UnicodeBasic", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -27,15 +27,6 @@ "manifestFile": "lake-manifest.json", "inputRev": "nightly", "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/hargonix/LeanInk", - "type": "git", - "subDir": null, - "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f", - "name": "leanInk", - "manifestFile": "lake-manifest.json", - "inputRev": "doc-gen", - "inherited": false, "configFile": "lakefile.lean"}], "name": "«doc-gen4»", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 394f65a5..5b7c669b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -20,9 +20,6 @@ require «UnicodeBasic» from git require Cli from git "https://github.com/mhuisi/lean4-cli" @ "nightly" -require leanInk from git - "https://github.com/hargonix/LeanInk" @ "doc-gen" - /-- Obtain the Github URL of a project by parsing the origin remote. -/ @@ -184,11 +181,7 @@ library_facet docs (lib) : FilePath := do basePath / "navbar.html", basePath / "search.html", basePath / "find" / "index.html", - basePath / "find" / "find.js", - basePath / "src" / "alectryon.css", - basePath / "src" / "alectryon.js", - basePath / "src" / "docutils_basic.css", - basePath / "src" / "pygments.css" + basePath / "find" / "find.js" ] coreJob.bindAsync fun _ coreInputTrace => do exeJob.bindAsync fun exeFile exeTrace => do diff --git a/static/alectryon/alectryon.css b/static/alectryon/alectryon.css deleted file mode 100644 index 67988e3d..00000000 --- a/static/alectryon/alectryon.css +++ /dev/null @@ -1,777 +0,0 @@ -@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 and
, 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%; - } -} diff --git a/static/alectryon/alectryon.js b/static/alectryon/alectryon.js deleted file mode 100644 index 6a469d0b..00000000 --- a/static/alectryon/alectryon.js +++ /dev/null @@ -1,172 +0,0 @@ -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; - /* and 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 = {})); diff --git a/static/alectryon/docutils_basic.css b/static/alectryon/docutils_basic.css deleted file mode 100644 index 75d06150..00000000 --- a/static/alectryon/docutils_basic.css +++ /dev/null @@ -1,593 +0,0 @@ -/****************************************************************************** -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 } - - - diff --git a/static/alectryon/pygments.css b/static/alectryon/pygments.css deleted file mode 100644 index d7b92455..00000000 --- a/static/alectryon/pygments.css +++ /dev/null @@ -1,82 +0,0 @@ -/* 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 */