diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean
index 732e555..c4b28a9 100644
--- a/DocGen4/IncludeStr.lean
+++ b/DocGen4/IncludeStr.lean
@@ -34,21 +34,21 @@ don't have to carry them around as files.
-/
@[termElab includeStr] def includeStrImpl : TermElab := λ stx _ => do
let str := stx[1].isStrLit?.get!
- let srcPath := FilePath.mk $ ←getFileName
+ let srcPath := FilePath.mk <| ←getFileName
let currentDir ← IO.currentDir
-- HACK: Currently we cannot get current file path in VSCode, we have to traversely find the matched subdirectory in the current directory.
if let some path ← match srcPath.parent with
- | some p => pure $ some $ p / str
+ | some p => pure <| some <| p / str
| none => do
let foundDir ← traverseDir currentDir λ p => p / str |>.pathExists
- pure $ foundDir.map (· / str)
+ pure <| foundDir.map (· / str)
then
if ←path.pathExists then
if ←path.isDir then
throwError s!"{str} is a directory"
else
let content ← FS.readFile path
- pure $ mkStrLit content
+ pure <| mkStrLit content
else
throwError s!"{path} does not exist as a file"
else
diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean
index b534744..60d1d31 100644
--- a/DocGen4/LeanInk/Output.lean
+++ b/DocGen4/LeanInk/Output.lean
@@ -55,7 +55,7 @@ def Token.toHtml (t : Token) : AlectryonM Html := do
-- TODO: render docstring
let mut parts := #[]
if let some tyi := t.typeinfo then
- parts := parts.push $ ←tyi.toHtml
+ parts := parts.push <| ←tyi.toHtml
parts := parts.push t.processSemantic
@@ -218,6 +218,6 @@ def moduleToHtml (module : Process.Module) (inkPath : System.FilePath) (sourceFi
let baseCtx ← readThe SiteBaseContext
let (html, _) := render |>.run ctx baseCtx
pure html
- | .error err => throw $ IO.userError s!"Error while parsing LeanInk Output: {err}"
+ | .error err => throw <| IO.userError s!"Error while parsing LeanInk Output: {err}"
end DocGen4.Output.LeanInk
diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean
index 0f9661f..26ab8db 100644
--- a/DocGen4/LeanInk/Process.lean
+++ b/DocGen4/LeanInk/Process.lean
@@ -33,8 +33,8 @@ def runInk (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : IO J
match Json.parse output with
| .ok out => pure out
| .error err =>
- throw $ IO.userError s!"LeanInk returned invalid JSON for file: {sourceFilePath}:\n{err}"
+ throw <| IO.userError s!"LeanInk returned invalid JSON for file: {sourceFilePath}:\n{err}"
| code =>
- throw $ IO.userError s!"LeanInk exited with code {code} for file: {sourceFilePath}:\n{←inkProcess.stderr.readToEnd}"
+ throw <| IO.userError s!"LeanInk exited with code {code} for file: {sourceFilePath}:\n{←inkProcess.stderr.readToEnd}"
end DocGen4.Output.LeanInk
diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index 10f1c48..e6e9db9 100644
--- a/DocGen4/Load.lean
+++ b/DocGen4/Load.lean
@@ -21,7 +21,7 @@ as well as all the dependencies.
-/
def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do
let (leanInstall?, lakeInstall?) ← Lake.findInstall?
- match ←(EIO.toIO' $ Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
+ match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
| .ok config =>
let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio
let libraryLeanGitHash := ws.env.lean.githash
@@ -30,16 +30,16 @@ def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do
let ctx ← Lake.mkBuildContext ws
(ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx
initSearchPath (←findSysroot) ws.leanPaths.oleanPath
- pure $ Except.ok ws
+ pure <| Except.ok ws
| .error err =>
- throw $ IO.userError err.toString
+ throw <| IO.userError err.toString
def envOfImports (imports : List Name) : IO Environment := do
importModules (imports.map (Import.mk · false)) Options.empty
def loadInit (imports : List Name) : IO Hierarchy := do
let env ← envOfImports imports
- pure $ Hierarchy.fromArray env.header.moduleNames
+ pure <| Hierarchy.fromArray env.header.moduleNames
/--
Load a list of modules from the current Lean search path into an `Environment`
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index db1d156..07b1229 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -90,7 +90,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
--let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath
let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath
- discard $ htmlOutputDeclarationDatas result |>.run config baseConfig
+ discard <| htmlOutputDeclarationDatas result |>.run config baseConfig
for (modName, module) in result.moduleInfo.toArray do
let fileDir := moduleNameToDirectory basePath modName
@@ -99,7 +99,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
-- 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 }
let moduleHtml := moduleToHtml module |>.run config baseConfig
- FS.createDirAll $ fileDir
+ FS.createDirAll fileDir
FS.writeFile filePath moduleHtml.toString
if let some inkPath := inkPath then
if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index c68d218..469b77c 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -75,7 +75,7 @@ def getRoot : BaseHtmlM String := do
def getHierarchy : BaseHtmlM Hierarchy := do pure (←read).hierarchy
def getCurrentName : BaseHtmlM (Option Name) := do pure (←read).currentName
def getResult : HtmlM AnalyzerResult := do pure (←read).result
-def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range
+def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure <| (←read).sourceLinker module range
def leanInkEnabled? : HtmlM Bool := do pure (←read).leanInkEnabled
/--
@@ -93,7 +93,7 @@ Returns the doc-gen4 link to a module name.
-/
def moduleNameToLink (n : Name) : BaseHtmlM String := do
let parts := n.components.map Name.toString
- pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+ pure <| (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
/--
Returns the HTML doc-gen4 link to a module name.
@@ -106,7 +106,7 @@ Returns the LeanInk link to a module name.
-/
def moduleNameToInkLink (n : Name) : BaseHtmlM String := do
let parts := "src" :: n.components.map Name.toString
- pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+ pure <| (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
/--
Returns the path to the HTML file that contains information about a module.
@@ -149,7 +149,7 @@ 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]!
- pure $ (←moduleNameToLink module) ++ "#" ++ name.toString
+ pure <| (←moduleNameToLink module) ++ "#" ++ name.toString
/--
Returns the HTML doc-gen4 link to a declaration name.
@@ -163,7 +163,7 @@ 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]!
- pure $ (←moduleNameToInkLink module) ++ "#" ++ name.toString
+ pure <| (←moduleNameToInkLink module) ++ "#" ++ name.toString
/--
Returns the HTML doc-gen4 link to a declaration name with "break_within"
@@ -185,7 +185,7 @@ 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 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
@@ -199,7 +199,7 @@ to as much information as possible.
partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
match i with
| TaggedText.text t => pure #[Html.escape t]
- | TaggedText.append tt => tt.foldlM (λ acc t => do pure $ acc ++ (←infoFormatToHtml t)) #[]
+ | TaggedText.append tt => tt.foldlM (λ acc t => do pure <| acc ++ (←infoFormatToHtml t)) #[]
| TaggedText.tag a t =>
match a.info.val.info with
| Info.ofTermInfo i =>
@@ -207,7 +207,7 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
| Expr.const name _ =>
match t with
| TaggedText.text t =>
- let (front, t, back) := splitWhitespaces $ Html.escape t
+ let (front, t, back) := splitWhitespaces <| Html.escape t
let elem := {t}
pure #[Html.text front, elem, Html.text back]
| _ =>
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index d1506ab..a501e08 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -161,7 +161,7 @@ def autoLink (el : Element) : HtmlM Element := do
match link? with
| some link =>
let attributes := Std.RBMap.empty.insert "href" link
- pure [Content.Element $ Element.Element "a" attributes #[Content.Character s]]
+ pure [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
| none =>
let sHead := s.dropRightWhile (λ c => c ≠ '.')
let sTail := s.takeRightWhile (λ c => c ≠ '.')
@@ -171,7 +171,7 @@ def autoLink (el : Element) : HtmlM Element := do
let attributes := Std.RBMap.empty.insert "href" link'
pure [
Content.Character sHead,
- Content.Element $ Element.Element "a" attributes #[Content.Character sTail]
+ Content.Element <| Element.Element "a" attributes #[Content.Character sTail]
]
| none =>
pure [Content.Character s]
@@ -204,7 +204,7 @@ def docStringToHtml (s : String) : HtmlM (Array Html) := do
match manyDocument rendered.mkIterator with
| Parsec.ParseResult.success _ res =>
res.mapM λ x => do
- pure (Html.text $ toString (← modifyElement x))
+ pure (Html.text <| toString (← modifyElement x))
| _ => pure #[Html.text rendered]
end Output
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index 6132dc8..48fcd3d 100644
--- a/DocGen4/Output/Index.lean
+++ b/DocGen4/Output/Index.lean
@@ -11,12 +11,13 @@ namespace Output
open scoped DocGen4.Jsx
-def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") $ pure $
-
-
-
Welcome to the documentation page
- What is up?
-
+def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
+ pure <|
+
+
+