From 9864ffd7a0253c22f2fead1c48b1417b2506ee7b Mon Sep 17 00:00:00 2001
From: Joshua Potter
Date: Thu, 14 Dec 2023 14:09:09 -0700
Subject: [PATCH] Remove embedded doc-gen4.
---
DocGen4.lean | 9 -
DocGen4/LeanInk.lean | 7 -
DocGen4/LeanInk/Output.lean | 215 -------
DocGen4/LeanInk/Process.lean | 57 --
DocGen4/Load.lean | 47 --
DocGen4/Output.lean | 152 -----
DocGen4/Output/Base.lean | 285 ---------
DocGen4/Output/Class.lean | 22 -
DocGen4/Output/ClassInductive.lean | 14 -
DocGen4/Output/Definition.lean | 51 --
DocGen4/Output/DocString.lean | 220 -------
DocGen4/Output/Find.lean | 22 -
DocGen4/Output/FoundationalTypes.lean | 51 --
DocGen4/Output/Index.lean | 84 ---
DocGen4/Output/Inductive.lean | 39 --
DocGen4/Output/Instance.lean | 8 -
DocGen4/Output/Module.lean | 219 -------
DocGen4/Output/Navbar.lean | 111 ----
DocGen4/Output/NotFound.lean | 26 -
DocGen4/Output/Search.lean | 48 --
DocGen4/Output/SourceLinker.lean | 37 --
DocGen4/Output/Structure.lean | 51 --
DocGen4/Output/Template.lean | 72 ---
DocGen4/Output/ToHtmlFormat.lean | 149 -----
DocGen4/Output/ToJson.lean | 151 -----
DocGen4/Process.lean | 21 -
DocGen4/Process/Analyze.lean | 163 -----
DocGen4/Process/Attributes.lean | 182 ------
DocGen4/Process/AxiomInfo.lean | 22 -
DocGen4/Process/Base.lean | 198 -------
DocGen4/Process/ClassInfo.lean | 24 -
DocGen4/Process/DefinitionInfo.lean | 74 ---
DocGen4/Process/DocInfo.lean | 223 -------
DocGen4/Process/Hierarchy.lean | 138 -----
DocGen4/Process/InductiveInfo.lean | 30 -
DocGen4/Process/InstanceInfo.lean | 45 --
DocGen4/Process/NameExt.lean | 48 --
DocGen4/Process/NameInfo.lean | 56 --
DocGen4/Process/OpaqueInfo.lean | 33 --
DocGen4/Process/StructureInfo.lean | 58 --
DocGen4/Process/TheoremInfo.lean | 19 -
Makefile | 14 -
README.md | 21 -
lake-manifest.json | 83 +--
lakefile.lean | 221 +------
scripts/run_pdflatex.sh | 26 -
static/alectryon/alectryon.css | 777 ------------------------
static/alectryon/alectryon.js | 172 ------
static/alectryon/docutils_basic.css | 593 ------------------
static/alectryon/pygments.css | 82 ---
static/color-scheme.js | 33 --
static/declaration-data.js | 272 ---------
static/expand-nav.js | 24 -
static/find/find.js | 94 ---
static/how-about.js | 39 --
static/importedBy.js | 19 -
static/instances.js | 41 --
static/jump-src.js | 10 -
static/mathjax-config.js | 41 --
static/nav.js | 43 --
static/search.js | 164 -----
static/site-root.js | 4 -
static/style.css | 825 --------------------------
static/tactic.js | 61 --
64 files changed, 49 insertions(+), 7091 deletions(-)
delete mode 100644 DocGen4.lean
delete mode 100644 DocGen4/LeanInk.lean
delete mode 100644 DocGen4/LeanInk/Output.lean
delete mode 100644 DocGen4/LeanInk/Process.lean
delete mode 100644 DocGen4/Load.lean
delete mode 100644 DocGen4/Output.lean
delete mode 100644 DocGen4/Output/Base.lean
delete mode 100644 DocGen4/Output/Class.lean
delete mode 100644 DocGen4/Output/ClassInductive.lean
delete mode 100644 DocGen4/Output/Definition.lean
delete mode 100644 DocGen4/Output/DocString.lean
delete mode 100644 DocGen4/Output/Find.lean
delete mode 100644 DocGen4/Output/FoundationalTypes.lean
delete mode 100644 DocGen4/Output/Index.lean
delete mode 100644 DocGen4/Output/Inductive.lean
delete mode 100644 DocGen4/Output/Instance.lean
delete mode 100644 DocGen4/Output/Module.lean
delete mode 100644 DocGen4/Output/Navbar.lean
delete mode 100644 DocGen4/Output/NotFound.lean
delete mode 100644 DocGen4/Output/Search.lean
delete mode 100644 DocGen4/Output/SourceLinker.lean
delete mode 100644 DocGen4/Output/Structure.lean
delete mode 100644 DocGen4/Output/Template.lean
delete mode 100644 DocGen4/Output/ToHtmlFormat.lean
delete mode 100644 DocGen4/Output/ToJson.lean
delete mode 100644 DocGen4/Process.lean
delete mode 100644 DocGen4/Process/Analyze.lean
delete mode 100644 DocGen4/Process/Attributes.lean
delete mode 100644 DocGen4/Process/AxiomInfo.lean
delete mode 100644 DocGen4/Process/Base.lean
delete mode 100644 DocGen4/Process/ClassInfo.lean
delete mode 100644 DocGen4/Process/DefinitionInfo.lean
delete mode 100644 DocGen4/Process/DocInfo.lean
delete mode 100644 DocGen4/Process/Hierarchy.lean
delete mode 100644 DocGen4/Process/InductiveInfo.lean
delete mode 100644 DocGen4/Process/InstanceInfo.lean
delete mode 100644 DocGen4/Process/NameExt.lean
delete mode 100644 DocGen4/Process/NameInfo.lean
delete mode 100644 DocGen4/Process/OpaqueInfo.lean
delete mode 100644 DocGen4/Process/StructureInfo.lean
delete mode 100644 DocGen4/Process/TheoremInfo.lean
delete mode 100644 Makefile
delete mode 100755 scripts/run_pdflatex.sh
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
delete mode 100644 static/color-scheme.js
delete mode 100644 static/declaration-data.js
delete mode 100644 static/expand-nav.js
delete mode 100644 static/find/find.js
delete mode 100644 static/how-about.js
delete mode 100644 static/importedBy.js
delete mode 100644 static/instances.js
delete mode 100644 static/jump-src.js
delete mode 100644 static/mathjax-config.js
delete mode 100644 static/nav.js
delete mode 100644 static/search.js
delete mode 100644 static/site-root.js
delete mode 100644 static/style.css
delete mode 100644 static/tactic.js
diff --git a/DocGen4.lean b/DocGen4.lean
deleted file mode 100644
index 09a4641..0000000
--- a/DocGen4.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-/-
-Copyright (c) 2021 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-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 c4b326a..0000000
--- 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 ae23832..0000000
--- a/DocGen4/LeanInk/Output.lean
+++ /dev/null
@@ -1,215 +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 :=
- if s.messages.size > 0 then
- #[
-
- [← s.messages.mapM Message.toHtml]
-
- ]
- else
- #[]
-
- let goals :=
- if s.goals.size > 0 then
- -- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
- #[
-
- [← s.goals.mapM Goal.toHtml]
-
- ]
- else
- #[]
-
- let buttonLabel ← getNextButtonLabel
-
- pure
-
-
-
- {← s.contents.toHtml}
-
-
- [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 3a826f8..0000000
--- 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/Load.lean b/DocGen4/Load.lean
deleted file mode 100644
index 7a6dec3..0000000
--- a/DocGen4/Load.lean
+++ /dev/null
@@ -1,47 +0,0 @@
-/-
-Copyright (c) 2021 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 DocGen4.Process
-import Lean.Data.HashMap
-
-namespace DocGen4
-
-open Lean System IO
-
-def envOfImports (imports : Array Name) : IO Environment := do
- importModules (imports.map (Import.mk · false)) Options.empty
-
-def loadInit (imports : Array Name) : IO Hierarchy := do
- let env ← envOfImports imports
- pure <| Hierarchy.fromArray env.header.moduleNames
-
-/--
-Load a list of modules from the current Lean search path into an `Environment`
-to process for documentation.
--/
-def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do
- initSearchPath (← findSysroot)
- let env ← envOfImports task.getLoad
- let config := {
- -- TODO: parameterize maxHeartbeats
- maxHeartbeats := 100000000,
- options := ⟨[
- (`pp.tagAppFns, true),
- (`pp.funBinderTypes, true)
- ]⟩,
- -- TODO: Figure out whether this could cause some bugs
- fileName := default,
- fileMap := default,
- catchRuntimeEx := true,
- }
-
- Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
-
-def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
- load <| .loadAll #[`Init, `Lean, `Lake]
-
-end DocGen4
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
deleted file mode 100644
index 41fd7fb..0000000
--- a/DocGen4/Output.lean
+++ /dev/null
@@ -1,152 +0,0 @@
-/-
-Copyright (c) 2021 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 DocGen4.Process
-import DocGen4.Output.Base
-import DocGen4.Output.Index
-import DocGen4.Output.Module
-import DocGen4.Output.NotFound
-import DocGen4.Output.Find
-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
-
-open Lean IO System Output Process
-
-def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
- let findBasePath := basePath / "find"
-
- -- Base structure
- FS.createDirAll basePath
- FS.createDirAll findBasePath
- FS.createDirAll srcBasePath
- FS.createDirAll declarationsBasePath
-
- -- All the doc-gen static stuff
- let indexHtml := ReaderT.run index config |>.toString
- let notFoundHtml := ReaderT.run notFound config |>.toString
- let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
- let navbarHtml := ReaderT.run navbar config |>.toString
- let searchHtml := ReaderT.run search config |>.toString
- let docGenStatic := #[
- ("style.css", styleCss),
- ("declaration-data.js", declarationDataCenterJs),
- ("color-scheme.js", colorSchemeJs),
- ("nav.js", navJs),
- ("jump-src.js", jumpSrcJs),
- ("expand-nav.js", expandNavJs),
- ("how-about.js", howAboutJs),
- ("search.html", searchHtml),
- ("search.js", searchJs),
- ("mathjax-config.js", mathjaxConfigJs),
- ("instances.js", instancesJs),
- ("importedBy.js", importedByJs),
- ("index.html", indexHtml),
- ("foundational_types.html", foundationalTypesHtml),
- ("404.html", notFoundHtml),
- ("navbar.html", navbarHtml)
- ]
- for (fileName, content) in docGenStatic do
- FS.writeFile (basePath / fileName) content
-
- let findHtml := ReaderT.run find { config with depthToRoot := 1 } |>.toString
- let findStatic := #[
- ("index.html", findHtml),
- ("find.js", findJs)
- ]
- 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) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
- let config : SiteContext := {
- result := result,
- sourceLinker := ← SourceLinker.sourceLinker gitUrl?
- 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
- 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 baseConfig := { baseConfig with
- depthToRoot := modName.components.dropLast.length
- currentName := some modName
- }
- 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 {
- depthToRoot := 0,
- currentName := none,
- hierarchy
- }
-
-def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
- htmlOutputSetup baseConfig
-
- let mut index : JsonIndex := {}
- let mut headerIndex : JsonHeaderIndex := {}
- for entry in ← System.FilePath.readDir declarationsBasePath do
- if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
- let fileContent ← FS.readFile entry.path
- let .ok jsonContent := Json.parse fileContent | unreachable!
- let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
- index := index.addModule module |>.run baseConfig
- headerIndex := headerIndex.addModule module
-
- let finalJson := toJson index
- let finalHeaderJson := toJson headerIndex
- -- The root JSON for find
- FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
- FS.writeFile (declarationsBasePath / "header-data.bmp") finalHeaderJson.compress
-
-/--
-The main entrypoint for outputting the documentation HTML based on an
-`AnalyzerResult`.
--/
-def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
- let baseConfig ← getSimpleBaseContext hierarchy
- htmlOutputResults baseConfig result gitUrl? ink
- htmlOutputIndex baseConfig
-
-end DocGen4
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
deleted file mode 100644
index 1d2c7e1..0000000
--- a/DocGen4/Output/Base.lean
+++ /dev/null
@@ -1,285 +0,0 @@
-/-
-Copyright (c) 2021 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-import DocGen4.Process
-import DocGen4.Output.ToHtmlFormat
-
-namespace DocGen4.Output
-
-open scoped DocGen4.Jsx
-open Lean System Widget Elab Process
-
-def basePath := FilePath.mk "." / ".lake" / "build" / "doc"
-def srcBasePath := basePath / "src"
-def declarationsBasePath := basePath / "declarations"
-
-/--
-The context used in the `BaseHtmlM` monad for HTML templating.
--/
-structure SiteBaseContext where
-
- /--
- The module hierarchy as a tree structure.
- -/
- hierarchy : Hierarchy
- /--
- How far away we are from the page root, used for relative links to the root.
- -/
- depthToRoot: Nat
- /--
- The name of the current module if there is one, there exist a few
- pages that don't have a module name.
- -/
- currentName : Option Name
-
-/--
-The context used in the `HtmlM` monad for HTML templating.
--/
-structure SiteContext where
- /--
- The full analysis result from the Process module.
- -/
- result : AnalyzerResult
- /--
- 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}
-
-abbrev BaseHtmlT := ReaderT SiteBaseContext
-abbrev BaseHtmlM := BaseHtmlT Id
-
-abbrev HtmlT (m) := ReaderT SiteContext (BaseHtmlT m)
-abbrev HtmlM := HtmlT Id
-
-def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : m α :=
- ReaderT.run x ctx |>.run baseCtx
-
-def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α :=
- ReaderT.run x ctx |>.run baseCtx |>.run
-
-instance [Monad m] : MonadLift HtmlM (HtmlT m) where
- monadLift x := do return x.run (← readThe SiteContext) (← readThe SiteBaseContext)
-
-instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
- monadLift x := do return x.run (← readThe SiteBaseContext)
-
-/--
-Obtains the root URL as a relative one to the current depth.
--/
-def getRoot : BaseHtmlM String := do
- let rec go: Nat -> String
- | 0 => "./"
- | Nat.succ n' => "../" ++ go n'
- let d <- SiteBaseContext.depthToRoot <$> read
- return (go d)
-
-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
-header but no real content this is the way to fill the template with content.
-This is untyped so HtmlM and BaseHtmlM can be mixed.
--/
-def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m β :=
- new >>= base
-
-def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β :=
- new >>= (monadLift ∘ base)
-
-/-
-Returns the doc-gen4 link to a module `NameExt`.
--/
-def moduleNameExtToLink (n : NameExt) : BaseHtmlM String := do
- let parts := n.name.components.map Name.toString
- return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ "." ++ n.ext.toString
-
-/--
-Returns the doc-gen4 link to a module name.
--/
-def moduleNameToLink (n : Name) : BaseHtmlM String := do
- let parts := n.components.map Name.toString
- return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
-
-/--
-Returns the doc-gen4 link to a module name.
--/
-def moduleNameToHtmlLink (n : Name) : BaseHtmlM String :=
- moduleNameExtToLink ⟨n, .html⟩
-
-/--
-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.
--/
-def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
- let parts := n.components.map Name.toString
- FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
-
-/--
-Returns the directory of the HTML file that contains information about a module.
--/
-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
-are used in documentation generation, notably JS and CSS ones.
--/
- def styleCss : String := include_str "../../static/style.css"
- def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
- def colorSchemeJs : String := include_str "../../static/color-scheme.js"
- def jumpSrcJs : String := include_str "../../static/jump-src.js"
- def navJs : String := include_str "../../static/nav.js"
- def expandNavJs : String := include_str "../../static/expand-nav.js"
- def howAboutJs : String := include_str "../../static/how-about.js"
- def searchJs : String := include_str "../../static/search.js"
- def instancesJs : String := include_str "../../static/instances.js"
- def importedByJs : String := include_str "../../static/importedBy.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
-
-/--
-Returns the doc-gen4 link to a declaration name.
--/
-def declNameToLink (name : Name) : HtmlM String := do
- let res ← getResult
- let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
- return (← moduleNameToHtmlLink module) ++ "#" ++ name.toString
-
-/--
-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
-nicely.
--/
-def breakWithin (name: String) : (Array Html) :=
- name.splitOn "."
- |> .map (fun (s: String) => {s} )
- |> .intersperse "."
- |> List.toArray
-
-/--
-Returns the HTML doc-gen4 link to a declaration name with "break_within"
-set as class.
--/
-def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
- return
- [breakWithin name.toString]
-
-
-/--
-In Lean syntax declarations the following pattern is quite common:
-```
-syntax term " + " term : term
-```
-that is, we place spaces around the operator in the middle. When the
-`InfoTree` framework provides us with information about what source token
-corresponds to which identifier it will thus say that `" + "` corresponds to
-`HAdd.hadd`. This is however not the way we want this to be linked, in the HTML
-only `+` should be linked, taking care of this is what this function is
-responsible for.
--/
-def splitWhitespaces (s : String) : (String × String × String) := Id.run do
- let front := "".pushn ' ' <| s.offsetOfPos (s.find (!Char.isWhitespace ·))
- let mut s := s.trimLeft
- let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
- s := s.trimRight
- (front, s, back)
-
-/--
-Turns a `CodeWithInfos` object, that is basically a Lean syntax tree with
-information about what the identifiers mean, into an HTML object that links
-to as much information as possible.
--/
-partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
- match i with
- | .text t => return #[Html.escape t]
- | .append tt => tt.foldlM (fun acc t => do return acc ++ (← infoFormatToHtml t)) #[]
- | .tag a t =>
- match a.info.val.info with
- | Info.ofTermInfo i =>
- let cleanExpr := i.expr.consumeMData
- match cleanExpr with
- | .const name _ =>
- -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
- -- find a better solution
- if (← getResult).name2ModIdx.contains name then
- match t with
- | .text t =>
- let (front, t, back) := splitWhitespaces <| Html.escape t
- let elem := {t}
- return #[Html.text front, elem, Html.text back]
- | _ =>
- return #[[← infoFormatToHtml t] ]
- else
- return #[[← infoFormatToHtml t] ]
- | .sort _ =>
- match t with
- | .text t =>
- let sortPrefix :: rest := t.splitOn " " | unreachable!
- let sortLink := {sortPrefix}
- let mut restStr := String.intercalate " " rest
- if restStr.length != 0 then
- restStr := " " ++ restStr
- return #[sortLink, Html.text restStr]
- | _ =>
- return #[[← infoFormatToHtml t] ]
- | _ =>
- return #[[← infoFormatToHtml t] ]
- | _ => return #[[← infoFormatToHtml t] ]
-
-def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
- return #[
- ,
- ,
- ,
- ,
- ,
-
- ]
-
-end DocGen4.Output
diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean
deleted file mode 100644
index 521afc3..0000000
--- a/DocGen4/Output/Class.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-import DocGen4.Output.Template
-import DocGen4.Output.Structure
-import DocGen4.Process
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-open Lean
-
-def classInstancesToHtml (className : Name) : HtmlM Html := do
- pure
-
- Instances
-
-
-
-def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do
- structureToHtml i
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/ClassInductive.lean b/DocGen4/Output/ClassInductive.lean
deleted file mode 100644
index 746b005..0000000
--- a/DocGen4/Output/ClassInductive.lean
+++ /dev/null
@@ -1,14 +0,0 @@
-import DocGen4.Output.Template
-import DocGen4.Output.Class
-import DocGen4.Output.Inductive
-import DocGen4.Process
-
-
-namespace DocGen4
-namespace Output
-
-def classInductiveToHtml (i : Process.ClassInductiveInfo) : HtmlM (Array Html) := do
- inductiveToHtml i
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
deleted file mode 100644
index c468ceb..0000000
--- a/DocGen4/Output/Definition.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-import DocGen4.Output.Template
-import DocGen4.Output.DocString
-import DocGen4.Process
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-open Lean Widget
-
-/-- This is basically an arbitrary number that seems to work okay. -/
-def equationLimit : Nat := 200
-
-def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
- return [← infoFormatToHtml c]
-
-/--
-Attempt to render all `simp` equations for this definition. At a size
-defined in `equationLimit` we stop trying since they:
-- are too ugly to read most of the time
-- take too long
--/
-def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do
- if let some eqs := i.equations then
- let equationsHtml ← eqs.mapM equationToHtml
- let filteredEquationsHtml := equationsHtml.filter (·.textLength < equationLimit)
- if equationsHtml.size ≠ filteredEquationsHtml.size then
- return #[
-
- Equations
-
- One or more equations did not get rendered due to their size.
- [filteredEquationsHtml]
-
-
- ]
- else
- return #[
-
- Equations
-
- [filteredEquationsHtml]
-
-
- ]
- else
- return #[]
-
-end Output
-end DocGen4
-
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
deleted file mode 100644
index ca4cdb9..0000000
--- a/DocGen4/Output/DocString.lean
+++ /dev/null
@@ -1,220 +0,0 @@
-import CMark
-import DocGen4.Output.Template
-import Lean.Data.Parsec
-import UnicodeBasic
-
-open Lean Xml Parser Parsec DocGen4.Process
-
-namespace DocGen4
-namespace Output
-
-/-- Auxiliary function for `splitAround`. -/
-@[specialize] partial def splitAroundAux (s : String) (p : Char → Bool) (b i : String.Pos) (r : List String) : List String :=
- if s.atEnd i then
- let r := (s.extract b i)::r
- r.reverse
- else
- let c := s.get i
- if p c then
- let i := s.next i
- splitAroundAux s p i i (c.toString::s.extract b (i-⟨1⟩)::r)
- else
- splitAroundAux s p b (s.next i) r
-
-/--
- Similar to `String.split` in Lean core, but keeps the separater.
- e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]`
--/
-def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
-
-instance : Inhabited Element := ⟨"", Lean.RBMap.empty, #[]⟩
-
-/-- Parse an array of Xml/Html document from String. -/
-def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
-
-/--
- Generate id for heading elements, with the following rules:
-
- 1. Characters in `letter`, `mark`, `number` and `symbol` unicode categories are preserved.
- 2. Any sequences of Characters in `punctuation`, `separator` and `other` categories are replaced by a single dash.
- 3. Cases (upper and lower) are preserved.
- 4. Xml/Html tags are ignored.
--/
-partial def xmlGetHeadingId (el : Xml.Element) : String :=
- elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
- where
- elementToPlainText el := match el with
- | (Element.Element _ _ contents) =>
- "".intercalate (contents.toList.map contentToPlainText)
- contentToPlainText c := match c with
- | Content.Element el => elementToPlainText el
- | Content.Comment _ => ""
- | Content.Character s => s
- replaceCharSeq pattern replacement s :=
- s.split pattern
- |>.filter (!·.isEmpty)
- |> replacement.intercalate
- unicodeToDrop (c : Char) : Bool :=
- let cats := [
- Unicode.GeneralCategory.P, -- punctuation
- Unicode.GeneralCategory.Z, -- separator
- Unicode.GeneralCategory.C -- other
- ]
- cats.any (Unicode.isInGeneralCategory c)
-
-/--
- This function try to find the given name, both globally and in current module.
-
- For global search, a precise name is need. If the global search fails, the function
- tries to find a local one that ends with the given search name.
--/
-def nameToLink? (s : String) : HtmlM (Option String) := do
- let res ← getResult
- if s.endsWith ".lean" && s.contains '/' then
- return (← getRoot) ++ s.dropRight 5 ++ ".html"
- else if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
- -- with exactly the same name
- if res.name2ModIdx.contains name then
- declNameToLink name
- -- module name
- else if res.moduleNames.contains name then
- moduleNameToHtmlLink name
- -- find similar name in the same module
- else
- match (← getCurrentName) with
- | some currentName =>
- match res.moduleInfo.find! currentName |>.members |> filterDocInfo |>.find? (sameEnd ·.getName name) with
- | some info =>
- declNameToLink info.getName
- | _ => return none
- | _ => return none
- else
- return none
- where
- -- check if two names have the same ending components
- sameEnd n1 n2 :=
- List.zip n1.componentsRev n2.componentsRev
- |>.all fun ⟨a, b⟩ => a == b
-
-/--
- Extend links with following rules:
-
- 1. if the link starts with `##`, a name search is used and will panic if not found
- 2. if the link starts with `#`, it's treated as id link, no modification
- 3. if the link starts with `http`, it's an absolute one, no modification
- 4. otherwise it's a relative link, extend it with base url
--/
-def extendLink (s : String) : HtmlM String := do
- -- for intra doc links
- if s.startsWith "##" then
- if let some link ← nameToLink? (s.drop 2) then
- return link
- else
- panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
- -- for id
- else if s.startsWith "#" then
- return s
- -- for absolute and relative urls
- else if s.startsWith "http" then
- return s
- else return ((← getRoot) ++ s)
-
-/-- Add attributes for heading. -/
-def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do
- match el with
- | Element.Element name attrs contents => do
- let id := xmlGetHeadingId el
- let anchorAttributes := Lean.RBMap.empty
- |>.insert "class" "hover-link"
- |>.insert "href" s!"#{id}"
- let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
- let newAttrs := attrs
- |>.insert "id" id
- |>.insert "class" "markdown-heading"
- let newContents := (←
- contents.mapM (fun c => match c with
- | Content.Element e => return Content.Element (← modifyElement e)
- | _ => pure c))
- |>.push (Content.Character " ")
- |>.push (Content.Element anchor)
- return ⟨ name, newAttrs, newContents⟩
-
-/-- Extend anchor links. -/
-def extendAnchor (el : Element) : HtmlM Element := do
- match el with
- | Element.Element name attrs contents =>
- let newAttrs ← match attrs.find? "href" with
- | some href => pure (attrs.insert "href" (← extendLink href))
- | none => pure attrs
- return ⟨ name, newAttrs, contents⟩
-
-/-- Automatically add intra documentation link for inline code span. -/
-def autoLink (el : Element) : HtmlM Element := do
- match el with
- | Element.Element name attrs contents =>
- let mut newContents := #[]
- for c in contents do
- match c with
- | Content.Character s =>
- newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join
- | _ => newContents := newContents.push c
- return ⟨ name, attrs, newContents ⟩
- where
- linkify s := do
- let link? ← nameToLink? s
- match link? with
- | some link =>
- let attributes := Lean.RBMap.empty.insert "href" link
- return [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
- | none =>
- let sHead := s.dropRightWhile (· != '.')
- let sTail := s.takeRightWhile (· != '.')
- let link'? ← nameToLink? sTail
- match link'? with
- | some link' =>
- let attributes := Lean.RBMap.empty.insert "href" link'
- return [
- Content.Character sHead,
- Content.Element <| Element.Element "a" attributes #[Content.Character sTail]
- ]
- | none =>
- return [Content.Character s]
- unicodeToSplit (c : Char) : Bool :=
- let cats := [
- Unicode.GeneralCategory.Z, -- separator
- Unicode.GeneralCategory.C -- other
- ]
- cats.any (Unicode.isInGeneralCategory c)
-
-/-- Core function of modifying the cmark rendered docstring html. -/
-partial def modifyElement (element : Element) : HtmlM Element :=
- match element with
- | el@(Element.Element name attrs contents) => do
- -- add id and class to
- if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then
- addHeadingAttributes el modifyElement
- -- extend relative href for
- else if name = "a" then
- extendAnchor el
- -- auto link for inline
- else if name = "code" ∧
- -- don't linkify code blocks explicitly tagged with a language other than lean
- (((attrs.find? "class").getD "").splitOn.all (fun s => s == "language-lean" || !s.startsWith "language-")) then
- autoLink el
- -- recursively modify
- else
- let newContents ← contents.mapM fun c => match c with
- | Content.Element e => return Content.Element (← modifyElement e)
- | _ => pure c
- return ⟨ name, attrs, newContents ⟩
-
-/-- Convert docstring to Html. -/
-def docStringToHtml (s : String) : HtmlM (Array Html) := do
- let rendered := CMark.renderHtml (Html.escape s)
- match manyDocument rendered.mkIterator with
- | Parsec.ParseResult.success _ res =>
- res.mapM fun x => do return Html.text <| toString (← modifyElement x)
- | _ => return #[Html.text rendered]
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean
deleted file mode 100644
index aa81f15..0000000
--- a/DocGen4/Output/Find.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-import DocGen4.Output.Template
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-open Lean
-
-def find : BaseHtmlM Html := do
- pure
-
-
-
-
-
-
-
-
-
-end Output
-end DocGen4
-
diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean
deleted file mode 100644
index 2297570..0000000
--- a/DocGen4/Output/FoundationalTypes.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-import DocGen4.Output.Template
-import DocGen4.Output.Inductive
-
-namespace DocGen4.Output
-
-open scoped DocGen4.Jsx
-
-def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundational Types") do
- pure <|
-
-
- Foundational Types
-
- Some of Lean's types are not defined in any Lean source files (even the prelude
) since they come from its foundational type theory. This page provides basic documentation for these types.
- For a more in-depth explanation of Lean's type theory, refer to
- TPiL .
-
-
- Sort u
- Sort u
is the type of types in Lean, and Sort u : Sort (u + 1)
.
- {← instancesForToHtml `_builtin_sortu}
-
- Type u
- Type u
is notation for Sort (u + 1)
.
- {← instancesForToHtml `_builtin_typeu}
-
- Prop
- Prop
is notation for Sort 0
.
- {← instancesForToHtml `_builtin_prop}
-
- Pi types, {"(a : α) → β a"}
- The type of dependent functions is known as a pi type.
- Non-dependent functions and implications are a special case.
- Note that these can also be written with the alternative notations:
-
- ∀ a : α, β a
, conventionally used where β a : Prop
.
- (a : α) → β a
- α → γ
, possible only if β a = γ
for all a
.
-
- Lean also permits ASCII-only spellings of the three variants:
-
- forall a : A, B a
for {"∀ a : α, β a"}
- (a : A) -> B a
, for (a : α) → β a
- A -> B
, for α → β
-
- Note that despite not itself being a function, (→)
is available as infix notation for
- {"fun α β, α → β"}
.
- -- TODO: instances for pi types
-
-
-end DocGen4.Output
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
deleted file mode 100644
index f12b0fa..0000000
--- a/DocGen4/Output/Index.lean
+++ /dev/null
@@ -1,84 +0,0 @@
-/-
-Copyright (c) 2021 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-import DocGen4.Output.ToHtmlFormat
-import DocGen4.Output.Template
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-
-def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
- pure <|
-
-
- Bookshelf
-
- A study of the books listed below. Most proofs are conducted in LaTeX.
- Where feasible, theorems are also formally proven in
- Lean .
-
-
- In Progress
-
- Apostol, Tom M. Calculus, Vol. 1: One-Variable Calculus, with an Introduction to Linear Algebra. 2nd ed. Vol. 1. 2 vols. Wiley, 1991.
- Enderton, Herbert B. A Mathematical Introduction to Logic. 2nd ed. San Diego: Harcourt/Academic Press, 2001.
- Enderton, Herbert B. Elements of Set Theory. New York: Academic Press, 1977.
- Fraleigh, John B. A First Course in Abstract Algebra, n.d.
-
-
- Complete
-
-
- Pending
-
- Axler, Sheldon. Linear Algebra Done Right. Undergraduate Texts in Mathematics. Cham: Springer International Publishing, 2015.
- Cormen, Thomas H., Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms. 3rd ed. Cambridge, Mass: MIT Press, 2009.
- Gries, David. The Science of Programming. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
- Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.
- Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.
- Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.
-
-
- Legend
-
- A color/symbol code is used on generated PDF headers to indicate their
- status:
-
-
- Dark gray statements are
- reserved for definitions and axioms that have been encoded in LaTeX.
- A reference to a definition in Lean may also be provided.
-
-
- Teal statements are reserved for
- statements, theorems, lemmas, etc. that have been proven in LaTeX
- and have a corresponding proof in Lean.
-
-
- Olive statements are reserved for
- statements, theorems, lemmas, etc. that have been proven in LaTeX.
- A reference to a statement in Lean may also be provided.
-
-
- Fuchsia statements are reserved
- for statements, theorems, lemmas, etc. that have been proven in
- LaTeX and will have a corresponding proof in Lean.
-
-
- Maroon serves as a catch-all for
- statements that don't fit the above categorizations. Incomplete
- definitions, statements without proof, etc. belong here.
-
-
-
- This was built using Lean 4 at commit {Lean.githash}
-
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
deleted file mode 100644
index 3d6eaf3..0000000
--- a/DocGen4/Output/Inductive.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import DocGen4.Output.Template
-import DocGen4.Output.DocString
-import DocGen4.Process
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-open Lean
-
-def instancesForToHtml (typeName : Name) : BaseHtmlM Html := do
- pure
-
- Instances For
-
-
-
-def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
- let shortName := c.name.componentsRev.head!.toString
- let name := c.name.toString
- if let some doc := c.doc then
- let renderedDoc ← docStringToHtml doc
- pure
-
- {shortName} : [← infoFormatToHtml c.type]
- [renderedDoc]
-
- else
- pure
-
- {shortName} : [← infoFormatToHtml c.type]
-
-
-def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
- let constructorsHtml := [← i.ctors.toArray.mapM ctorToHtml]
- return #[constructorsHtml]
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/Instance.lean b/DocGen4/Output/Instance.lean
deleted file mode 100644
index 78f098d..0000000
--- a/DocGen4/Output/Instance.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import DocGen4.Output.Template
-import DocGen4.Output.Definition
-
-namespace DocGen4
-namespace Output
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
deleted file mode 100644
index df6ac05..0000000
--- a/DocGen4/Output/Module.lean
+++ /dev/null
@@ -1,219 +0,0 @@
-/-
-Copyright (c) 2021 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-import DocGen4.Output.Template
-import DocGen4.Output.Inductive
-import DocGen4.Output.Structure
-import DocGen4.Output.Class
-import DocGen4.Output.Definition
-import DocGen4.Output.Instance
-import DocGen4.Output.ClassInductive
-import DocGen4.Output.DocString
-import DocGen4.Process
-import Lean.Data.Xml.Parser
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-open Lean Process
-
-/--
-Render an `Arg` as HTML, adding opacity effects etc. depending on what
-type of binder it has.
--/
-def argToHtml (arg : Arg) : HtmlM Html := do
- let (l, r, implicit) := match arg.binderInfo with
- | BinderInfo.default => ("(", ")", false)
- | BinderInfo.implicit => ("{", "}", true)
- | BinderInfo.strictImplicit => ("⦃", "⦄", true)
- | BinderInfo.instImplicit => ("[", "]", true)
- let mut nodes :=
- match arg.name with
- | some name => #[Html.text s!"{l}{name.toString} : "]
- | none => #[Html.text s!"{l}"]
- nodes := nodes.append (← infoFormatToHtml arg.type)
- nodes := nodes.push r
- let inner := [nodes]
- let html := Html.element "span" false #[("class", "decl_args")] #[inner]
- if implicit then
- return {html}
- else
- return html
-
-/--
-Render the structures this structure extends from as HTML so it can be
-added to the top level.
--/
-def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do
- let mut nodes := #[]
- if s.parents.size > 0 then
- nodes := nodes.push extends
- let mut parents := #[]
- for parent in s.parents do
- let link ← declNameToHtmlBreakWithinLink parent
- let inner := {link}
- let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
- parents := parents.push html
- nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
- return nodes
-
-/--
-Render the general header of a declaration containing its declaration type
-and name.
--/
-def docInfoHeader (doc : DocInfo) : HtmlM Html := do
- let mut nodes := #[]
- nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription]
- nodes := nodes.push
-
- {← declNameToHtmlBreakWithinLink doc.getName}
-
- for arg in doc.getArgs do
- nodes := nodes.push (← argToHtml arg)
-
- match doc with
- | DocInfo.structureInfo i => nodes := nodes.append (← structureInfoHeader i)
- | DocInfo.classInfo i => nodes := nodes.append (← structureInfoHeader i)
- | _ => nodes := nodes
-
- nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"]
- nodes := nodes.push [← infoFormatToHtml doc.getType]
- return
-
-/--
-The main entry point for rendering a single declaration inside a given module.
--/
-def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
- -- basic info like headers, types, structure fields, etc.
- let docInfoHtml ← match doc with
- | DocInfo.inductiveInfo i => inductiveToHtml i
- | DocInfo.structureInfo i => structureToHtml i
- | DocInfo.classInfo i => classToHtml i
- | DocInfo.classInductiveInfo i => classInductiveToHtml i
- | _ => pure #[]
- -- rendered doc stirng
- let docStringHtml ← match doc.getDocString with
- | some s => docStringToHtml s
- | none => pure #[]
- -- extra information like equations and instances
- let extraInfoHtml ← match doc with
- | DocInfo.classInfo i => pure #[← classInstancesToHtml i.name]
- | DocInfo.definitionInfo i => pure ((← equationsToHtml i) ++ #[← instancesForToHtml i.name])
- | DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo
- | DocInfo.classInductiveInfo i => pure #[← classInstancesToHtml i.name]
- | DocInfo.inductiveInfo i => pure #[← instancesForToHtml i.name]
- | DocInfo.structureInfo i => pure #[← instancesForToHtml i.name]
- | _ => pure #[]
- let attrs := doc.getAttrs
- let attrsHtml :=
- if attrs.size > 0 then
- let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
- #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
- else
- #[]
- let leanInkHtml :=
- if ← leanInkEnabled? then
- #[
-
- ]
- else
- #[]
-
- pure
-
-
-
- [leanInkHtml]
- [attrsHtml]
- {← docInfoHeader doc}
- [docStringHtml]
- [docInfoHtml]
- [extraInfoHtml]
-
-
-
-/--
-Rendering a module doc string, that is the ones with an ! after the opener
-as HTML.
--/
-def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do
- pure
-
- [← docStringToHtml mdoc.doc]
-
-
-/--
-Render a module member, that is either a module doc string or a declaration
-as HTML.
--/
-def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
- match member with
- | ModuleMember.docInfo d => docInfoToHtml module d
- | ModuleMember.modDoc d => modDocToHtml d
-
-def declarationToNavLink (module : Name) : Html :=
-
-
-/--
-Returns the list of all imports this module does.
--/
-def getImports (module : Name) : HtmlM (Array Name) := do
- let res ← getResult
- return res.moduleInfo.find! module |>.imports
-
-/--
-Sort the list of all modules this one is importing, linkify it
-and return the HTML.
--/
-def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
- let imports := (← getImports moduleName).qsort Name.lt
- imports.mapM (fun i => do return {← moduleToHtmlLink i} )
-
-/--
-Render the internal nav bar (the thing on the right on all module pages).
--/
-def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
- pure
-
-
- source
-
-
- Imports
-
- [← importsHtml moduleName]
-
-
-
- Imported by
-
-
-
- [members.map declarationToNavLink]
-
-
-/--
-The main entry point to rendering the HTML for an entire module.
--/
-def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do
- let relevantMembers := module.members.filter Process.ModuleMember.shouldRender
- let memberDocs ← relevantMembers.mapM (moduleMemberToHtml module.name)
- let memberNames := filterDocInfo relevantMembers |>.map DocInfo.getName
- templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[
- ← internalNav memberNames module.name,
- Html.element "main" false #[] memberDocs
- ]
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
deleted file mode 100644
index 7081e6d..0000000
--- a/DocGen4/Output/Navbar.lean
+++ /dev/null
@@ -1,111 +0,0 @@
-/-
-Copyright (c) 2021 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 DocGen4.Output.ToHtmlFormat
-import DocGen4.Output.Base
-
-namespace DocGen4
-namespace Output
-
-open Lean
-open scoped DocGen4.Jsx
-
-def moduleListFile (file : NameExt) : BaseHtmlM Html := do
- let contents :=
- if file.ext == .pdf then
- {s!"🗎 {file.getString!} (pdf )"}
- else
- {file.getString!}
- return
- {contents}
-
-
-/--
-Build the HTML tree representing the module hierarchy.
--/
-partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
- let children := Array.mk (h.getChildren.toList.map Prod.snd)
- let nodes ← children.mapM (fun c =>
- if c.getChildren.toList.length != 0 then
- moduleListDir c
- else if Hierarchy.isFile c && c.getChildren.toList.length = 0 then
- moduleListFile (Hierarchy.getNameExt c)
- else
- pure ""
- )
- let moduleLink ← moduleNameToHtmlLink h.getName
- let summary :=
- if h.isFile then
- {s!"{h.getName.getString!} ({file })"}
- else
- {h.getName.getString!}
-
- pure
-
- {summary}
- [nodes]
-
-
-/--
-Return a list of top level modules, linkified and rendered as HTML
--/
-def moduleList : BaseHtmlM Html := do
- let hierarchy ← getHierarchy
- let mut list := Array.empty
- for (_, cs) in hierarchy.getChildren do
- list := list.push <| ← moduleListDir cs
- return [list]
-
-/--
-The main entry point to rendering the navbar on the left hand side.
--/
-def navbar : BaseHtmlM Html := do
- pure
-
-
- [← baseHtmlHeadDeclarations]
-
-
-
-
-
-
-
-
-
- General documentation
-
-
- /-
- TODO: Add these in later
-
-
-
-
-
-
- -/
- Library
- {← moduleList}
-
- -- `input` is a void tag, but can be self-closed to make parsing easier.
-
Color scheme
-
-
-
-
-
-
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/NotFound.lean b/DocGen4/Output/NotFound.lean
deleted file mode 100644
index 976ba06..0000000
--- a/DocGen4/Output/NotFound.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-/-
-Copyright (c) 2021 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-import DocGen4.Output.ToHtmlFormat
-import DocGen4.Output.Template
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-
-/--
-Render the 404 page.
--/
-def notFound : BaseHtmlM Html := do templateExtends (baseHtml "404") <|
- pure <|
-
- 404 Not Found
- Unfortunately, the page you were looking for is no longer here.
-
-
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/Search.lean b/DocGen4/Output/Search.lean
deleted file mode 100644
index 8fdbff6..0000000
--- a/DocGen4/Output/Search.lean
+++ /dev/null
@@ -1,48 +0,0 @@
-/-
-Copyright (c) 2023 Jeremy Salwen. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeremy Salwen
--/
-import DocGen4.Output.ToHtmlFormat
-import DocGen4.Output.Template
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-
-def search : BaseHtmlM Html := do templateExtends (baseHtml "Search") <|
- pure <|
-
- Search Results
- Query:
-
-
- Allowed Kinds:
-
- def
-
- theorem
-
- inductive
-
- structure
-
- class
-
- instance
-
- axiom
-
- opaque
-
-
-
-
-
-
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean
deleted file mode 100644
index 44121f7..0000000
--- a/DocGen4/Output/SourceLinker.lean
+++ /dev/null
@@ -1,37 +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
-
-namespace DocGen4.Output.SourceLinker
-
-open Lean
-
-/--
-Given a lake workspace with all the dependencies as well as the hash of the
-compiler release to work with this provides a function to turn names of
-declarations into (optionally positional) Github URLs.
--/
-def sourceLinker (gitUrl? : Option String) : IO (Name → Option DeclarationRange → String) := do
- -- TOOD: Refactor this, we don't need to pass in the module into the returned closure
- -- since we have one sourceLinker per module
-
- return fun module range =>
- let parts := module.components.map Name.toString
- let path := String.intercalate "/" parts
- let root := module.getRoot
- let leanHash := Lean.githash
- let basic := if root == `Lean ∨ root == `Init then
- s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
- else if root == `Lake then
- s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/lake/{path}.lean"
- else
- gitUrl?.get!
-
- match range with
- | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
- | none => basic
-
-end DocGen4.Output.SourceLinker
diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
deleted file mode 100644
index 8f48dc3..0000000
--- a/DocGen4/Output/Structure.lean
+++ /dev/null
@@ -1,51 +0,0 @@
-import DocGen4.Output.Template
-import DocGen4.Output.DocString
-import DocGen4.Process
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-open Lean
-
-/--
-Render a single field consisting of its documentation, its name and its type as HTML.
--/
-def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
- let shortName := f.name.componentsRev.head!.toString
- let name := f.name.toString
- if let some doc := f.doc then
- let renderedDoc ← docStringToHtml doc
- pure
-
- {s!"{shortName} "} : [← infoFormatToHtml f.type]
- [renderedDoc]
-
- else
- pure
-
- {s!"{shortName} "} : [← infoFormatToHtml f.type]
-
-
-/--
-Render all information about a structure as HTML.
--/
-def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
- let structureHtml :=
- if Name.isSuffixOf `mk i.ctor.name then
- (
- [← i.fieldInfo.mapM fieldToHtml]
- )
- else
- let ctorShortName := i.ctor.name.componentsRev.head!.toString
- (
- {s!"{ctorShortName} "} :: (
-
- [← i.fieldInfo.mapM fieldToHtml]
-
- )
- )
- return #[structureHtml]
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean
deleted file mode 100644
index 5995e16..0000000
--- a/DocGen4/Output/Template.lean
+++ /dev/null
@@ -1,72 +0,0 @@
-/-
-Copyright (c) 2021 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-import DocGen4.Output.ToHtmlFormat
-import DocGen4.Output.Navbar
-
-namespace DocGen4
-namespace Output
-
-open scoped DocGen4.Jsx
-
-/--
-The HTML template used for all pages.
--/
-def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := do
- let moduleConstant :=
- if let some module := ← getCurrentName then
- #[]
- else
- #[]
- pure
-
-
- [← baseHtmlHeadDeclarations]
-
- {title}
-
-
-
-
-
- [moduleConstant]
-
-
-
-
-
-
-
-
-
-
-
-
-
-
- [site]
-
-
-
-
-
-
-
-/--
-A comfortability wrapper around `baseHtmlGenerator`.
--/
-def baseHtml (title : String) (site : Html) : BaseHtmlM Html := baseHtmlGenerator title #[site]
-
-end Output
-end DocGen4
diff --git a/DocGen4/Output/ToHtmlFormat.lean b/DocGen4/Output/ToHtmlFormat.lean
deleted file mode 100644
index 5a4285e..0000000
--- a/DocGen4/Output/ToHtmlFormat.lean
+++ /dev/null
@@ -1,149 +0,0 @@
-/-
-Copyright (c) 2021 Wojciech Nawrocki. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Authors: Wojciech Nawrocki, Sebastian Ullrich, Henrik Böving
--/
-import Lean.Data.Json
-import Lean.Parser
-
-/-! This module defines:
-- a representation of HTML trees
-- together with a JSX-like DSL for writing them
-- and widget support for visualizing any type as HTML. -/
-
-namespace DocGen4
-
-open Lean
-
-inductive Html where
- -- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson
- -- element (tag : String) (flatten : Bool) (attrs : Array HtmlAttribute) (children : Array Html)
- | element : String → Bool → Array (String × String) → Array Html → Html
- | text : String → Html
- deriving Repr, BEq, Inhabited, FromJson, ToJson
-
-instance : Coe String Html :=
- ⟨Html.text⟩
-
-namespace Html
-
-def attributesToString (attrs : Array (String × String)) :String :=
- attrs.foldl (fun acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ v ++ "\"") ""
-
--- TODO: Termination proof
-partial def toStringAux : Html → String
-| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}{tag}>\n"
-| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}{tag}>\n"
-| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}{tag}>\n"
-| element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}{tag}>"
-| text s => s
-
-def toString (html : Html) : String :=
- html.toStringAux.trimRight
-
-instance : ToString Html :=
- ⟨toString⟩
-
-partial def textLength : Html → Nat
-| text s => s.length
-| element _ _ _ children =>
- let lengths := children.map textLength
- lengths.foldl Nat.add 0
-
-def escapePairs : Array (String × String) :=
- #[
- ("&", "&"),
- ("<", "<"),
- (">", ">"),
- ("\"", """)
- ]
-
-def escape (s : String) : String :=
- escapePairs.foldl (fun acc (o, r) => acc.replace o r) s
-
-end Html
-
-namespace Jsx
-open Parser PrettyPrinter
-
-declare_syntax_cat jsxElement
-declare_syntax_cat jsxChild
-
--- JSXTextCharacter : SourceCharacter but not one of {, <, > or }
-def jsxText : Parser :=
- withAntiquot (mkAntiquot "jsxText" `jsxText) {
- fn := fun c s =>
- let startPos := s.pos
- let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s
- mkNodeToken `jsxText startPos c s }
-
-@[combinator_formatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
-@[combinator_parenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
-
-syntax jsxAttrName := rawIdent <|> str
-syntax jsxAttrVal := str <|> group("{" term "}")
-syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal
-syntax jsxAttrSpread := "[" term "]"
-syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
-
-syntax "<" rawIdent jsxAttr* "/>" : jsxElement
-syntax "<" rawIdent jsxAttr* ">" jsxChild* "" rawIdent ">" : jsxElement
-
-syntax jsxText : jsxChild
-syntax "{" term "}" : jsxChild
-syntax "[" term "]" : jsxChild
-syntax jsxElement : jsxChild
-
-scoped syntax:max jsxElement : term
-
-def translateAttrs (attrs : Array (TSyntax `DocGen4.Jsx.jsxAttr)) : MacroM (TSyntax `term) := do
- let mut as ← `(#[])
- for attr in attrs.map TSyntax.raw do
- as ← match attr with
- | `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
- let n ← match n with
- | `(jsxAttrName| $n:str) => pure n
- | `(jsxAttrName| $n:ident) => pure <| quote (toString n.getId)
- | _ => Macro.throwUnsupported
- let v ← match v with
- | `(jsxAttrVal| {$v}) => pure v
- | `(jsxAttrVal| $v:str) => pure v
- | _ => Macro.throwUnsupported
- `(($as).push ($n, ($v : String)))
- | `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))
- | _ => Macro.throwUnsupported
- return as
-
-private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × (TSyntax `term)):= do
- unless n.getId == m.getId do
- 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
- | `(jsxChild|$t:jsxText) => `(($cs).push (Html.text $(quote t.raw[0]!.getAtomVal)))
- -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
- | `(jsxChild|{$t}) => `(($cs).push ($t : Html))
- | `(jsxChild|[$t]) => `($cs ++ ($t : Array Html))
- | `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html))
- | _ => Macro.throwUnsupported
- let tag := toString n.getId
- pure <| (tag, cs)
-
-macro_rules
- | `(<$n $attrs* />) => do
- let kind := quote (toString n.getId)
- let attrs ← translateAttrs attrs
- `(Html.element $kind true $attrs #[])
- | `(<$n $attrs* >$children*$m>) => do
- let (tag, children) ← htmlHelper n children m
- `(Html.element $(quote tag) true $(← translateAttrs attrs) $children)
-
-end Jsx
-
-/-- A type which implements `ToHtmlFormat` will be visualized
-as the resulting HTML in editors which support it. -/
-class ToHtmlFormat (α : Type u) where
- formatHtml : α → Html
-
-end DocGen4
diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean
deleted file mode 100644
index 2843d05..0000000
--- a/DocGen4/Output/ToJson.lean
+++ /dev/null
@@ -1,151 +0,0 @@
-import Lean
-import DocGen4.Process
-import DocGen4.Output.Base
-import DocGen4.Output.Module
-import Lean.Data.RBMap
-
-namespace DocGen4.Output
-
-open Lean
-
-structure JsonDeclarationInfo where
- name : String
- kind : String
- doc : String
- docLink : String
- sourceLink : String
- line : Nat
- deriving FromJson, ToJson
-
-structure JsonDeclaration where
- info : JsonDeclarationInfo
- header : String
-deriving FromJson, ToJson
-
-structure JsonInstance where
- name : String
- className : String
- typeNames : Array String
- deriving FromJson, ToJson
-
-structure JsonModule where
- name : String
- declarations : List JsonDeclaration
- instances : Array JsonInstance
- imports : Array String
- deriving FromJson, ToJson
-
-structure JsonHeaderIndex where
- declarations : List (String × JsonDeclaration) := []
-
-structure JsonIndexedDeclarationInfo where
- kind : String
- docLink : String
- deriving FromJson, ToJson
-
-structure JsonIndexedModule where
- importedBy : Array String
- url : String
- deriving FromJson, ToJson
-
-structure JsonIndex where
- declarations : List (String × JsonIndexedDeclarationInfo) := []
- instances : HashMap String (RBTree String Ord.compare) := .empty
- modules : HashMap String JsonIndexedModule := {}
- instancesFor : HashMap String (RBTree String Ord.compare) := .empty
-
-instance : ToJson JsonHeaderIndex where
- toJson idx := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v))
-
-instance : ToJson JsonIndex where
- toJson idx := Id.run do
- let jsonDecls := Json.mkObj <| idx.declarations.map (fun (k, v) => (k, toJson v))
- let jsonInstances := Json.mkObj <| idx.instances.toList.map (fun (k, v) => (k, toJson v.toArray))
- let jsonModules := Json.mkObj <| idx.modules.toList.map (fun (k, v) => (k, toJson v))
- let jsonInstancesFor := Json.mkObj <| idx.instancesFor.toList.map (fun (k, v) => (k, toJson v.toArray))
- let finalJson := Json.mkObj [
- ("declarations", jsonDecls),
- ("instances", jsonInstances),
- ("modules", jsonModules),
- ("instancesFor", jsonInstancesFor)
- ]
- return finalJson
-
-def JsonHeaderIndex.addModule (index : JsonHeaderIndex) (module : JsonModule) : JsonHeaderIndex :=
- let merge idx decl := { idx with declarations := (decl.info.name, decl) :: idx.declarations }
- module.declarations.foldl merge index
-
-def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM JsonIndex := do
- let mut index := index
- let newDecls := module.declarations.map (fun d => (d.info.name, {
- kind := d.info.kind,
- docLink := d.info.docLink,
- }))
- index := { index with
- declarations := newDecls ++ index.declarations
- }
-
- -- TODO: In theory one could sort instances and imports by name and batch the writes
- for inst in module.instances do
- let mut insts := index.instances.findD inst.className {}
- insts := insts.insert inst.name
- index := { index with instances := index.instances.insert inst.className insts }
- for typeName in inst.typeNames do
- let mut instsFor := index.instancesFor.findD typeName {}
- instsFor := instsFor.insert inst.name
- index := { index with instancesFor := index.instancesFor.insert typeName instsFor }
-
- -- TODO: dedup
- if index.modules.find? module.name |>.isNone then
- let moduleLink <- moduleNameToLink (String.toName module.name)
- let indexedModule := { url := moduleLink, importedBy := #[] }
- index := { index with modules := index.modules.insert module.name indexedModule }
-
- for imp in module.imports do
- let indexedImp ←
- match index.modules.find? imp with
- | some i => pure i
- | none =>
- let impLink ← moduleNameToLink (String.toName imp)
- let indexedModule := { url := impLink, importedBy := #[] }
- pure indexedModule
- index := { index with
- modules :=
- index.modules.insert
- imp
- { indexedImp with importedBy := indexedImp.importedBy.push module.name }
- }
- return index
-
-def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
- let name := info.getName.toString
- let kind := info.getKind
- let doc := info.getDocString.getD ""
- let docLink ← declNameToLink info.getName
- let sourceLink ← getSourceUrl module info.getDeclarationRange
- let line := info.getDeclarationRange.pos.line
- let header := (← docInfoHeader info).toString
- let info := { name, kind, doc, docLink, sourceLink, line }
- return { info, header }
-
-def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
- let mut jsonDecls := []
- let mut instances := #[]
- let declInfo := Process.filterDocInfo module.members
- for decl in declInfo do
- jsonDecls := (← DocInfo.toJson module.name decl) :: jsonDecls
- if let .instanceInfo i := decl then
- instances := instances.push {
- name := i.name.toString,
- className := i.className.toString
- typeNames := i.typeNames.map Name.toString
- }
- let jsonMod : JsonModule := {
- name := module.name.toString,
- declarations := jsonDecls,
- instances,
- imports := module.imports.map Name.toString
- }
- return ToJson.toJson jsonMod
-
-end DocGen4.Output
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
deleted file mode 100644
index dd6a317..0000000
--- a/DocGen4/Process.lean
+++ /dev/null
@@ -1,21 +0,0 @@
-/-
-Copyright (c) 2021 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
--/
-
-import DocGen4.Process.Analyze
-import DocGen4.Process.Attributes
-import DocGen4.Process.AxiomInfo
-import DocGen4.Process.Base
-import DocGen4.Process.ClassInfo
-import DocGen4.Process.DefinitionInfo
-import DocGen4.Process.DocInfo
-import DocGen4.Process.Hierarchy
-import DocGen4.Process.InductiveInfo
-import DocGen4.Process.InstanceInfo
-import DocGen4.Process.NameExt
-import DocGen4.Process.NameInfo
-import DocGen4.Process.OpaqueInfo
-import DocGen4.Process.StructureInfo
-import DocGen4.Process.TheoremInfo
diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean
deleted file mode 100644
index 3e6600d..0000000
--- a/DocGen4/Process/Analyze.lean
+++ /dev/null
@@ -1,163 +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 Lean.Data.HashMap
-import Lean.Data.HashSet
-
-import DocGen4.Process.Base
-import DocGen4.Process.Hierarchy
-import DocGen4.Process.DocInfo
-
-namespace DocGen4.Process
-
-open Lean Meta
-
-/--
-Member of a module, either a declaration or some module doc string.
--/
-inductive ModuleMember where
-| docInfo (info : DocInfo) : ModuleMember
-| modDoc (doc : ModuleDoc) : ModuleMember
-deriving Inhabited
-
-/--
-A Lean module.
--/
-structure Module where
- /--
- Name of the module.
- -/
- name : Name
- /--
- All members of the module, sorted according to their line numbers.
- -/
- members : Array ModuleMember
- imports : Array Name
- deriving Inhabited
-
-/--
-The result of running a full doc-gen analysis on a project.
--/
-structure AnalyzerResult where
- /--
- The map from module names to indices of the `moduleNames` array.
- -/
- name2ModIdx : HashMap Name ModuleIdx
- /--
- The list of all modules, accessible nicely via `name2ModIdx`.
- -/
- moduleNames : Array Name
- /--
- A map from module names to information about these modules.
- -/
- moduleInfo : HashMap Name Module
- deriving Inhabited
-
-namespace ModuleMember
-
-def getDeclarationRange : ModuleMember → DeclarationRange
-| docInfo i => i.getDeclarationRange
-| modDoc i => i.declarationRange
-
-/--
-An order for module members, based on their declaration range.
--/
-def order (l r : ModuleMember) : Bool :=
- Position.lt l.getDeclarationRange.pos r.getDeclarationRange.pos
-
-def getName : ModuleMember → Name
-| docInfo i => i.getName
-| modDoc _ => Name.anonymous
-
-def getDocString : ModuleMember → Option String
-| docInfo i => i.getDocString
-| modDoc i => i.doc
-
-def shouldRender : ModuleMember → Bool
-| docInfo i => i.shouldRender
-| modDoc _ => true
-
-end ModuleMember
-
-inductive AnalyzeTask where
-| loadAll (load : Array Name) : AnalyzeTask
-| loadAllLimitAnalysis (analyze : Array Name) : AnalyzeTask
-
-def AnalyzeTask.getLoad : AnalyzeTask → Array Name
-| loadAll load => load
-| loadAllLimitAnalysis load => load
-
-def getAllModuleDocs (relevantModules : Array Name) : MetaM (HashMap Name Module) := do
- let env ← getEnv
- let mut res := mkHashMap relevantModules.size
- for module in relevantModules do
- let modDocs := getModuleDoc? env module |>.getD #[] |>.map .modDoc
- let some modIdx := env.getModuleIdx? module | unreachable!
- let moduleData := env.header.moduleData.get! modIdx
- let imports := moduleData.imports.map Import.module
- res := res.insert module <| Module.mk module modDocs imports
- return res
-
-/--
-Run the doc-gen analysis on all modules that are loaded into the `Environment`
-of this `MetaM` run and mentioned by the `AnalyzeTask`.
--/
-def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
- let env ← getEnv
- let relevantModules := match task with
- | .loadAll _ => HashSet.fromArray env.header.moduleNames
- | .loadAllLimitAnalysis analysis => HashSet.fromArray analysis
- let allModules := env.header.moduleNames
-
- let mut res ← getAllModuleDocs relevantModules.toArray
-
- for (name, cinfo) in env.constants.toList do
- let some modidx := env.getModuleIdxFor? name | unreachable!
- let moduleName := env.allImportedModuleNames.get! modidx
- if !relevantModules.contains moduleName then
- continue
-
- try
- let config := {
- maxHeartbeats := 5000000,
- options := ← getOptions,
- fileName := ← getFileName,
- fileMap := ← getFileMap,
- catchRuntimeEx := true,
- }
- let analysis ← Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant (name, cinfo)) config { env := env } {} {}
- if let some dinfo := analysis then
- let moduleName := env.allImportedModuleNames.get! modidx
- let module := res.find! moduleName
- res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
- catch e =>
- if let some pos := e.getRef.getPos? then
- let pos := (← getFileMap).toPosition pos
- IO.println s!"WARNING: Failed to obtain information in file: {pos}, for: {name}, {← e.toMessageData.toString}"
- else
- IO.println s!"WARNING: Failed to obtain information for: {name}: {← e.toMessageData.toString}"
-
- -- TODO: This could probably be faster if we did sorted insert above instead
- for (moduleName, module) in res.toArray do
- res := res.insert moduleName {module with members := module.members.qsort ModuleMember.order}
-
- let hierarchy := Hierarchy.fromArray allModules
- let analysis := {
- name2ModIdx := env.const2ModIdx,
- moduleNames := allModules,
- moduleInfo := res,
- }
- return (analysis, hierarchy)
-
-def filterDocInfo (ms : Array ModuleMember) : Array DocInfo :=
- ms.filterMap filter
- where
- filter : ModuleMember → Option DocInfo
- | ModuleMember.docInfo i => some i
- | _ => none
-
-end DocGen4.Process
diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean
deleted file mode 100644
index ff6e7f3..0000000
--- a/DocGen4/Process/Attributes.lean
+++ /dev/null
@@ -1,182 +0,0 @@
-import Lean
-
-namespace DocGen4
-
-open Lean Meta
--- The following is probably completely overengineered but I love it
-
-/--
-Captures the notion of a value based attributes, `attrKind` is things like
-`EnumAttributes`.
--/
-class ValueAttr (attrKind : Type → Type) where
- /--
- Given a certain value based attribute, an `Environment` and the `Name` of
- a declaration returns the value of the attribute on this declaration if present.
- -/
- getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Environment → Name → Option String
-
-/--
-Contains a specific attribute declaration of a certain attribute kind (enum based, parametric etc.).
--/
-structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
- {α : Type}
- attr : attrKind α
- [str : ToString α]
- [inhab : Inhabited α]
-
-/--
-Obtain the value of an enum attribute for a certain name.
--/
-def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := do
- let val ← EnumAttributes.getValue attr env decl
- some (toString val)
-
-instance : ValueAttr EnumAttributes where
- getValue := enumGetValue
-
-/--
-Obtain the value of a parametric attribute for a certain name.
--/
-def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := do
- let val ← ParametricAttribute.getParam? attr env decl
- some (attr.attr.name.toString ++ " " ++ toString val)
-
-instance : ValueAttr ParametricAttribute where
- getValue := parametricGetValue
-
-abbrev EnumAttrWrapper := ValueAttrWrapper EnumAttributes
-abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute
-
-/--
-The list of all tag based attributes doc-gen knows about and can recover.
--/
-def tagAttributes : Array TagAttribute :=
- #[IR.UnboxResult.unboxAttr, neverExtractAttr,
- Elab.Term.elabWithoutExpectedTypeAttr, matchPatternAttr]
-
-deriving instance Repr for Compiler.InlineAttributeKind
-deriving instance Repr for Compiler.SpecializeAttributeKind
-
-open Compiler in
-instance : ToString InlineAttributeKind where
- toString kind :=
- match kind with
- | .inline => "inline"
- | .noinline => "noinline"
- | .macroInline => "macro_inline"
- | .inlineIfReduce => "inline_if_reduce"
- | .alwaysInline => "always_inline"
-
-open Compiler in
-instance : ToString SpecializeAttributeKind where
- toString kind :=
- match kind with
- | .specialize => "specialize"
- | .nospecialize => "nospecialize"
-
-instance : ToString ReducibilityStatus where
- toString kind :=
- match kind with
- | .reducible => "reducible"
- | .semireducible => "semireducible"
- | .irreducible => "irreducible"
-
-/--
-The list of all enum based attributes doc-gen knows about and can recover.
--/
-@[reducible]
-def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨reducibilityAttrs⟩]
-
-instance : ToString ExternEntry where
- toString entry :=
- match entry with
- | .adhoc `all => ""
- | .adhoc backend => s!"{backend} adhoc"
- | .standard `all fn => fn
- | .standard backend fn => s!"{backend} {fn}"
- | .inline backend pattern => s!"{backend} inline {String.quote pattern}"
- -- TODO: The docs in the module dont specific how to render this
- | .foreign backend fn => s!"{backend} foreign {fn}"
-
-instance : ToString ExternAttrData where
- toString data := (data.arity?.map toString |>.getD "") ++ " " ++ String.intercalate " " (data.entries.map toString)
-
-/--
-The list of all parametric attributes (that is, attributes with any kind of information attached)
-doc-gen knows about and can recover.
--/
-def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩, ⟨exportAttr⟩, ⟨Compiler.specializeAttr⟩]
-
-def getTags (decl : Name) : MetaM (Array String) := do
- let env ← getEnv
- return tagAttributes.filter (TagAttribute.hasTag · env decl) |>.map (·.attr.name.toString)
-
-def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind] [Inhabited α] [ToString α] (decl : Name) (attr : attrKind α) : MetaM (Option String) := do
- let env ← getEnv
- return va.getValue attr env decl
-
-def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do
- let mut res := #[]
- for attr in attrs do
- if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then
- res := res.push val
- return res
-
-def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes
-def getParametricValues (decl : Name) : MetaM (Array String) := do
- let mut uniform ← getValues decl parametricAttributes
- -- This attribute contains an `Option Name` but we would like to pretty print it better
- if let some depTag := Linter.deprecatedAttr.getParam? (← getEnv) decl then
- let str := match depTag with
- | some alt => s!"deprecated {alt.toString}"
- | none => "deprecated"
- uniform := uniform.push str
- return uniform
-
-def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do
- let insts ← getDefaultInstances className
- for (inst, prio) in insts do
- if inst == decl then
- return some s!"defaultInstance {prio}"
- return none
-
-def hasSimp (decl : Name) : MetaM (Option String) := do
- let thms ← simpExtension.getTheorems
- if thms.isLemma (.decl decl) then
- return "simp"
- else
- return none
-
-def hasCsimp (decl : Name) : MetaM (Option String) := do
- let env ← getEnv
- if Compiler.hasCSimpAttribute env decl then
- return some "csimp"
- else
- return none
-
-/--
-The list of custom attributes, that don't fit in the parametric or enum
-attribute kinds, doc-gen konws about and can recover.
--/
-def customAttrs := #[hasSimp, hasCsimp]
-
-def getCustomAttrs (decl : Name) : MetaM (Array String) := do
- let mut values := #[]
- for attr in customAttrs do
- if let some value ← attr decl then
- values := values.push value
- return values
-
-/--
-The main entry point for recovering all attribute values for a given
-declaration.
--/
-def getAllAttributes (decl : Name) : MetaM (Array String) := do
- let tags ← getTags decl
- let enums ← getEnumValues decl
- let parametric ← getParametricValues decl
- let customs ← getCustomAttrs decl
- return customs ++ tags ++ enums ++ parametric
-
-end DocGen4
diff --git a/DocGen4/Process/AxiomInfo.lean b/DocGen4/Process/AxiomInfo.lean
deleted file mode 100644
index 6d87398..0000000
--- a/DocGen4/Process/AxiomInfo.lean
+++ /dev/null
@@ -1,22 +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 DocGen4.Process.Base
-import DocGen4.Process.NameInfo
-
-namespace DocGen4.Process
-
-open Lean Meta
-
-def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
- let info ← Info.ofConstantVal v.toConstantVal
- return {
- toInfo := info,
- isUnsafe := v.isUnsafe
- }
-
-end DocGen4.Process
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
deleted file mode 100644
index cf3df3a..0000000
--- a/DocGen4/Process/Base.lean
+++ /dev/null
@@ -1,198 +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
-
-namespace DocGen4.Process
-open Lean Widget Meta
-
-/--
-Stores information about a typed name.
--/
-structure NameInfo where
- /--
- The name that has this info attached.
- -/
- name : Name
- /--
- The pretty printed type of this name.
- -/
- type : CodeWithInfos
- /--
- The doc string of the name if it exists.
- -/
- doc : Option String
- deriving Inhabited
-
-
-/--
-An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
--/
-structure Arg where
- /--
- The name of the argument. For auto generated argument names like `[Monad α]`
- this is none
- -/
- name : Option Name
- /--
- The pretty printed type of the argument.
- -/
- type : CodeWithInfos
- /--
- What kind of binder was used for the argument.
- -/
- binderInfo : BinderInfo
-
-/--
-A base structure for information about a declaration.
--/
-structure Info extends NameInfo where
- /--
- The list of arguments to the declaration.
- -/
- args : Array Arg
- /--
- In which lines the declaration was created.
- -/
- declarationRange : DeclarationRange
- /--
- A list of (known) attributes that are attached to the declaration.
- -/
- attrs : Array String
- /--
- Whether this info item should be rendered
- -/
- render : Bool := true
- deriving Inhabited
-
-/--
-Information about an `axiom` declaration.
--/
-structure AxiomInfo extends Info where
- isUnsafe : Bool
- deriving Inhabited
-
-/--
-Information about a `theorem` declaration.
--/
-structure TheoremInfo extends Info
- deriving Inhabited
-
-/--
-Information about an `opaque` declaration.
--/
-structure OpaqueInfo extends Info where
- /--
- The pretty printed value of the declaration.
- -/
- value : CodeWithInfos
- /--
- A value of partial is interpreted as this opaque being part of a partial def
- since the actual definition for a partial def is hidden behind an inaccessible value.
- -/
- definitionSafety : DefinitionSafety
- deriving Inhabited
-
-/--
-Information about a `def` declaration, note that partial defs are handled by `OpaqueInfo`.
--/
-structure DefinitionInfo extends Info where
- isUnsafe : Bool
- hints : ReducibilityHints
- equations : Option (Array CodeWithInfos)
- isNonComputable : Bool
- deriving Inhabited
-
-/--
-Information about an `instance` declaration.
--/
-structure InstanceInfo extends DefinitionInfo where
- className : Name
- typeNames : Array Name
- deriving Inhabited
-
-/--
-Information about an `inductive` declaration
--/
-structure InductiveInfo extends Info where
- /--
- List of all constructors of this inductive type.
- -/
- ctors : List NameInfo
- isUnsafe : Bool
- deriving Inhabited
-
-/--
-Information about a `structure` declaration.
--/
-structure StructureInfo extends Info where
- /--
- Information about all the fields of the structure.
- -/
- fieldInfo : Array NameInfo
- /--
- All the structures this one inherited from.
- -/
- parents : Array Name
- /--
- The constructor of the structure.
- -/
- ctor : NameInfo
- deriving Inhabited
-
-/--
-Information about a `class` declaration.
--/
-abbrev ClassInfo := StructureInfo
-
-/--
-Information about a `class inductive` declaration.
--/
-abbrev ClassInductiveInfo := InductiveInfo
-
-
-/--
-Information about a constructor of an inductive type
--/
-abbrev ConstructorInfo := Info
-
-/--
-A general type for informations about declarations.
--/
-inductive DocInfo where
-| axiomInfo (info : AxiomInfo) : DocInfo
-| theoremInfo (info : TheoremInfo) : DocInfo
-| opaqueInfo (info : OpaqueInfo) : DocInfo
-| definitionInfo (info : DefinitionInfo) : DocInfo
-| instanceInfo (info : InstanceInfo) : DocInfo
-| inductiveInfo (info : InductiveInfo) : DocInfo
-| structureInfo (info : StructureInfo) : DocInfo
-| classInfo (info : ClassInfo) : DocInfo
-| classInductiveInfo (info : ClassInductiveInfo) : DocInfo
-| ctorInfo (info : ConstructorInfo) : DocInfo
- deriving Inhabited
-
-/--
-Turns an `Expr` into a pretty printed `CodeWithInfos`.
--/
-def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
- let ⟨fmt, infos⟩ ← PrettyPrinter.ppExprWithInfos expr
- let tt := TaggedText.prettyTagged fmt
- let ctx := {
- env := ← getEnv
- mctx := ← getMCtx
- options := ← getOptions
- currNamespace := ← getCurrNamespace
- openDecls := ← getOpenDecls
- fileMap := default,
- ngen := ← getNGen
- }
- return tagCodeInfos ctx infos tt
-
-def isInstance (declName : Name) : MetaM Bool := do
- return (instanceExtension.getState (← getEnv)).instanceNames.contains declName
-
-end DocGen4.Process
diff --git a/DocGen4/Process/ClassInfo.lean b/DocGen4/Process/ClassInfo.lean
deleted file mode 100644
index 0c29db7..0000000
--- a/DocGen4/Process/ClassInfo.lean
+++ /dev/null
@@ -1,24 +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 DocGen4.Process.Base
-import DocGen4.Process.NameInfo
-import DocGen4.Process.StructureInfo
-import DocGen4.Process.InductiveInfo
-
-namespace DocGen4.Process
-
-open Lean Meta
-
-def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
- StructureInfo.ofInductiveVal v
-
-def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
- InductiveInfo.ofInductiveVal v
-
-end DocGen4.Process
diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean
deleted file mode 100644
index 6f75b7c..0000000
--- a/DocGen4/Process/DefinitionInfo.lean
+++ /dev/null
@@ -1,74 +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 DocGen4.Process.Base
-import DocGen4.Process.NameInfo
-
-namespace DocGen4.Process
-
-open Lean Meta Widget
-
-partial def stripArgs (e : Expr) (k : Expr → MetaM α) : MetaM α :=
- match e.consumeMData with
- | Expr.forallE name type body bi =>
- let name := name.eraseMacroScopes
- Meta.withLocalDecl name bi type fun fvar => do
- stripArgs (Expr.instantiate1 body fvar) k
- | _ => k e
-
-def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
- withOptions (tactic.hygienic.set . false) do
- lambdaTelescope v.value fun xs body => do
- let us := v.levelParams.map mkLevelParam
- let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
- let type ← mkForallFVars xs type
- return type
-
-def processEq (eq : Name) : MetaM CodeWithInfos := do
- let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
- stripArgs type prettyPrintTerm
-
-def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
- let info ← Info.ofConstantVal v.toConstantVal
- let isUnsafe := v.safety == DefinitionSafety.unsafe
- let isNonComputable := isNoncomputable (← getEnv) v.name
-
- try
- let eqs? ← getEqnsFor? v.name
-
- match eqs? with
- | some eqs =>
- let equations ← eqs.mapM processEq
- return {
- toInfo := info,
- isUnsafe,
- hints := v.hints,
- equations,
- isNonComputable
- }
- | none =>
- let equations := #[← stripArgs (← valueToEq v) prettyPrintTerm]
- return {
- toInfo := info,
- isUnsafe,
- hints := v.hints,
- equations,
- isNonComputable
- }
- catch err =>
- IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {← err.toMessageData.toString}"
- return {
- toInfo := info,
- isUnsafe,
- hints := v.hints,
- equations := none,
- isNonComputable
- }
-
-
-
-end DocGen4.Process
diff --git a/DocGen4/Process/DocInfo.lean b/DocGen4/Process/DocInfo.lean
deleted file mode 100644
index e736c16..0000000
--- a/DocGen4/Process/DocInfo.lean
+++ /dev/null
@@ -1,223 +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 DocGen4.Process.Base
-import DocGen4.Process.AxiomInfo
-import DocGen4.Process.TheoremInfo
-import DocGen4.Process.OpaqueInfo
-import DocGen4.Process.InstanceInfo
-import DocGen4.Process.DefinitionInfo
-import DocGen4.Process.ClassInfo
-import DocGen4.Process.StructureInfo
-import DocGen4.Process.InductiveInfo
-
-
-namespace DocGen4.Process
-namespace DocInfo
-
-open Lean Meta Widget
-
-def getDeclarationRange : DocInfo → DeclarationRange
-| axiomInfo i => i.declarationRange
-| theoremInfo i => i.declarationRange
-| opaqueInfo i => i.declarationRange
-| definitionInfo i => i.declarationRange
-| instanceInfo i => i.declarationRange
-| inductiveInfo i => i.declarationRange
-| structureInfo i => i.declarationRange
-| classInfo i => i.declarationRange
-| classInductiveInfo i => i.declarationRange
-| ctorInfo i => i.declarationRange
-
-def getName : DocInfo → Name
-| axiomInfo i => i.name
-| theoremInfo i => i.name
-| opaqueInfo i => i.name
-| definitionInfo i => i.name
-| instanceInfo i => i.name
-| inductiveInfo i => i.name
-| structureInfo i => i.name
-| classInfo i => i.name
-| classInductiveInfo i => i.name
-| ctorInfo i => i.name
-
-def getKind : DocInfo → String
-| axiomInfo _ => "axiom"
-| theoremInfo _ => "theorem"
-| opaqueInfo _ => "opaque"
-| definitionInfo _ => "def"
-| instanceInfo _ => "instance"
-| inductiveInfo _ => "inductive"
-| structureInfo _ => "structure"
-| classInfo _ => "class"
-| classInductiveInfo _ => "class"
-| ctorInfo _ => "ctor" -- TODO: kind ctor support in js
-
-def getType : DocInfo → CodeWithInfos
-| axiomInfo i => i.type
-| theoremInfo i => i.type
-| opaqueInfo i => i.type
-| definitionInfo i => i.type
-| instanceInfo i => i.type
-| inductiveInfo i => i.type
-| structureInfo i => i.type
-| classInfo i => i.type
-| classInductiveInfo i => i.type
-| ctorInfo i => i.type
-
-def getArgs : DocInfo → Array Arg
-| axiomInfo i => i.args
-| theoremInfo i => i.args
-| opaqueInfo i => i.args
-| definitionInfo i => i.args
-| instanceInfo i => i.args
-| inductiveInfo i => i.args
-| structureInfo i => i.args
-| classInfo i => i.args
-| classInductiveInfo i => i.args
-| ctorInfo i => i.args
-
-def getAttrs : DocInfo → Array String
-| axiomInfo i => i.attrs
-| theoremInfo i => i.attrs
-| opaqueInfo i => i.attrs
-| definitionInfo i => i.attrs
-| instanceInfo i => i.attrs
-| inductiveInfo i => i.attrs
-| structureInfo i => i.attrs
-| classInfo i => i.attrs
-| classInductiveInfo i => i.attrs
-| ctorInfo i => i.attrs
-
-def getDocString : DocInfo → Option String
-| axiomInfo i => i.doc
-| theoremInfo i => i.doc
-| opaqueInfo i => i.doc
-| definitionInfo i => i.doc
-| instanceInfo i => i.doc
-| inductiveInfo i => i.doc
-| structureInfo i => i.doc
-| classInfo i => i.doc
-| classInductiveInfo i => i.doc
-| ctorInfo i => i.doc
-
-def shouldRender : DocInfo → Bool
-| axiomInfo i => i.render
-| theoremInfo i => i.render
-| opaqueInfo i => i.render
-| definitionInfo i => i.render
-| instanceInfo i => i.render
-| inductiveInfo i => i.render
-| structureInfo i => i.render
-| classInfo i => i.render
-| classInductiveInfo i => i.render
-| ctorInfo i => i.render
-
-def isBlackListed (declName : Name) : MetaM Bool := do
- match ← findDeclarationRanges? declName with
- | some _ =>
- let env ← getEnv
- pure (declName.isInternal)
- <||> (pure <| isAuxRecursor env declName)
- <||> (pure <| isNoConfusion env declName)
- <||> isRec declName
- <||> isMatcher declName
- -- TODO: Evaluate whether filtering out declarations without range is sensible
- | none => return true
-
--- TODO: Is this actually the best way?
-def isProjFn (declName : Name) : MetaM Bool := do
- let env ← getEnv
- match declName with
- | Name.str parent name =>
- if isStructure env parent then
- match getStructureInfo? env parent with
- | some i =>
- match i.fieldNames.find? (· == name) with
- | some _ => return true
- | none => return false
- | none => panic! s!"{parent} is not a structure"
- else
- return false
- | _ => return false
-
-def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := fun (name, info) => do
- if ← isBlackListed name then
- return none
- match info with
- | ConstantInfo.axiomInfo i => return some <| axiomInfo (← AxiomInfo.ofAxiomVal i)
- | ConstantInfo.thmInfo i => return some <| theoremInfo (← TheoremInfo.ofTheoremVal i)
- | ConstantInfo.opaqueInfo i => return some <| opaqueInfo (← OpaqueInfo.ofOpaqueVal i)
- | ConstantInfo.defnInfo i =>
- if ← isProjFn i.name then
- let info ← DefinitionInfo.ofDefinitionVal i
- return some <| definitionInfo { info with render := false }
- else
- if ← isInstance i.name then
- let info ← InstanceInfo.ofDefinitionVal i
- return some <| instanceInfo info
- else
- let info ← DefinitionInfo.ofDefinitionVal i
- return some <| definitionInfo info
- | ConstantInfo.inductInfo i =>
- let env ← getEnv
- if isStructure env i.name then
- if isClass env i.name then
- return some <| classInfo (← ClassInfo.ofInductiveVal i)
- else
- return some <| structureInfo (← StructureInfo.ofInductiveVal i)
- else
- if isClass env i.name then
- return some <| classInductiveInfo (← ClassInductiveInfo.ofInductiveVal i)
- else
- return some <| inductiveInfo (← InductiveInfo.ofInductiveVal i)
- | ConstantInfo.ctorInfo i =>
- let info ← Info.ofConstantVal i.toConstantVal
- return some <| ctorInfo { info with render := false }
- -- we ignore these for now
- | ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => return none
-
-def getKindDescription : DocInfo → String
-| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
-| theoremInfo _ => "theorem"
-| opaqueInfo i =>
- match i.definitionSafety with
- | DefinitionSafety.safe => "opaque"
- | DefinitionSafety.unsafe => "unsafe opaque"
- | DefinitionSafety.partial => "partial def"
-| definitionInfo i => Id.run do
- let mut modifiers := #[]
- if i.isUnsafe then
- modifiers := modifiers.push "unsafe"
- if i.isNonComputable then
- modifiers := modifiers.push "noncomputable"
-
- let defKind :=
- if i.hints.isAbbrev then
- "abbrev"
- else
- "def"
- modifiers := modifiers.push defKind
- return String.intercalate " " modifiers.toList
-| instanceInfo i => Id.run do
- let mut modifiers := #[]
- if i.isUnsafe then
- modifiers := modifiers.push "unsafe"
- if i.isNonComputable then
- modifiers := modifiers.push "noncomputable"
-
- modifiers := modifiers.push "instance"
- return String.intercalate " " modifiers.toList
-| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
-| structureInfo _ => "structure"
-| classInfo _ => "class"
-| classInductiveInfo _ => "class inductive"
-| ctorInfo _ => "constructor"
-
-end DocInfo
-
-end DocGen4.Process
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean
deleted file mode 100644
index 6d10e88..0000000
--- a/DocGen4/Process/Hierarchy.lean
+++ /dev/null
@@ -1,138 +0,0 @@
-/-
-Copyright (c) 2021 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 Lean.Data.HashMap
-
-import DocGen4.Process.NameExt
-
-def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α :=
- xs.foldr (flip .insert) .empty
-
-namespace DocGen4
-
-open Lean Name
-
-def getNLevels (name : Name) (levels: Nat) : Name :=
- let components := name.componentsRev
- (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
-
-inductive Hierarchy where
-| node (name : NameExt) (isFile : Bool) (children : RBNode NameExt (fun _ => Hierarchy)) : Hierarchy
-
-instance : Inhabited Hierarchy := ⟨Hierarchy.node ⟨.anonymous, .html⟩ false RBNode.leaf⟩
-
-abbrev HierarchyMap := RBNode NameExt (fun _ => Hierarchy)
-
--- Everything in this namespace is adapted from stdlib's RBNode
-namespace HierarchyMap
-
-def toList : HierarchyMap → List (NameExt × Hierarchy)
-| t => t.revFold (fun ps k v => (k, v)::ps) []
-
-def toArray : HierarchyMap → Array (NameExt × Hierarchy)
-| t => t.fold (fun ps k v => ps ++ #[(k, v)] ) #[]
-
-def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (NameExt × Hierarchy) → σ → m (ForInStep σ)) : m σ :=
- t.forIn init (fun a b acc => f (a, b) acc)
-
-instance : ForIn m HierarchyMap (NameExt × Hierarchy) where
- forIn := HierarchyMap.hForIn
-
-end HierarchyMap
-
-namespace Hierarchy
-
-def empty (n : NameExt) (isFile : Bool) : Hierarchy :=
- node n isFile RBNode.leaf
-
-def getName : Hierarchy → Name
-| node n _ _ => n.name
-
-def getNameExt : Hierarchy → NameExt
-| node n _ _ => n
-
-def getChildren : Hierarchy → HierarchyMap
-| node _ _ c => c
-
-def isFile : Hierarchy → Bool
-| node _ f _ => f
-
-partial def insert! (h : Hierarchy) (n : NameExt) : Hierarchy := Id.run do
- let hn := h.getNameExt
- let mut cs := h.getChildren
-
- if getNumParts hn.name + 1 == getNumParts n.name then
- match cs.find NameExt.cmp n with
- | none =>
- node hn h.isFile (cs.insert NameExt.cmp n <| empty n true)
- | some (node _ true _) => h
- | some (node _ false ccs) =>
- cs := cs.erase NameExt.cmp n
- node hn h.isFile (cs.insert NameExt.cmp n <| node n true ccs)
- else
- let leveled := ⟨getNLevels n.name (getNumParts hn.name + 1), .html⟩
- match cs.find NameExt.cmp leveled with
- | some nextLevel =>
- cs := cs.erase NameExt.cmp leveled
- -- BUG?
- node hn h.isFile <| cs.insert NameExt.cmp leveled (nextLevel.insert! n)
- | none =>
- let child := (insert! (empty leveled false) n)
- node hn h.isFile <| cs.insert NameExt.cmp leveled child
-
-partial def fromArray (names : Array Name) : Hierarchy :=
- (names.map (fun n => NameExt.mk n .html)).foldl insert! (empty ⟨anonymous, .html⟩ false)
-
-partial def fromArrayExt (names : Array NameExt) : Hierarchy :=
- names.foldl insert! (empty ⟨anonymous, .html⟩ false)
-
-def baseDirBlackList : HashSet String :=
- HashSet.fromArray #[
- "404.html",
- "color-scheme.js",
- "declaration-data.js",
- "declarations",
- "expand-nav.js",
- "find",
- "foundational_types.html",
- "how-about.js",
- "index.html",
- "jump-src.js",
- "mathjax-config.js",
- "navbar.html",
- "nav.js",
- "search.html",
- "search.js",
- "src",
- "style.css"
- ]
-
-partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array NameExt) := do
- let mut children := #[]
- for entry in ← System.FilePath.readDir dir do
- if ← entry.path.isDir then
- children := children ++ (← fromDirectoryAux entry.path (.str previous entry.fileName))
- else if entry.path.extension = some "html" then
- children := children.push <| ⟨.str previous (entry.fileName.dropRight ".html".length), .html⟩
- else if entry.path.extension = some "pdf" then
- children := children.push <| ⟨.str previous (entry.fileName.dropRight ".pdf".length), .pdf⟩
- return children
-
-def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
- let mut children := #[]
- for entry in ← System.FilePath.readDir dir do
- if baseDirBlackList.contains entry.fileName then
- continue
- else if ← entry.path.isDir then
- children := children ++ (← fromDirectoryAux entry.path (.mkSimple entry.fileName))
- else if entry.path.extension = some "html" then
- children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".html".length), .html⟩
- else if entry.path.extension = some "pdf" then
- children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".pdf".length), .pdf⟩
- return Hierarchy.fromArrayExt children
-
-end Hierarchy
-end DocGen4
diff --git a/DocGen4/Process/InductiveInfo.lean b/DocGen4/Process/InductiveInfo.lean
deleted file mode 100644
index 1c27a1d..0000000
--- a/DocGen4/Process/InductiveInfo.lean
+++ /dev/null
@@ -1,30 +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 DocGen4.Process.Base
-import DocGen4.Process.NameInfo
-
-namespace DocGen4.Process
-
-open Lean Meta
-
-def getConstructorType (ctor : Name) : MetaM Expr := do
- let env ← getEnv
- match env.find? ctor with
- | some (ConstantInfo.ctorInfo i) => pure i.type
- | _ => panic! s!"Constructor {ctor} was requested but does not exist"
-
-def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
- let info ← Info.ofConstantVal v.toConstantVal
- let ctors ← v.ctors.mapM (fun name => do NameInfo.ofTypedName name (← getConstructorType name))
- return {
- toInfo := info,
- ctors,
- isUnsafe := v.isUnsafe
- }
-
-end DocGen4.Process
diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean
deleted file mode 100644
index df37004..0000000
--- a/DocGen4/Process/InstanceInfo.lean
+++ /dev/null
@@ -1,45 +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 DocGen4.Process.Base
-import DocGen4.Process.NameInfo
-import DocGen4.Process.DefinitionInfo
-
-namespace DocGen4.Process
-
-open Lean Meta
-
-def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do
- let (_, _, tail) ← forallMetaTelescopeReducing typ
- let args := tail.getAppArgs
- let (_, bis, _) ← forallMetaTelescopeReducing (← inferType tail.getAppFn)
- let (_, names) ← (bis.zip args).mapM findName |>.run .empty
- return names
-where
- findName : BinderInfo × Expr → StateRefT (Array Name) MetaM Unit
- | (.default, .sort .zero) => modify (·.push "_builtin_prop")
- | (.default, .sort (.succ _)) => modify (·.push "_builtin_typeu")
- | (.default, .sort _) => modify (·.push "_builtin_sortu")
- | (.default, e) =>
- match e.getAppFn with
- | .const name .. => modify (·.push name)
- | _ => return ()
- | _ => return ()
-
-def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
- let mut info ← DefinitionInfo.ofDefinitionVal v
- let some className ← isClass? v.type | panic! s!"isClass? on {v.name} returned none"
- if let some instAttr ← getDefaultInstance v.name className then
- info := { info with attrs := info.attrs.push instAttr }
- let typeNames ← getInstanceTypes v.type
- return {
- toDefinitionInfo := info,
- className,
- typeNames
- }
-
-end DocGen4.Process
diff --git a/DocGen4/Process/NameExt.lean b/DocGen4/Process/NameExt.lean
deleted file mode 100644
index d1be339..0000000
--- a/DocGen4/Process/NameExt.lean
+++ /dev/null
@@ -1,48 +0,0 @@
-/-
-A generalization of `Lean.Name` that includes a file extension.
--/
-import Lean
-
-open Lean Name
-
-inductive Extension where
-| html
-| pdf
-deriving Repr
-
-namespace Extension
-
-def cmp : Extension → Extension → Ordering
- | html, html => Ordering.eq
- | html, _ => Ordering.lt
- | pdf, pdf => Ordering.eq
- | pdf, _ => Ordering.gt
-
-instance : BEq Extension where
- beq e1 e2 :=
- match cmp e1 e2 with
- | Ordering.eq => true
- | _ => false
-
-def toString : Extension → String
- | html => "html"
- | pdf => "pdf"
-
-end Extension
-
-structure NameExt where
- name : Name
- ext : Extension
-
-namespace NameExt
-
-def cmp (n₁ n₂ : NameExt) : Ordering :=
- match Name.cmp n₁.name n₂.name with
- | Ordering.eq => Extension.cmp n₁.ext n₂.ext
- | ord => ord
-
-def getString! : NameExt → String
- | ⟨str _ s, _⟩ => s
- | _ => unreachable!
-
-end NameExt
diff --git a/DocGen4/Process/NameInfo.lean b/DocGen4/Process/NameInfo.lean
deleted file mode 100644
index c827778..0000000
--- a/DocGen4/Process/NameInfo.lean
+++ /dev/null
@@ -1,56 +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 DocGen4.Process.Base
-import DocGen4.Process.Attributes
-
-namespace DocGen4.Process
-open Lean Meta
-
-def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
- let env ← getEnv
- return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n}
-
-partial def argTypeTelescope {α : Type} (e : Expr) (k : Array ((Option Name) × Expr × BinderInfo) → Expr → MetaM α) : MetaM α :=
- go e #[]
-where
- go (e : Expr) (args : Array ((Option Name) × Expr × BinderInfo)) : MetaM α := do
- let helper := fun name type body bi =>
- -- Once we hit a name with a macro scope we stop traversing the expression
- -- and print what is left after the : instead. The only exception
- -- to this is instances since these almost never have a name
- -- but should still be printed as arguments instead of after the :.
- if bi.isInstImplicit && name.hasMacroScopes then
- let arg := (none, type, bi)
- Meta.withLocalDecl name bi type fun fvar => do
- go (Expr.instantiate1 body fvar) (args.push arg)
- else if name.hasMacroScopes then
- k args e
- else
- let arg := (some name, type, bi)
- Meta.withLocalDecl name bi type fun fvar => do
- go (Expr.instantiate1 body fvar) (args.push arg)
- match e.consumeMData with
- | Expr.forallE name type body binderInfo => helper name type body binderInfo
- | _ => k args e
-
-def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
- argTypeTelescope v.type fun args type => do
- let args ← args.mapM (fun (n, e, b) => do return Arg.mk n (← prettyPrintTerm e) b)
- let nameInfo ← NameInfo.ofTypedName v.name type
- match ← findDeclarationRanges? v.name with
- -- TODO: Maybe selection range is more relevant? Figure this out in the future
- | some range =>
- return {
- toNameInfo := nameInfo,
- args,
- declarationRange := range.range,
- attrs := ← getAllAttributes v.name
- }
- | none => panic! s!"{v.name} is a declaration without position"
-
-end DocGen4.Process
diff --git a/DocGen4/Process/OpaqueInfo.lean b/DocGen4/Process/OpaqueInfo.lean
deleted file mode 100644
index d85affa..0000000
--- a/DocGen4/Process/OpaqueInfo.lean
+++ /dev/null
@@ -1,33 +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 DocGen4.Process.Base
-import DocGen4.Process.NameInfo
-
-namespace DocGen4.Process
-
-open Lean Meta
-
-def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
- let info ← Info.ofConstantVal v.toConstantVal
- let value ← prettyPrintTerm v.value
- let env ← getEnv
- let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
- let definitionSafety :=
- if isPartial then
- DefinitionSafety.partial
- else if v.isUnsafe then
- DefinitionSafety.unsafe
- else
- DefinitionSafety.safe
- return {
- toInfo := info,
- value,
- definitionSafety
- }
-
-end DocGen4.Process
diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean
deleted file mode 100644
index aaf32f1..0000000
--- a/DocGen4/Process/StructureInfo.lean
+++ /dev/null
@@ -1,58 +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 DocGen4.Process.Base
-import DocGen4.Process.NameInfo
-
-namespace DocGen4.Process
-
-open Lean Meta
-
-/--
- Execute `k` with an array containing pairs `(fieldName, fieldType)`.
- `k` is executed in an updated local context which contains local declarations for the `structName` parameters.
--/
-def withFields (info : InductiveVal) (k : Array (Name × Expr) → MetaM α) (includeSubobjectFields : Bool := false) : MetaM α := do
- let structName := info.name
- let us := info.levelParams.map mkLevelParam
- forallTelescopeReducing info.type fun params _ =>
- withLocalDeclD `s (mkAppN (mkConst structName us) params) fun s => do
- let mut info := #[]
- for fieldName in getStructureFieldsFlattened (← getEnv) structName includeSubobjectFields do
- let proj ← mkProjection s fieldName
- info := info.push (fieldName, (← inferType proj))
- k info
-
-def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do
- withFields v fun fields =>
- fields.foldlM (init := #[]) (fun acc (name, type) => do return acc.push (← NameInfo.ofTypedName (v.name.append name) type))
-
-def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
- let info ← Info.ofConstantVal v.toConstantVal
- let env ← getEnv
- let parents := getParentStructures env v.name
- let ctorVal := getStructureCtor env v.name
- let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type
- match getStructureInfo? env v.name with
- | some i =>
- if i.fieldNames.size - parents.size > 0 then
- return {
- toInfo := info,
- fieldInfo := ← getFieldTypes v,
- parents,
- ctor
- }
- else
- return {
- toInfo := info,
- fieldInfo := #[],
- parents,
- ctor
- }
- | none => panic! s!"{v.name} is not a structure"
-
-end DocGen4.Process
diff --git a/DocGen4/Process/TheoremInfo.lean b/DocGen4/Process/TheoremInfo.lean
deleted file mode 100644
index e5ce277..0000000
--- a/DocGen4/Process/TheoremInfo.lean
+++ /dev/null
@@ -1,19 +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 DocGen4.Process.Base
-import DocGen4.Process.NameInfo
-
-namespace DocGen4.Process
-
-open Lean Meta
-
-def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
- let info ← Info.ofConstantVal v.toConstantVal
- return { toInfo := info }
-
-end DocGen4.Process
diff --git a/Makefile b/Makefile
deleted file mode 100644
index 309c03a..0000000
--- a/Makefile
+++ /dev/null
@@ -1,14 +0,0 @@
-all:
- @echo "Please specify a build target."
-
-docs:
- -ls build/doc | \
- grep -v -E 'Init|Lean|Mathlib' | \
- xargs -I {} rm -r "build/doc/{}"
- -./scripts/run_pdflatex.sh build > /dev/null
- lake build Bookshelf:docs
-
-docs!:
- -rm -r build/doc
- -./scripts/run_pdflatex.sh build > /dev/null
- lake build Bookshelf:docs
diff --git a/README.md b/README.md
index 3fea8aa..57e4132 100644
--- a/README.md
+++ b/README.md
@@ -13,24 +13,3 @@ feasible, theorems are also formally proven in [Lean](https://leanprover.github.
- [ ] Gustedt, Jens. Modern C. Shelter Island, NY: Manning Publications Co, 2020.
- [ ] Ross, Sheldon. A First Course in Probability Theory. 8th ed. Pearson Prentice Hall, n.d.
- [ ] Smullyan, Raymond M. To Mock a Mockingbird: And Other Logic Puzzles Including an Amazing Adventure in Combinatory Logic. Oxford: Oxford university press, 2000.
-
-## Documentation
-
-This project has absorbed [doc-gen4](https://github.com/leanprover/doc-gen4) to
-ease customization. In particular, the `DocGen4` module found in this project
-allows generating PDFs and including them in the navbar. To generate
-documentation and serve files locally, run the following:
-
-```bash
-> make docs[!]
-> lake run server
-```
-
-The `docs` build target avoids cleaning files that are expected to not change
-often (e.g. `Lean`, `Init`, and `Mathlib` related content). If you've upgraded
-Lean or Mathlib, run `make docs!` instead to generate documentation from
-scratch.
-
-Both assume you have `pdflatex` and `python3` available in your `$PATH`. To
-change how the server behaves, refer to the `.env` file located in the root
-directory of this project.
diff --git a/lake-manifest.json b/lake-manifest.json
index fd3b11e..f777383 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,43 +1,7 @@
{"version": 7,
"packagesDir": ".lake/packages",
"packages":
- [{"url": "https://github.com/mhuisi/lean4-cli",
- "type": "git",
- "subDir": null,
- "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
- "name": "Cli",
- "manifestFile": "lake-manifest.json",
- "inputRev": "nightly",
- "inherited": false,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/xubaiw/CMark.lean",
- "type": "git",
- "subDir": null,
- "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
- "name": "CMark",
- "manifestFile": "lake-manifest.json",
- "inputRev": "main",
- "inherited": false,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/fgdorais/lean4-unicode-basic",
- "type": "git",
- "subDir": null,
- "rev": "dc62b29a26fcc3da545472ab8ad2c98ef3433634",
- "name": "UnicodeBasic",
- "manifestFile": "lake-manifest.json",
- "inputRev": "main",
- "inherited": false,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/hargonix/LeanInk",
- "type": "git",
- "subDir": null,
- "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
- "name": "leanInk",
- "manifestFile": "lake-manifest.json",
- "inputRev": "doc-gen",
- "inherited": false,
- "configFile": "lakefile.lean"},
- {"url": "https://github.com/leanprover/std4.git",
+ [{"url": "https://github.com/leanprover/std4.git",
"type": "git",
"subDir": null,
"rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
@@ -73,6 +37,15 @@
"inputRev": "v0.0.23",
"inherited": true,
"configFile": "lakefile.lean"},
+ {"url": "https://github.com/leanprover/lean4-cli",
+ "type": "git",
+ "subDir": null,
+ "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+ "name": "Cli",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
@@ -81,6 +54,42 @@
"manifestFile": "lake-manifest.json",
"inputRev": "v4.3.0",
"inherited": false,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/xubaiw/CMark.lean",
+ "type": "git",
+ "subDir": null,
+ "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
+ "name": "CMark",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+ "type": "git",
+ "subDir": null,
+ "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
+ "name": "UnicodeBasic",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/hargonix/LeanInk",
+ "type": "git",
+ "subDir": null,
+ "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
+ "name": "leanInk",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "doc-gen",
+ "inherited": true,
+ "configFile": "lakefile.lean"},
+ {"url": "https://github.com/leanprover/doc-gen4",
+ "type": "git",
+ "subDir": null,
+ "rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1",
+ "name": "«doc-gen4»",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "main",
+ "inherited": false,
"configFile": "lakefile.lean"}],
"name": "bookshelf",
"lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index 2c2cad2..39a8fc4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,232 +4,17 @@ open System Lake DSL
package «bookshelf»
--- ========================================
--- Imports
--- ========================================
-
-require Cli from git
- "https://github.com/mhuisi/lean4-cli" @
- "nightly"
-require CMark from git
- "https://github.com/xubaiw/CMark.lean" @
- "main"
-require UnicodeBasic from git
- "https://github.com/fgdorais/lean4-unicode-basic" @
- "main"
-require leanInk from git
- "https://github.com/hargonix/LeanInk" @
- "doc-gen"
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @
"v4.3.0"
require std from git
"https://github.com/leanprover/std4.git" @
"v4.3.0"
-
--- ========================================
--- Documentation Generator
--- ========================================
-
-lean_lib DocGen4
-
-lean_exe «doc-gen4» {
- root := `Main
- supportInterpreter := true
-}
-
-/--
-Turns a Github git remote URL into an HTTPS Github URL.
-Three link types from git supported:
-- https://github.com/org/repo
-- https://github.com/org/repo.git
-- git@github.com:org/repo.git
-TODO: This function is quite brittle and very Github specific, we can
-probably do better.
--/
-def getGithubBaseUrl (gitUrl : String) : String := Id.run do
- let mut url := gitUrl
- if url.startsWith "git@" then
- url := url.drop 15
- url := url.dropRight 4
- return s!"https://github.com/{url}"
- else if url.endsWith ".git" then
- return url.dropRight 4
- else
- return url
-
-/--
-Obtain the Github URL of a project by parsing the origin remote.
--/
-def getProjectGithubUrl (directory : System.FilePath := "." ) : IO String := do
- let out ← IO.Process.output {
- cmd := "git",
- args := #["remote", "get-url", "origin"],
- cwd := directory
- }
- if out.exitCode != 0 then
- throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the git remote in {directory}"
- return out.stdout.trimRight
-
-/--
-Obtain the git commit hash of the project that is currently getting analyzed.
--/
-def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
- let out ← IO.Process.output {
- cmd := "git",
- args := #["rev-parse", "HEAD"]
- cwd := directory
- }
- if out.exitCode != 0 then
- throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the current commit in {directory}"
- return out.stdout.trimRight
-
-def getGitUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
- let baseUrl := getGithubBaseUrl (← getProjectGithubUrl pkg.dir)
- let commit ← getProjectCommit pkg.dir
-
- let parts := mod.name.components.map toString
- let path := String.intercalate "/" parts
- let libPath := pkg.config.srcDir / lib.srcDir
- let basePath := String.intercalate "/" (libPath.components.filter (· != "."))
- let url := s!"{baseUrl}/blob/{commit}/{basePath}/{path}.lean"
- return url
-
-module_facet docs (mod) : FilePath := do
- let some docGen4 ← findLeanExe? `«doc-gen4»
- | error "no doc-gen4 executable configuration found in workspace"
- let exeJob ← docGen4.exe.fetch
- let modJob ← mod.leanArts.fetch
- let ws ← getWorkspace
- let pkg ← ws.packages.find? (·.isLocalModule mod.name)
- let libConfig ← pkg.leanLibConfigs.toArray.find? (·.isLocalModule mod.name)
- -- Build all documentation imported modules
- let imports ← mod.imports.fetch
- let depDocJobs ← BuildJob.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs
- let gitUrl ← getGitUrl pkg libConfig mod
- let buildDir := ws.root.buildDir
- let docFile := mod.filePath (buildDir / "doc") "html"
- depDocJobs.bindAsync fun _ depDocTrace => do
- exeJob.bindAsync fun exeFile exeTrace => do
- modJob.bindSync fun _ modTrace => do
- let depTrace := mixTraceArray #[exeTrace, modTrace, depDocTrace]
- let trace ← buildFileUnlessUpToDate docFile depTrace do
- logStep s!"Documenting module: {mod.name}"
- proc {
- cmd := exeFile.toString
- args := #["single", mod.name.toString, gitUrl]
- env := ← getAugmentedEnv
- }
- return (docFile, trace)
-
--- TODO: technically speaking this facet does not show all file dependencies
-target coreDocs : FilePath := do
- let some docGen4 ← findLeanExe? `«doc-gen4»
- | error "no doc-gen4 executable configuration found in workspace"
- let exeJob ← docGen4.exe.fetch
- let basePath := (←getWorkspace).root.buildDir / "doc"
- let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
- exeJob.bindSync fun exeFile exeTrace => do
- let trace ← buildFileUnlessUpToDate dataFile exeTrace do
- logStep "Documenting Lean core: Init and Lean"
- proc {
- cmd := exeFile.toString
- args := #["genCore"]
- env := ← getAugmentedEnv
- }
- return (dataFile, trace)
-
-library_facet docs (lib) : FilePath := do
- -- Ordering is important. The index file is generated by walking through the
- -- filesystem directory. Files copied from the shell scripts need to exist
- -- prior to this.
- let mods ← lib.modules.fetch
- let moduleJobs ← BuildJob.mixArray <| ← mods.mapM (fetch <| ·.facet `docs)
- let coreJob : BuildJob FilePath ← coreDocs.fetch
- let exeJob ← «doc-gen4».fetch
- -- Shared with DocGen4.Output
- let basePath := (←getWorkspace).root.buildDir / "doc"
- let dataFile := basePath / "declarations" / "declaration-data.bmp"
- let staticFiles := #[
- basePath / "style.css",
- basePath / "declaration-data.js",
- basePath / "color-scheme.js",
- basePath / "nav.js",
- basePath / "jump-src.js",
- basePath / "expand-nav.js",
- basePath / "how-about.js",
- basePath / "search.js",
- basePath / "mathjax-config.js",
- basePath / "instances.js",
- basePath / "importedBy.js",
- basePath / "index.html",
- basePath / "404.html",
- 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"
- ]
- coreJob.bindAsync fun _ coreInputTrace => do
- exeJob.bindAsync fun exeFile exeTrace => do
- moduleJobs.bindSync fun _ inputTrace => do
- let depTrace := mixTraceArray #[inputTrace, exeTrace, coreInputTrace]
- let trace ← buildFileUnlessUpToDate dataFile depTrace do
- logInfo "Documentation indexing"
- proc {
- cmd := exeFile.toString
- args := #["index"]
- }
- let traces ← staticFiles.mapM computeTrace
- let indexTrace := mixTraceArray traces
-
- return (dataFile, trace.mix indexTrace)
-
--- ========================================
--- Bookshelf
--- ========================================
+meta if get_config? env = some "dev" then
+ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @
+ "main"
@[default_target]
lean_lib «Bookshelf» {
roots := #[`Bookshelf, `Common]
}
-
-/--
-The contents of our `.env` file.
--/
-structure Config where
- port : Nat := 5555
-
-/--
-Read in the `.env` file into an in-memory structure.
--/
-private def readConfig : StateT Config ScriptM Unit := do
- let env <- IO.FS.readFile ".env"
- for line in env.trim.split (fun c => c == '\n') do
- match line.split (fun c => c == '=') with
- | ["PORT", port] => modify (fun c => { c with port := String.toNat! port })
- | _ => error "Malformed `.env` file."
- return ()
-
-/--
-Start an HTTP server for locally serving documentation. It is expected the
-documentation has already been generated prior via
-
-```bash
-> lake build Bookshelf:docs
-```
-
-USAGE:
- lake run server
--/
-script server (_args) do
- let ((), config) <- StateT.run readConfig {}
- IO.println s!"Running Lean on `http://localhost:{config.port}`"
- _ <- IO.Process.run {
- cmd := "python3",
- args := #["-m", "http.server", toString config.port, "-d", "build/doc"],
- }
- return 0
diff --git a/scripts/run_pdflatex.sh b/scripts/run_pdflatex.sh
deleted file mode 100755
index 5911bf6..0000000
--- a/scripts/run_pdflatex.sh
+++ /dev/null
@@ -1,26 +0,0 @@
-#!/usr/bin/env bash
-
-if ! command -v pdflatex > /dev/null; then
- >&2 echo 'pdflatex was not found in the current $PATH.'
- exit 1
-fi
-
-BUILD_DIR="$1"
-
-function process_file () {
- REL_DIR=$(dirname "$1")
- REL_BASE=$(basename -s ".tex" "$1")
- mkdir -p "$BUILD_DIR/doc/$REL_DIR"
- (cd "$REL_DIR" && pdflatex "$REL_BASE.tex")
- cp "$REL_DIR/$REL_BASE.pdf" "$BUILD_DIR/doc/$REL_DIR/"
-}
-
-export BUILD_DIR
-export -f process_file
-
-# We run this command twice to allow any cross-references to resolve correctly.
-# https://tex.stackexchange.com/questions/41539/does-hyperref-work-between-two-files
-for _ in {1..2}; do
- find ./* \( -path build -o -path lake-packages \) -prune -o -name "*.tex" -print0 \
- | xargs -0 -I{} bash -c "process_file {}"
-done
diff --git a/static/alectryon/alectryon.css b/static/alectryon/alectryon.css
deleted file mode 100644
index 67988e3..0000000
--- 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 6a469d0..0000000
--- 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 75d0615..0000000
--- 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 d7b9245..0000000
--- 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 */
diff --git a/static/color-scheme.js b/static/color-scheme.js
deleted file mode 100644
index 5b061ee..0000000
--- a/static/color-scheme.js
+++ /dev/null
@@ -1,33 +0,0 @@
-function getTheme() {
- return localStorage.getItem("theme") || "system";
-}
-
-function setTheme(themeName) {
- localStorage.setItem('theme', themeName);
- if (themeName == "system") {
- themeName = parent.matchMedia("(prefers-color-scheme: dark)").matches ? "dark" : "light";
- }
- // the navbar is in an iframe, so we need to set this variable in the parent document
- for (const win of [window, parent]) {
- win.document.documentElement.setAttribute('data-theme', themeName);
- }
-}
-
-setTheme(getTheme())
-
-document.addEventListener("DOMContentLoaded", function() {
- document.querySelectorAll("#color-theme-switcher input").forEach((input) => {
- if (input.value == getTheme()) {
- input.checked = true;
- }
- input.addEventListener('change', e => setTheme(e.target.value));
- });
-
- // also check to see if the user changes their theme settings while the page is loaded.
- parent.matchMedia('(prefers-color-scheme: dark)').addEventListener('change', event => {
- setTheme(getTheme());
- })
-});
-
-// un-hide the colorscheme picker
-document.querySelector("#settings").removeAttribute('hidden');
\ No newline at end of file
diff --git a/static/declaration-data.js b/static/declaration-data.js
deleted file mode 100644
index a20c494..0000000
--- a/static/declaration-data.js
+++ /dev/null
@@ -1,272 +0,0 @@
-/**
- * This module is a wrapper that facilitates manipulating the declaration data.
- *
- * Please see {@link DeclarationDataCenter} for more information.
- */
-
-const CACHE_DB_NAME = "declaration-data";
-const CACHE_DB_VERSION = 1;
-const CACHE_DB_KEY = "DECLARATIONS_KEY";
-
-/**
- * The DeclarationDataCenter is used for declaration searching.
- *
- * For usage, see the {@link init} and {@link search} methods.
- */
-export class DeclarationDataCenter {
- /**
- * The declaration data. Users should not interact directly with this field.
- *
- * *NOTE:* This is not made private to support legacy browsers.
- */
- declarationData = null;
-
- /**
- * Used to implement the singleton, in case we need to fetch data mutiple times in the same page.
- */
- static requestSingleton = null;
-
- /**
- * Construct a DeclarationDataCenter with given data.
- *
- * Please use {@link DeclarationDataCenter.init} instead, which automates the data fetching process.
- * @param {*} declarationData
- */
- constructor(declarationData) {
- this.declarationData = declarationData;
- }
-
- /**
- * The actual constructor of DeclarationDataCenter
- * @returns {Promise}
- */
- static async init() {
- if (DeclarationDataCenter.requestSingleton === null) {
- DeclarationDataCenter.requestSingleton = DeclarationDataCenter.getData();
- }
- return await DeclarationDataCenter.requestSingleton;
- }
-
- static async getData() {
- const dataListUrl = new URL(
- `${SITE_ROOT}/declarations/declaration-data.bmp`,
- window.location
- );
-
- // try to use cache first
- // TODO: This API is not thought 100% through. If we have a DB cached
- // already it will not even ask the remote for a new one so we end up
- // with outdated declaration-data. This has to have some form of cache
- // invalidation: https://github.com/leanprover/doc-gen4/issues/133
- // const data = await fetchCachedDeclarationData().catch(_e => null);
- const data = null;
- if (data) {
- // if data is defined, use the cached one.
- return new DeclarationDataCenter(data);
- } else {
- // undefined. then fetch the data from the server.
- const dataListRes = await fetch(dataListUrl);
- const data = await dataListRes.json();
- // TODO https://github.com/leanprover/doc-gen4/issues/133
- // await cacheDeclarationData(data);
- return new DeclarationDataCenter(data);
- }
- }
-
- /**
- * Search for a declaration.
- * @returns {Array}
- */
- search(pattern, strict = true, allowedKinds = undefined, maxResults = undefined) {
- if (!pattern) {
- return [];
- }
- if (strict) {
- let decl = this.declarationData.declarations[pattern];
- return decl ? [decl] : [];
- } else {
- return getMatches(this.declarationData.declarations, pattern, allowedKinds, maxResults);
- }
- }
-
- /**
- * Search for all instances of a certain typeclass
- * @returns {Array}
- */
- instancesForClass(className) {
- const instances = this.declarationData.instances[className];
- if (!instances) {
- return [];
- } else {
- return instances;
- }
- }
-
- /**
- * Search for all instances that involve a certain type
- * @returns {Array}
- */
- instancesForType(typeName) {
- const instances = this.declarationData.instancesFor[typeName];
- if (!instances) {
- return [];
- } else {
- return instances;
- }
- }
-
- /**
- * Analogous to Lean declNameToLink
- * @returns {String}
- */
- declNameToLink(declName) {
- return this.declarationData.declarations[declName].docLink;
- }
-
- /**
- * Find all modules that imported the given one.
- * @returns {Array}
- */
- moduleImportedBy(moduleName) {
- return this.declarationData.modules[moduleName].importedBy;
- }
-
- /**
- * Analogous to Lean moduleNameToLink
- * @returns {String}
- */
- moduleNameToLink(moduleName) {
- return this.declarationData.modules[moduleName].url;
- }
-}
-
-function isSeparator(char) {
- return char === "." || char === "_";
-}
-
-// HACK: the fuzzy matching is quite hacky
-
-function matchCaseSensitive(declName, lowerDeclName, pattern) {
- let i = 0,
- j = 0,
- err = 0,
- lastMatch = 0;
- while (i < declName.length && j < pattern.length) {
- if (pattern[j] === declName[i] || pattern[j] === lowerDeclName[i]) {
- err += (isSeparator(pattern[j]) ? 0.125 : 1) * (i - lastMatch);
- if (pattern[j] !== declName[i]) err += 0.5;
- lastMatch = i + 1;
- j++;
- } else if (isSeparator(declName[i])) {
- err += 0.125 * (i + 1 - lastMatch);
- lastMatch = i + 1;
- }
- i++;
- }
- err += 0.125 * (declName.length - lastMatch);
- if (j === pattern.length) {
- return err;
- }
-}
-
-function getMatches(declarations, pattern, allowedKinds = undefined, maxResults = undefined) {
- const lowerPats = pattern.toLowerCase().split(/\s/g);
- const patNoSpaces = pattern.replace(/\s/g, "");
- const results = [];
- for (const [name, {
- kind,
- docLink,
- }] of Object.entries(declarations)) {
- // Apply "kind" filter
- if (allowedKinds !== undefined) {
- if (!allowedKinds.has(kind)) {
- continue;
- }
- }
- const lowerName = name.toLowerCase();
- let err = matchCaseSensitive(name, lowerName, patNoSpaces);
- if (err !== undefined) {
- results.push({
- name,
- kind,
- err,
- lowerName,
- docLink,
- });
- }
- }
- return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults);
-}
-
-// TODO: refactor the indexedDB part to be more robust
-
-/**
- * Get the indexedDB database, automatically initialized.
- * @returns {Promise}
- */
-async function getDeclarationDatabase() {
- return new Promise((resolve, reject) => {
- const request = indexedDB.open(CACHE_DB_NAME, CACHE_DB_VERSION);
-
- request.onerror = function (event) {
- reject(
- new Error(
- `fail to open indexedDB ${CACHE_DB_NAME} of version ${CACHE_DB_VERSION}`
- )
- );
- };
- request.onupgradeneeded = function (event) {
- let db = event.target.result;
- // We only need to store one object, so no key path or increment is needed.
- db.createObjectStore("declaration");
- };
- request.onsuccess = function (event) {
- resolve(event.target.result);
- };
- });
-}
-
-/**
- * Store data in indexedDB object store.
- * @param {Map} data
- */
-async function cacheDeclarationData(data) {
- let db = await getDeclarationDatabase();
- let store = db
- .transaction("declaration", "readwrite")
- .objectStore("declaration");
- return new Promise((resolve, reject) => {
- let clearRequest = store.clear();
- let addRequest = store.add(data, CACHE_DB_KEY);
-
- addRequest.onsuccess = function (event) {
- resolve();
- };
- addRequest.onerror = function (event) {
- reject(new Error(`fail to store declaration data`));
- };
- clearRequest.onerror = function (event) {
- reject(new Error("fail to clear object store"));
- };
- });
-}
-
-/**
- * Retrieve data from indexedDB database.
- * @returns {Promise|undefined>}
- */
-async function fetchCachedDeclarationData() {
- let db = await getDeclarationDatabase();
- let store = db
- .transaction("declaration", "readonly")
- .objectStore("declaration");
- return new Promise((resolve, reject) => {
- let transactionRequest = store.get(CACHE_DB_KEY);
- transactionRequest.onsuccess = function (event) {
- resolve(event.target.result);
- };
- transactionRequest.onerror = function (event) {
- reject(new Error(`fail to store declaration data`));
- };
- });
-}
diff --git a/static/expand-nav.js b/static/expand-nav.js
deleted file mode 100644
index 6ecb246..0000000
--- a/static/expand-nav.js
+++ /dev/null
@@ -1,24 +0,0 @@
-document.querySelector('.navframe').addEventListener('load', function() {
- // Get the current page URL without the suffix after #
- var currentPageURL = window.location.href.split('#')[0];
-
- // Get all anchor tags
- var as = document.querySelector('.navframe').contentWindow.document.body.querySelectorAll('a');
- for (const a of as) {
- if (a.href) {
- var href = a.href.split('#')[0];
- // find the one with the current url
- if (href === currentPageURL) {
- a.style.fontStyle = 'italic';
- // open all detail tags above the current
- var el = a.parentNode.closest('details');
- while (el) {
- el.open = true;
- el = el.parentNode.closest('details');
- }
- }
- // seeing as we found the link we were looking for, stop
- break;
- }
- }
-});
\ No newline at end of file
diff --git a/static/find/find.js b/static/find/find.js
deleted file mode 100644
index 57953fc..0000000
--- a/static/find/find.js
+++ /dev/null
@@ -1,94 +0,0 @@
-/**
- * This module is used for the `/find` endpoint.
- *
- * Two basic kinds of search syntax are supported:
- *
- * 1. Query-Fragment syntax: `/find?pattern=Nat.add#doc` for documentation and `/find?pattern=Nat.add#src` for source code.
- * 2. Fragment-Only syntax:`/find/#doc/Nat.add` for documentation and `/find/#src/Nat.add` for source code.
- *
- * Though both of them are valid, the first one is highly recommended, and the second one is for compatibility and taste.
- *
- * There are some extended usage for the QF syntax. For example, appending `strict=false` to the query part
- * (`/find?pattern=Nat.add&strict=false#doc`) will allow you to use the fuzzy search, rather than strict match.
- * Also, the fragment is extensible as well. For now only `#doc` and `#src` are implement, and the plain query without
- * hash (`/find?pattern=Nat.add`) is used for computer-friendly data (semantic web is great! :P), while all other fragments
- * fallback to the `#doc` view.
- */
-
-import { DeclarationDataCenter } from "../declaration-data.js";
-
-function leanFriendlyRegExp(c) {
- try {
- return new RegExp("(? p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR))
- ?.filter((l) => l.length == 2 && l[0].length > 0)
-);
-const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? [];
-
-const encodedPattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined
-const pattern = encodedPattern && decodeURIComponent(encodedPattern);
-const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true
-const view = fragmentPaths[0];
-
-findAndRedirect(pattern, strict, view);
-
-/**
- * Find the result and redirect to the result page.
- * @param {string} pattern the pattern to search for
- * @param {string} view the view of the find result (`"doc"` or `"src"` for now)
- */
-async function findAndRedirect(pattern, strict, view) {
- // if no pattern provided, directly redirect to the 404 page
- if (!pattern) {
- window.location.replace(`${SITE_ROOT}404.html`);
- }
- // search for result
- try {
- const dataCenter = await DeclarationDataCenter.init();
- let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array
- // if no result found, redirect to the 404 page
- if (!result) {
- // TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found.
- window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`);
- } else {
- result.docLink = SITE_ROOT + result.docLink;
- // success, redirect to doc or source page, or to the semantic rdf.
- if (!view) {
- window.location.replace(result.link);
- } else if (view == "doc") {
- window.location.replace(result.docLink);
- } else if (view == "src") {
- const [module, decl] = result.docLink.split("#", 2);
- window.location.replace(`${module}?jump=src#${decl}`);
- } else {
- // fallback to doc page
- window.location.replace(result.docLink);
- }
- }
- } catch (e) {
- document.write(`Cannot fetch data, please check your network connection.\n${e}`);
- }
-}
diff --git a/static/how-about.js b/static/how-about.js
deleted file mode 100644
index 5c03ffd..0000000
--- a/static/how-about.js
+++ /dev/null
@@ -1,39 +0,0 @@
-/**
- * This module implements the `howabout` functionality in the 404 page.
- */
-
-import { DeclarationDataCenter } from "./declaration-data.js";
-
-const HOW_ABOUT = document.querySelector("#howabout");
-
-// Show url of the missing page
-if (HOW_ABOUT) {
- HOW_ABOUT.parentNode
- .insertBefore(document.createElement("pre"), HOW_ABOUT)
- .appendChild(document.createElement("code")).innerText =
- window.location.href.replace(/[/]/g, "/\u200b");
-
- // TODO: add how about functionality for similar page as well.
- const pattern = window.location.hash.replace("#", "");
-
- // try to search for similar declarations
- if (pattern) {
- HOW_ABOUT.innerText = "Please wait a second. I'll try to help you.";
- DeclarationDataCenter.init().then((dataCenter) => {
- let results = dataCenter.search(pattern, false);
- if (results.length > 0) {
- HOW_ABOUT.innerText = "How about one of these instead:";
- const ul = HOW_ABOUT.appendChild(document.createElement("ul"));
- for (const { name, docLink } of results) {
- const li = ul.appendChild(document.createElement("li"));
- const a = li.appendChild(document.createElement("a"));
- a.href = docLink;
- a.appendChild(document.createElement("code")).innerText = name;
- }
- } else {
- HOW_ABOUT.innerText =
- "Sorry, I cannot find any similar declarations. Check the link or use the module navigation to find what you want :P";
- }
- });
- }
-}
diff --git a/static/importedBy.js b/static/importedBy.js
deleted file mode 100644
index 5eb7fca..0000000
--- a/static/importedBy.js
+++ /dev/null
@@ -1,19 +0,0 @@
-import { DeclarationDataCenter } from "./declaration-data.js";
-
-fillImportedBy();
-
-async function fillImportedBy() {
- if (typeof(MODULE_NAME) == "undefined") {
- return;
- }
- const dataCenter = await DeclarationDataCenter.init();
- const moduleName = MODULE_NAME;
- const importedByList = document.querySelector(".imported-by-list");
- const importedBy = dataCenter.moduleImportedBy(moduleName);
- var innerHTML = "";
- for(var module of importedBy) {
- const moduleLink = dataCenter.moduleNameToLink(module);
- innerHTML += `${module} `
- }
- importedByList.innerHTML = innerHTML;
-}
diff --git a/static/instances.js b/static/instances.js
deleted file mode 100644
index 9389a29..0000000
--- a/static/instances.js
+++ /dev/null
@@ -1,41 +0,0 @@
-import { DeclarationDataCenter } from "./declaration-data.js";
-
-annotateInstances();
-annotateInstancesFor()
-
-async function annotateInstances() {
- const dataCenter = await DeclarationDataCenter.init();
- const instanceForLists = [...(document.querySelectorAll(".instances-list"))];
-
- for (const instanceForList of instanceForLists) {
- const className = instanceForList.id.slice("instances-list-".length);
- const instances = dataCenter.instancesForClass(className);
- var innerHTML = "";
- for(var instance of instances) {
- const instanceLink = dataCenter.declNameToLink(instance);
- innerHTML += `${instance} `
- }
- instanceForList.innerHTML = innerHTML;
- }
-}
-
-async function annotateInstancesFor() {
- const dataCenter = await DeclarationDataCenter.init();
- const instanceForLists = [...(document.querySelectorAll(".instances-for-list"))];
-
- for (const instanceForList of instanceForLists) {
- const typeName = instanceForList.id.slice("instances-for-list-".length);
- const instances = dataCenter.instancesForType(typeName);
- if (instances.length == 0) {
- instanceForList.remove();
- } else {
- var innerHTML = "";
- for(var instance of instances) {
- const instanceLink = dataCenter.declNameToLink(instance);
- innerHTML += `${instance} `;
- }
- const instanceEnum = instanceForList.querySelector(".instances-for-enum");
- instanceEnum.innerHTML = innerHTML;
- }
- }
-}
diff --git a/static/jump-src.js b/static/jump-src.js
deleted file mode 100644
index e7397e5..0000000
--- a/static/jump-src.js
+++ /dev/null
@@ -1,10 +0,0 @@
-document.addEventListener("DOMContentLoaded", () => {
- const hash = document.location.hash.substring(1);
- const tgt = new URLSearchParams(document.location.search).get("jump");
- if (tgt === "src" && hash) {
- const target = document.getElementById(hash)
- ?.querySelector(".gh_link a")
- ?.getAttribute("href");
- if (target) window.location.replace(target);
- }
-})
\ No newline at end of file
diff --git a/static/mathjax-config.js b/static/mathjax-config.js
deleted file mode 100644
index 076dbf6..0000000
--- a/static/mathjax-config.js
+++ /dev/null
@@ -1,41 +0,0 @@
-/*
- * This file is for configing MathJax behavior.
- * See https://docs.mathjax.org/en/latest/web/configuration.html
- *
- * This configuration is copied from old doc-gen3
- * https://github.com/leanprover-community/doc-gen
- */
-MathJax = {
- tex: {
- inlineMath: [["$", "$"]],
- displayMath: [["$$", "$$"]],
- },
- options: {
- skipHtmlTags: [
- "script",
- "noscript",
- "style",
- "textarea",
- "pre",
- "code",
- "annotation",
- "annotation-xml",
- "decl",
- "decl_meta",
- "attributes",
- "decl_args",
- "decl_header",
- "decl_name",
- "decl_type",
- "equation",
- "equations",
- "structure_field",
- "structure_fields",
- "constructor",
- "constructors",
- "instances",
- ],
- ignoreHtmlClass: "tex2jax_ignore",
- processHtmlClass: "tex2jax_process",
- },
-};
diff --git a/static/nav.js b/static/nav.js
deleted file mode 100644
index ff8404e..0000000
--- a/static/nav.js
+++ /dev/null
@@ -1,43 +0,0 @@
-/**
- * This module is used to implement persistent navbar expansion.
- */
-
-// The variable to store the expansion information.
-let expanded = {};
-
-// Load expansion information from sessionStorage.
-for (const e of (sessionStorage.getItem("expanded") || "").split(",")) {
- if (e !== "") {
- expanded[e] = true;
- }
-}
-
-/**
- * Save expansion information to sessionStorage.
- */
-function saveExpanded() {
- sessionStorage.setItem(
- "expanded",
- Object.getOwnPropertyNames(expanded)
- .filter((e) => expanded[e])
- .join(",")
- );
-}
-
-// save expansion information when user change the expansion.
-for (const elem of document.getElementsByClassName("nav_sect")) {
- const id = elem.getAttribute("data-path");
- if (!id) continue;
- if (expanded[id]) {
- elem.open = true;
- }
- elem.addEventListener("toggle", () => {
- expanded[id] = elem.open;
- saveExpanded();
- });
-}
-
-// Scroll to center.
-for (const currentFileLink of document.getElementsByClassName("visible")) {
- currentFileLink.scrollIntoView({ block: "center" });
-}
\ No newline at end of file
diff --git a/static/search.js b/static/search.js
deleted file mode 100644
index 4556c64..0000000
--- a/static/search.js
+++ /dev/null
@@ -1,164 +0,0 @@
-/**
- * This module is used to handle user's interaction with the search form.
- */
-
-import { DeclarationDataCenter } from "./declaration-data.js";
-
-// Search form and input in the upper right toolbar
-const SEARCH_FORM = document.querySelector("#search_form");
-const SEARCH_INPUT = SEARCH_FORM.querySelector("input[name=q]");
-
-// Search form on the /search.html_page. These may be null.
-const SEARCH_PAGE_INPUT = document.querySelector("#search_page_query")
-const SEARCH_RESULTS = document.querySelector("#search_results")
-
-// Max results to show for autocomplete or /search.html page.
-const AC_MAX_RESULTS = 30
-const SEARCH_PAGE_MAX_RESULTS = undefined
-
-// Create an `div#autocomplete_results` to hold all autocomplete results.
-let ac_results = document.createElement("div");
-ac_results.id = "autocomplete_results";
-SEARCH_FORM.appendChild(ac_results);
-
-/**
- * Attach `selected` class to the the selected autocomplete result.
- */
-function handleSearchCursorUpDown(down) {
- const sel = ac_results.querySelector(`.selected`);
- if (sel) {
- sel.classList.remove("selected");
- const toSelect = down
- ? sel.nextSibling
- : sel.previousSibling;
- toSelect && toSelect.classList.add("selected");
- } else {
- const toSelect = down ? ac_results.firstChild : ac_results.lastChild;
- toSelect && toSelect.classList.add("selected");
- }
-}
-
-/**
- * Perform search (when enter is pressed).
- */
-function handleSearchEnter() {
- const sel = ac_results.querySelector(`.selected .result_link a`) || document.querySelector(`#search_button`);
- sel.click();
-}
-
-/**
- * Allow user to navigate autocomplete results with up/down arrow keys, and choose with enter.
- */
-SEARCH_INPUT.addEventListener("keydown", (ev) => {
- switch (ev.key) {
- case "Down":
- case "ArrowDown":
- ev.preventDefault();
- handleSearchCursorUpDown(true);
- break;
- case "Up":
- case "ArrowUp":
- ev.preventDefault();
- handleSearchCursorUpDown(false);
- break;
- case "Enter":
- ev.preventDefault();
- handleSearchEnter();
- break;
- }
-});
-
-/**
- * Remove all children of a DOM node.
- */
-function removeAllChildren(node) {
- while (node.firstChild) {
- node.removeChild(node.lastChild);
- }
-}
-
-/**
- * Handle user input and perform search.
- */
-function handleSearch(dataCenter, err, ev, sr, maxResults, autocomplete) {
- const text = ev.target.value;
-
- // If no input clear all.
- if (!text) {
- sr.removeAttribute("state");
- removeAllChildren(sr);
- return;
- }
-
- // searching
- sr.setAttribute("state", "loading");
-
- if (dataCenter) {
- var allowedKinds;
- if (!autocomplete) {
- allowedKinds = new Set();
- document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
- {
- if (checkbox.checked) {
- allowedKinds.add(checkbox.value);
- }
- }
- );
- }
- const result = dataCenter.search(text, false, allowedKinds, maxResults);
-
- // in case user has updated the input.
- if (ev.target.value != text) return;
-
- // update autocomplete results
- removeAllChildren(sr);
- for (const { name, kind, docLink } of result) {
- const row = sr.appendChild(document.createElement("div"));
- row.classList.add("search_result")
- const linkdiv = row.appendChild(document.createElement("div"))
- linkdiv.classList.add("result_link")
- const link = linkdiv.appendChild(document.createElement("a"));
- link.innerText = name;
- link.title = name;
- link.href = SITE_ROOT + docLink;
- }
- }
- // handle error
- else {
- removeAllChildren(sr);
- const d = sr.appendChild(document.createElement("a"));
- d.innerText = `Cannot fetch data, please check your network connection.\n${err}`;
- }
- sr.setAttribute("state", "done");
-}
-
-// https://www.joshwcomeau.com/snippets/javascript/debounce/
-const debounce = (callback, wait) => {
- let timeoutId = null;
- return (...args) => {
- window.clearTimeout(timeoutId);
- timeoutId = window.setTimeout(() => {
- callback.apply(null, args);
- }, wait);
- };
-}
-
-DeclarationDataCenter.init()
- .then((dataCenter) => {
- // Search autocompletion.
- SEARCH_INPUT.addEventListener("input", debounce(ev => handleSearch(dataCenter, null, ev, ac_results, AC_MAX_RESULTS, true), 300));
- if(SEARCH_PAGE_INPUT) {
- SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(dataCenter, null, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false))
- document.querySelectorAll(".kind_checkbox").forEach((checkbox) =>
- checkbox.addEventListener("input", ev => SEARCH_PAGE_INPUT.dispatchEvent(new Event("input")))
- );
- SEARCH_PAGE_INPUT.dispatchEvent(new Event("input"))
- };
- SEARCH_INPUT.dispatchEvent(new Event("input"))
- })
- .catch(e => {
- SEARCH_INPUT.addEventListener("input", debounce(ev => handleSearch(null, e, ev, ac_results, AC_MAX_RESULTS, true), 300));
- if(SEARCH_PAGE_INPUT) {
- SEARCH_PAGE_INPUT.addEventListener("input", ev => handleSearch(null, e, ev, SEARCH_RESULTS, SEARCH_PAGE_MAX_RESULTS, false));
- }
- });
diff --git a/static/site-root.js b/static/site-root.js
deleted file mode 100644
index 3dd39a3..0000000
--- a/static/site-root.js
+++ /dev/null
@@ -1,4 +0,0 @@
-/**
- * Get the site root, {siteRoot} is to be replaced by doc-gen4.
- */
-export const SITE_ROOT = "{siteRoot}";
\ No newline at end of file
diff --git a/static/style.css b/static/style.css
deleted file mode 100644
index 4c6b2f8..0000000
--- a/static/style.css
+++ /dev/null
@@ -1,825 +0,0 @@
-@import url('https://cdnjs.cloudflare.com/ajax/libs/lato-font/3.0.0/css/lato-font.min.css');
-@import url('https://cdnjs.cloudflare.com/ajax/libs/juliamono/0.051/juliamono.css');
-
-* {
- box-sizing: border-box;
-}
-
-body {
- font-size: 17px;
- font-variant-ligatures: none;
- font-family: 'Lato Medium';
- color: var(--text-color);
- background: var(--body-bg);
-}
-
-input, select, textarea, button{font-family:inherit;}
-
-a {
- color: var(--link-color);
-}
-
-a.pdf {
- color: var(--link-pdf-color);
-}
-
-h1, h2, h3, h4, h5, h6 {
- font-family: 'Lato Medium';
- font-size: 17px;
-}
-
-body { line-height: 1.5; }
-nav { line-height: normal; }
-
-:root {
- --header-height: 3em;
- --fragment-offset: calc(var(--header-height) + 1em);
- --content-width: 55vw;
-
- --header-bg: #f8f8f8;
- --body-bg: white;
- --code-bg: #f3f3f3;
- --text-color: black;
- --link-color: hsl(210, 100%, 30%);
- --link-pdf-color: hsl(272, 61%, 34%);
-
- --implicit-arg-text-color: var(--text-color);
-
- --def-color: #92dce5;
- --def-color-hsl-angle: 187;
- --theorem-color: #8fe388;
- --theorem-color-hsl-angle: 115;
- --axiom-and-constant-color: #f44708;
- --axiom-and-constant-color-hsl-angle: 16;
- --structure-and-inductive-color: #f0a202;
- --structure-and-inductive-color-hsl-angle: 40;
- --starting-percentage: 100;
-
- --hamburger-bg-color: #eee;
- --hamburger-active-color: white;
- --hamburger-border-color: #ccc;
-
- --tags-border-color: #555;
-
- --fragment-offset: calc(var(--header-height) + 1em);
- --content-width: 55vw;
-}
-/* automatic dark theme if no javascript */
-@media (prefers-color-scheme: dark) {
- :root {
- --header-bg: #111010;
- --body-bg: #171717;
- --code-bg: #363333;
- --text-color: #eee;
- --link-color: #58a6ff;
- --link-pdf-color: #9d58fd;
-
- --implicit-arg-text-color: var(--text-color);
-
- --def-color: #1F497F;
- --def-color-hsl-angle: 214;
- --theorem-color: #134E2D;
- --theorem-color-hsl-angle: 146;
- --axiom-and-constant-color: #6B1B1A;
- --axiom-and-constant-color-hsl-angle: 1;
- --structure-and-inductive-color: #73461C;
- --structure-and-inductive-color-hsl-angle: 29;
- --starting-percentage: 30;
-
- --hamburger-bg-color: #2d2c2c;
- --hamburger-active-color: black;
- --hamburger-border-color: #717171;
-
- --tags-border-color: #AAA;
- }
-}
-
-[data-theme="light"] {
- color-scheme: light;
-
- --header-height: 3em;
- --fragment-offset: calc(var(--header-height) + 1em);
- --content-width: 55vw;
-
- --header-bg: #f8f8f8;
- --body-bg: white;
- --code-bg: #f3f3f3;
- --text-color: black;
- --link-color: hsl(210, 100%, 30%);
- --link-pdf-color: hsl(272, 61%, 34%);
-
- --implicit-arg-text-color: var(--text-color);
-
- --def-color: #92dce5;
- --def-color-hsl-angle: 187;
- --theorem-color: #8fe388;
- --theorem-color-hsl-angle: 115;
- --axiom-and-constant-color: #f44708;
- --axiom-and-constant-color-hsl-angle: 16;
- --structure-and-inductive-color: #f0a202;
- --structure-and-inductive-color-hsl-angle: 40;
- --starting-percentage: 100;
-
- --hamburger-bg-color: #eee;
- --hamburger-active-color: white;
- --hamburger-border-color: #ccc;
-
- --tags-border-color: #555;
-
- --fragment-offset: calc(var(--header-height) + 1em);
- --content-width: 55vw;
-}
-
-[data-theme="dark"] {
- color-scheme: dark;
-
- --header-bg: #111010;
- --body-bg: #171717;
- --code-bg: #363333;
- --text-color: #eee;
- --link-color: #58a6ff;
- --link-pdf-color: #9d58fd;
-
- --implicit-arg-text-color: var(--text-color);
-
- --def-color: #1F497F;
- --def-color-hsl-angle: 214;
- --theorem-color: #134E2D;
- --theorem-color-hsl-angle: 146;
- --axiom-and-constant-color: #6B1B1A;
- --axiom-and-constant-color-hsl-angle: 1;
- --structure-and-inductive-color: #73461C;
- --structure-and-inductive-color-hsl-angle: 29;
- --starting-percentage: 30;
-
- --hamburger-bg-color: #2d2c2c;
- --hamburger-active-color: black;
- --hamburger-border-color: #717171;
-
- --tags-border-color: #AAA;
-}
-
-@supports (width: min(10px, 5vw)) {
- :root {
- --content-width: clamp(20em, 55vw, 60em);
- }
-}
-
-#nav_toggle {
- display: none;
-}
-label[for="nav_toggle"] {
- display: none;
-}
-
-header {
- height: var(--header-height);
- float: left;
- position: fixed;
- width: 100vw;
- max-width: 100%;
- left: 0;
- right: 0;
- top: 0;
- --header-side-padding: 2em;
- padding: 0 var(--header-side-padding);
- background: var(--header-bg);
- z-index: 1;
- display: flex;
- align-items: center;
- justify-content: space-between;
-}
-@supports (width: min(10px, 5vw)) {
- header {
- --header-side-padding: calc(max(2em, (100vw - var(--content-width) - 30em) / 2));
- }
-}
-@media screen and (max-width: 1000px) {
- :root {
- --content-width: 100vw;
- }
-
- .internal_nav {
- display: none;
- }
-
- body .nav {
- width: 100vw;
- max-width: 100vw;
- margin-left: 1em;
- z-index: 1;
- }
-
- body main {
- width: unset;
- max-width: unset;
- margin-left: unset;
- margin-right: unset;
- }
- body .decl > div {
- overflow-x: unset;
- }
-
- #nav_toggle:not(:checked) ~ .nav {
- display: none;
- }
- #nav_toggle:checked ~ main {
- visibility: hidden;
- }
-
- label[for="nav_toggle"]::before {
- content: '≡';
- }
- label[for="nav_toggle"] {
- display: inline-block;
- margin-right: 1em;
- border: 1px solid var(--hamburger-border-color);
- padding: 0.5ex 1ex;
- cursor: pointer;
- background: var(--hamburger-bg-color);
- }
- #nav_toggle:checked ~ * label[for="nav_toggle"] {
- background: var(--hamburger-active-color);
- }
-
- body header h1 {
- font-size: 100%;
- }
-
- header {
- --header-side-padding: 1ex;
- }
-}
-@media screen and (max-width: 700px) {
- header h1 span { display: none; }
- :root { --header-side-padding: 1ex; }
- #search_form button { display: none; }
- #search_form input { width: 100%; }
- header #autocomplete_results {
- left: 1ex;
- right: 1ex;
- width: inherit;
- }
- body header > * { margin: 0; }
-}
-
-header > * {
- display: inline-block;
- padding: 0;
- margin: 0 1em;
- vertical-align: middle;
-}
-
-header h1 {
- font-weight: normal;
- font-size: 160%;
-}
-
-header header_filename {
- font-size: 150%;
-}
-@media (max-width: 80em) {
- .header .header_filename {
- display: none;
- }
-}
-
-/* inserted by nav.js */
-#autocomplete_results {
- position: absolute;
- top: var(--header-height);
- right: calc(var(--header-side-padding));
- width: calc(20em + 4em);
- z-index: 1;
- background: var(--header-bg);
- border: 1px solid #aaa;
- border-top: none;
- overflow-x: hidden;
- overflow-y: auto;
- max-height: calc(100vh - var(--header-height));
-}
-
-#autocomplete_results:empty {
- display: none;
-}
-
-#autocomplete_results[state="loading"]:empty {
- display: block;
- cursor: progress;
-}
-#autocomplete_results[state="loading"]:empty::before {
- display: block;
- content: ' 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 🐙 ';
- padding: 1ex;
- animation: marquee 10s linear infinite;
-}
-@keyframes marquee {
- 0% { transform: translate(100%, 0); }
- 100% { transform: translate(-100%, 0); }
-}
-
-#autocomplete_results[state="done"]:empty {
- display: block;
- text-align: center;
- padding: 1ex;
-}
-#autocomplete_results[state="done"]:empty::before {
- content: '(no results)';
- font-style: italic;
-}
-
-#autocomplete_results a {
- display: block;
- color: inherit;
- padding: 1ex;
- border-left: 0.5ex solid transparent;
- padding-left: 0.5ex;
- cursor: pointer;
-}
-
-#autocomplete_results .selected .result_link a {
- background: var(--body-bg);
- border-color: var(--structure-and-inductive-color);
-}
-
-
-#search_results {
- display: table;
- width: 100%;
-}
-#search_results[state="done"]:empty::before {
- content: '(no results)';
- font-style: italic;
-}
-
-#search_results .result_link, #search_results .result_doc {
- border-bottom: 1px solid rgba(0, 0, 0, 0.8);
-}
-
-.search_result {
- display: table-row;
-}
-
-.result_link, .result_doc {
- display: table-cell;
- overflow: hidden;
- word-break: break-word;
-}
-
-main, nav {
- margin-top: calc(var(--header-height) + 1em);
-}
-
-/* extra space for scrolling things to the top */
-main {
- margin-bottom: 90vh;
-}
-
-main {
- max-width: var(--content-width);
- /* center it: */
- margin-left: auto;
- margin-right: auto;
-}
-
-nav {
- float: left;
- height: calc(100vh - var(--header-height) - 1em);
- position: fixed;
- top: 0;
- overflow: auto;
- scrollbar-width: thin;
- scrollbar-color: transparent transparent;
-}
-
-nav:hover {
- scrollbar-color: gray transparent;
-}
-
-nav {
- --column-available-space: calc((100vw - var(--content-width) - 5em)/2);
- --column-width: calc(var(--column-available-space) - 1ex);
- --dist-to-edge: 1ex;
- width: var(--content-width);
- max-width: var(--column-width);
-}
-@supports (width: min(10px, 5vw)) {
- .nav { --desired-column-width: 20em; }
- .internal_nav { --desired-column-width: 30em; }
- nav {
- --column-available-space: calc(max(0px, (100vw - var(--content-width) - 5em)/2));
- --column-width: calc(clamp(0px, var(--column-available-space) - 1ex, var(--desired-column-width)));
- --dist-to-edge: calc(max(1ex, var(--column-available-space) - var(--column-width)));
- }
-}
-
-.nav { left: var(--dist-to-edge); }
-.internal_nav { right: var(--dist-to-edge); }
-
-.internal_nav .nav_link, .taclink {
- /* indent everything but first line by 2ex */
- text-indent: -2ex; padding-left: 2ex;
-}
-
-.navframe {
- height: 100%;
- width: 100%;
-}
-
-.navframe .nav {
- position: absolute;
- left: 0;
- margin-left: 0;
-}
-
-.internal_nav .imports {
- margin-bottom: 1rem;
-}
-
-.tagfilter-div {
- margin-bottom: 1em;
-}
-.tagfilter-div > summary {
- margin-bottom: 1ex;
-}
-
-/* top-level modules in left navbar */
-.nav .module_list > details {
- margin-top: 1ex;
-}
-
-.nav details > * {
- padding-left: 2ex;
-}
-
-.nav summary {
- cursor: pointer;
- padding-left: 0;
-}
-
-.nav summary::marker {
- font-size: 85%;
-}
-
-.nav .nav_file {
- display: inline-block;
-}
-
-.nav h3 {
- margin-block-end: 4px;
-}
-
-/* People use way too long declaration names. */
-.internal_nav, .decl_name {
- overflow-wrap: break-word;
-}
-
-/* Add a linebreak after a declaration name. */
-.decl_name::after {
- content: "\A";
- white-space: pre;
-}
-
-.nav_link {
- overflow-wrap: break-word;
-}
-
-.navframe {
- --header-height: 0;
-}
-
-#settings {
- margin-top: 5em;
-}
-#settings h3 {
- font-size: inherit;
-}
-
-#color-theme-switcher {
- display: flex;
- justify-content: space-between;
- padding: 0 2ex;
- flex-flow: row wrap;
-}
-
-/* custom radio buttons for dark/light switch */
-#color-theme-switcher input {
- -webkit-appearance: none;
- -moz-appearance: none;
- appearance: none;
- display: inline-block;
- box-sizing: content-box;
- height: 1em;
- width: 1em;
- background-clip: content-box;
- padding: 2px;
- border: 2px solid transparent;
- margin-bottom: -4px;
- border-radius: 50%;
-}
-#color-theme-dark { background-color: #444; }
-#color-theme-light { background-color: #ccc; }
-#color-theme-system {
- background-image: linear-gradient(60deg, #444, #444 50%, #CCC 50%, #CCC);
-}
-#color-theme-switcher input:checked {
- border-color: var(--text-color);
-}
-
-.decl > div, .mod_doc {
- padding-left: 8px;
- padding-right: 8px;
-}
-
-.decl {
- margin-top: 20px;
- margin-bottom: 20px;
-}
-
-.decl > div {
- /* sometimes declarations arguments are way too long
- and would continue into the right column,
- so put a scroll bar there: */
- overflow-x: auto;
-}
-
-/* Make `#id` links appear below header. */
-.decl, h1[id], h2[id], h3[id], h4[id], h5[id], h6[id] {
- scroll-margin-top: var(--fragment-offset);
-}
-/* don't need as much vertical space for these
-inline elements */
-a[id], li[id] {
- scroll-margin-top: var(--header-height);
-}
-
-/* HACK: Safari doesn't support scroll-margin-top for
-fragment links (yet?)
-https://caniuse.com/mdn-css_properties_scroll-margin-top
-https://bugs.webkit.org/show_bug.cgi?id=189265
-*/
-@supports not (scroll-margin-top: var(--fragment-offset)) {
- .decl::before, h1[id]::before, h2[id]::before, h3[id]::before,
- h4[id]::before, h5[id]::before, h6[id]::before,
- a[id]::before, li[id]::before {
- content: "";
- display: block;
- height: var(--fragment-offset);
- margin-top: calc(-1 * var(--fragment-offset));
- box-sizing: inherit;
- visibility: hidden;
- width: 1px;
- }
-}
-
-
-/* hide # after markdown headings except on hover */
-.markdown-heading:not(:hover) > .hover-link {
- visibility: hidden;
-}
-
-main h2, main h3, main h4, main h5, main h6 {
- margin-top: 2rem;
-}
-.decl + .mod_doc > h2,
- .decl + .mod_doc > h3,
- .decl + .mod_doc > h4,
- .decl + .mod_doc > h5,
- .decl + .mod_doc > h6 {
- margin-top: 4rem;
-}
-
-.def, .instance {
- border-left: 10px solid var(--text-color);
- border-top: 2px solid var(--text-color);
-}
-
-.theorem {
- border-left: 10px solid var(--theorem-color);
- border-top: 2px solid var(--theorem-color);
-}
-
-.axiom, .opaque {
- border-left: 10px solid var(--axiom-and-constant-color);
- border-top: 2px solid var(--axiom-and-constant-color);
-}
-
-.structure, .inductive, .class {
- border-left: 10px solid var(--structure-and-inductive-color);
- border-top: 2px solid var(--structure-and-inductive-color);
-}
-
-.fn {
- display: inline-block;
- /* border: 1px dashed red; */
- text-indent: -1ex;
- padding-left: 1ex;
- white-space: pre-wrap;
- vertical-align: top;
-}
-
-.fn { --fn: 1; }
-.fn .fn { --fn: 2; }
-.fn .fn .fn { --fn: 3; }
-.fn .fn .fn .fn { --fn: 4; }
-.fn .fn .fn .fn .fn { --fn: 5; }
-.fn .fn .fn .fn .fn .fn { --fn: 6; }
-.fn .fn .fn .fn .fn .fn .fn { --fn: 7; }
-.fn .fn .fn .fn .fn .fn .fn .fn { --fn: 8; }
-.fn {
- transition: background-color 100ms ease-in-out;
-}
-
-.def .fn:hover, .instance .fn:hover {
- background-color: hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*var(--fn)));
- box-shadow: 0 0 0 1px hsla(var(--def-color-hsl-angle), 61%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
- border-radius: 5px;
-}
-.theorem .fn:hover {
- background-color: hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*var(--fn)));
- box-shadow: 0 0 0 1px hsla(var(--theorem-color-hsl-angle), 62%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
- border-radius: 5px;
-}
-.axiom .fn:hover, .opaque .fn:hover {
- background-color: hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*var(--fn)));
- box-shadow: 0 0 0 1px hsla(var(--axiom-and-constant-color-hsl-angle), 94%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
- border-radius: 5px;
-}
-.structure .fn:hover, .inductive .fn:hover, .class .fn:hover {
- background-color: hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*var(--fn)));
- box-shadow: 0 0 0 1px hsla(var(--structure-and-inductive-color-hsl-angle), 98%, calc(var(--starting-percentage) - 5%*(var(--fn) + 1)));
- border-radius: 5px;
-}
-
-.decl_args, .decl_type .decl_parent {
- font-weight: normal;
-}
-
-.implicits, .impl_arg {
- color: var(--text-color);
- white-space: normal;
-}
-
-.decl_kind, .decl_name, .decl_extends {
- font-weight: bold;
-}
-
-/* break long declaration names at periods where possible */
-.break_within {
- word-break: break-all;
-}
-
-.break_within .name {
- word-break: normal;
-}
-
-.decl_header {
- /* indent everything but first line twice as much as decl_type */
- text-indent: -8ex; padding-left: 8ex;
-}
-
-.decl_type {
- margin-top: 2px;
- margin-left: 4ex; /* extra indentation */
-}
-
-.imports li, code, .decl_header, .attributes, .structure_field_info,
-.constructor, .instances li, .instances-for-list li, .equation,
-.structure_ext_ctor {
- font-size: 16px;
- font-family: 'JuliaMono', monospace;
-}
-
-pre {
- white-space: break-spaces;
-}
-
-code, pre { background: var(--code-bg); }
-code, pre { border-radius: 5px; }
-code { padding: 1px 3px; }
-pre { padding: 1ex; }
-pre code { padding: 0 0; }
-
-#howabout code { background: inherit; }
-#howabout li { margin-bottom: 0.5ex; }
-
-.structure_fields, .constructors {
- display: block;
- padding-inline-start: 0;
- margin-top: 1ex;
- text-indent: -2ex; padding-left: 2ex;
-}
-
-.structure_field {
- display: block;
- margin-left: 2ex;
-}
-
-.inductive_ctor_doc {
- text-indent: 2ex;
- font-family: 'Lato Medium';
- font-size: 17px;
-}
-
-.structure_field_doc {
- text-indent: 0;
- font-family: 'Lato Medium';
- font-size: 17px;
-}
-
-.structure_ext_fields {
- display: block;
- padding-inline-start: 0;
- margin-top: 1ex;
- text-indent: -2ex; padding-left: 2ex;
-}
-
-.structure_ext_fields .structure_field {
- margin-left: -1ex !important;
-}
-
-.structure_ext_ctor {
- display: block;
- text-indent: -3ex;
-}
-
-.constructor {
- display: block;
-}
-.constructor:before {
- content: '| ';
- color: gray;
-}
-
-/** Don't show underline on types, to prevent the ≤ vs < confusion. **/
-a:link, a:visited, a:active {
- color:var(--link-color);
- text-decoration: none;
-}
-
-a.pdf:link, a.pdf:visited, a.pdf:active {
- color:var(--link-pdf-color);
-}
-
-/** Show it on hover though. **/
-a:hover {
- text-decoration: underline;
-}
-
-.impl_arg {
- font-style: italic;
- transition: opacity 300ms ease-in;
-}
-
-.decl_header:not(:hover) .impl_arg {
- opacity: 30%;
- transition: opacity 1000ms ease-out;
-}
-
-.gh_link {
- float: right;
- margin-left: 10px;
-}
-
-.ink_link {
- float: right;
- margin-left: 20px;
-}
-
-
-.docfile h2, .note h2 {
- margin-block-start: 3px;
- margin-block-end: 0px;
-}
-
-.docfile h2 a {
- color: var(--text-color);
-}
-
-.tags {
- margin-bottom: 1ex;
-}
-
-.tags ul {
- display: inline;
- padding: 0;
-}
-
-.tags li {
- border: 1px solid var(--tags-border-color);
- border-radius: 4px;
- list-style-type: none;
- padding: 1px 3px;
- margin-left: 1ex;
- display: inline-block;
-}
-
-/* used by nav.js */
-.hide { display: none; }
-
-.tactic, .note {
- border-top: 3px solid #0479c7;
- padding-top: 2em;
- margin-top: 2em;
- margin-bottom: 2em;
-}
diff --git a/static/tactic.js b/static/tactic.js
deleted file mode 100644
index e40c4ec..0000000
--- a/static/tactic.js
+++ /dev/null
@@ -1,61 +0,0 @@
-// TODO: The tactic part seem to be unimplemented now.
-
-function filterSelectionClass(tagNames, classname) {
- if (tagNames.length == 0) {
- for (const elem of document.getElementsByClassName(classname)) {
- elem.classList.remove("hide");
- }
- } else {
- // Add the "show" class (display:block) to the filtered elements, and remove the "show" class from the elements that are not selected
- for (const elem of document.getElementsByClassName(classname)) {
- elem.classList.add("hide");
- for (const tagName of tagNames) {
- if (elem.classList.contains(tagName)) {
- elem.classList.remove("hide");
- }
- }
- }
- }
-}
-
-function filterSelection(c) {
- filterSelectionClass(c, "tactic");
- filterSelectionClass(c, "taclink");
-}
-
-var filterBoxes = document.getElementsByClassName("tagfilter");
-
-function updateDisplay() {
- filterSelection(getSelectValues());
-}
-
-function getSelectValues() {
- var result = [];
-
- for (const opt of filterBoxes) {
- if (opt.checked) {
- result.push(opt.value);
- }
- }
- return result;
-}
-
-function setSelectVal(val) {
- for (const opt of filterBoxes) {
- opt.checked = val;
- }
-}
-
-updateDisplay();
-
-for (const opt of filterBoxes) {
- opt.addEventListener("change", updateDisplay);
-}
-
-const tse = document.getElementById("tagfilter-selectall");
-if (tse != null) {
- tse.addEventListener("change", function () {
- setSelectVal(this.checked);
- updateDisplay();
- });
-}