37 lines
1.2 KiB
Plaintext
37 lines
1.2 KiB
Plaintext
/-
|
||
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
|