diff --git a/Main.lean b/Main.lean
index 1dc5ed6..eef68ef 100644
--- a/Main.lean
+++ b/Main.lean
@@ -8,6 +8,7 @@ import LeanDoc.Doc.Html
import LeanDoc.Output
import LeanDoc.Output.Html
import LeanDoc.Doc.Concrete
+import LeanDoc.Doc.Lsp
open LeanDoc Doc Output Html Concrete ToHtml Elab Monad
open Lean Elab Term
@@ -22,7 +23,7 @@ def vanish : RoleExpander
def rev : RoleExpander
| _args, stxs => .reverse <$> stxs.mapM elabInline
-def html [Monad m] (doc : Part .none) : m Html := Genre.none.toHtml {logError := fun _ => pure ()} () () doc
+def html [Monad m] (doc : Doc .none) : m Html := Genre.none.toHtml {logError := fun _ => pure ()} () () doc
def main : IO Unit := do
IO.println <| Html.asString <| Html.embody <| ← html <| #doc (.none) "My wonderful document" =>
@@ -59,6 +60,12 @@ As someone said:
Block code too
```
+[foo][my link][^foo]
+
## Other idea
+[my link]: https://example.com
+
+[^foo]: blah blah blah *BLAH*!
+
## Further subsection
diff --git a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean
index 25364a2..2fc5c8f 100644
--- a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean
+++ b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean
@@ -97,12 +97,9 @@ namespace Blog
structure Post where
date : Date
authors : List String
- content : Part Blog
+ content : Doc Blog
draft : Bool
-deriving TypeName
-
-instance : Inhabited Post where
- default := ⟨default, default, default, default⟩
+deriving TypeName, Inhabited
partial def TraverseState.freshId (state : Blog.TraverseState) (path : List String) (hint : Lean.Name) : String := Id.run do
let mut idStr := mangle (toString hint)
diff --git a/src/leanblog/LeanDoc/Genre/Blog/Generate.lean b/src/leanblog/LeanDoc/Genre/Blog/Generate.lean
index d8a758d..5cd8437 100644
--- a/src/leanblog/LeanDoc/Genre/Blog/Generate.lean
+++ b/src/leanblog/LeanDoc/Genre/Blog/Generate.lean
@@ -89,7 +89,7 @@ def inPage (here : Page) (act : GenerateM α) : GenerateM α :=
withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [here.name]}) act
def inPost (here : Post) (act : GenerateM α) : GenerateM α :=
- withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [c.ctxt.config.postName here.date here.content.titleString ]}) act
+ withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [c.ctxt.config.postName here.date here.content.content.titleString ]}) act
@@ -125,7 +125,7 @@ mutual
if post.draft && !(← showDrafts) then continue
inPost post <| do
let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.postTemplate, id⟩
- let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart post.content
+ let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart post.content.content
ensureDir (← currentDir)
IO.println s!"Generating post {← currentDir}"
IO.FS.withFile ((← currentDir).join "index.html") .write fun h => do
@@ -142,7 +142,7 @@ mutual
some <$> ps.mapM fun p =>
theme.archiveEntryTemplate.render (.ofList [("post", ⟨.mk p, #[]⟩)])
else pure none
- let pageParams : Template.Params ← forPart txt
+ let pageParams : Template.Params ← forPart txt.content
let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.pageTemplate, id⟩
let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <|
match postList with
@@ -164,7 +164,7 @@ def Site.generate (theme : Theme) (site : Site): GenerateM Unit := do
let root ← currentDir
ensureDir root
let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.pageTemplate, id⟩
- let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart site.frontPage
+ let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart site.frontPage.content
let filename := root.join "index.html"
IO.FS.withFile filename .write fun h => do
h.putStrLn ""
diff --git a/src/leanblog/LeanDoc/Genre/Blog/Site.lean b/src/leanblog/LeanDoc/Genre/Blog/Site.lean
index de79a78..0a8ae08 100644
--- a/src/leanblog/LeanDoc/Genre/Blog/Site.lean
+++ b/src/leanblog/LeanDoc/Genre/Blog/Site.lean
@@ -10,7 +10,7 @@ inductive Dir α where
deriving Inhabited
defmethod Post.traverse1 (post : Post) : Blog.TraverseM Post :=
- withReader (fun ctxt => {ctxt with path := ctxt.path ++ [ctxt.config.postName post.date post.content.titleString]}) <| do
+ withReader (fun ctxt => {ctxt with path := ctxt.path ++ [ctxt.config.postName post.date post.content.content.titleString]}) <| do
let content' ← Blog.traverse post.content
pure {post with content := content'}
@@ -20,7 +20,7 @@ def Dir.traverse1 (dir : Dir α) (sub : α → Blog.TraverseM α) : Blog.Travers
| .blog posts => .blog <$> posts.mapM Post.traverse1
inductive Page where
- | page (name : String) (id : Lean.Name) (text : Part Blog) (contents : Dir Page)
+ | page (name : String) (id : Lean.Name) (text : Doc Blog) (contents : Dir Page)
| static (name : String) (files : System.FilePath)
instance : Inhabited Page where
@@ -41,7 +41,7 @@ partial def Page.traverse1 (nav : Page) : Blog.TraverseM Page := do
| .static .. => pure nav
structure Site where
- frontPage : Part Blog
+ frontPage : Doc Blog
contents : Dir Page
def Site.traverse1 (site : Site) : Blog.TraverseM Site := do
@@ -69,7 +69,7 @@ class MonadPath (m : Type → Type u) where
export MonadPath (currentPath)
def postName [Monad m] [MonadConfig m] (post : Post) : m String := do
- pure <| (← currentConfig).postName post.date post.content.titleString
+ pure <| (← currentConfig).postName post.date post.content.content.titleString
def relative [Monad m] [MonadConfig m] [MonadPath m] (target : List String) : m (List String) := do
return relativize (← currentPath) target
diff --git a/src/leanblog/LeanDoc/Genre/Blog/Theme.lean b/src/leanblog/LeanDoc/Genre/Blog/Theme.lean
index 1f250b3..5abd674 100644
--- a/src/leanblog/LeanDoc/Genre/Blog/Theme.lean
+++ b/src/leanblog/LeanDoc/Genre/Blog/Theme.lean
@@ -31,12 +31,12 @@ def dirLinks : Dir Page → TemplateM (Array Html)
| .pages subs =>
subs.filterMapM fun
| .page name _id txt .. =>
- pure <| some {{{{txt.titleString}}}}
+ pure <| some {{{{txt.content.titleString}}}}
| .static .. => pure none
| .blog subs =>
subs.mapM fun s => do
- let url ← mkLink [(← currentConfig).postName s.date s.content.titleString]
- return {{{{s.content.titleString}}}}
+ let url ← mkLink [(← currentConfig).postName s.date s.content.content.titleString]
+ return {{{{s.content.content.titleString}}}}
where
mkLink dest := do
let dest' ← relative dest
@@ -91,7 +91,7 @@ def archiveEntry : Template := do
| Date.mk y m d => {{ s!"{y}-{m}-{d}" }}
}}
" — "
- {{post.content.titleString}}
+ {{post.content.content.titleString}}
}}]
diff --git a/src/leandoc/LeanDoc/Doc.lean b/src/leandoc/LeanDoc/Doc.lean
index 830a991..59f5f46 100644
--- a/src/leandoc/LeanDoc/Doc.lean
+++ b/src/leandoc/LeanDoc/Doc.lean
@@ -54,6 +54,7 @@ inductive Inline (genre : Genre) : Type where
| code (string : String)
| linebreak (string : String)
| link (content : Array (Inline genre)) (dest : LinkDest)
+ | footnote (name : String)
| image (alt : String) (dest : LinkDest)
| concat (content : Array (Inline genre))
| other (container : genre.Inline) (content : Array (Inline genre))
@@ -61,9 +62,19 @@ inductive Inline (genre : Genre) : Type where
private def reprArray (r : α → Nat → Format) (arr : Array α) : Format :=
.bracket "#[" (.joinSep (arr.toList.map (r · max_prec)) ("," ++ .line)) "]"
+private def reprList (r : α → Nat → Format) (xs : List α) : Format :=
+ .bracket "[" (.joinSep (xs.map (r · max_prec)) ("," ++ .line)) "]"
+
+private def reprPair (x : α → Nat → Format) (y : β → Nat → Format) (v : α × β) : Format :=
+ .bracket "(" (x v.fst max_prec ++ ("," ++.line) ++ y v.snd max_prec) ")"
+
private def reprCtor (c : Name) (args : List Format) : Format :=
.nest 2 <| .group (.joinSep (.text s!"{c}" :: args) .line)
+private def reprHash [BEq α] [Hashable α] (k : α → Nat → Format) (v : β → Nat → Format) (h : Lean.HashMap α β) : Format :=
+ reprCtor ``Lean.HashMap.ofList [reprList (fun x _ => reprPair k v x) h.toList]
+
+
partial def Inline.reprPrec [Repr g.Inline] (inline : Inline g) (prec : Nat) : Std.Format :=
open Repr Std.Format in
let rec go i p :=
@@ -78,6 +89,7 @@ partial def Inline.reprPrec [Repr g.Inline] (inline : Inline g) (prec : Nat) : S
reprArray go content,
reprArg dest
]
+ | .footnote name => reprCtor ``Inline.footnote [reprArg name]
| .image content dest => reprCtor ``Inline.image [
reprArg content,
reprArg dest
@@ -175,6 +187,20 @@ partial def Part.reprPrec [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] (
instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] : Repr (Part g) := ⟨Part.reprPrec⟩
+structure Doc (genre : Genre) where
+ content : Part genre
+ linkRefs : Lean.HashMap String String
+ footnotes : Lean.HashMap String (Array (Inline genre))
+deriving Inhabited
+
+instance [Repr k] [Repr v] [BEq k] [Hashable k] : Repr (Lean.HashMap k v) where
+ reprPrec h _n := reprCtor ``Lean.HashMap.ofList [reprArg h.toList]
+
+def Doc.reprPrec [Repr (Inline g)] [Repr (Part g)] (doc : Doc g) (prec : Nat) : Std.Format :=
+ reprCtor ``Doc.mk [reprArg doc.content, reprArg doc.linkRefs, reprArg doc.footnotes]
+
+instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] [Repr (Part g)] : Repr (Doc g) := ⟨Doc.reprPrec⟩
+
class Traverse (g : Genre) (m : outParam (Type → Type)) where
part [MonadReader g.TraverseContext m] [MonadState g.TraverseState m] : Part g → m Unit
block [MonadReader g.TraverseContext m] [MonadState g.TraverseState m] : Block g → m Unit
@@ -187,8 +213,8 @@ class Traverse (g : Genre) (m : outParam (Type → Type)) where
partial def Genre.traverse (g : Genre)
[Traverse g m] [Monad m] [MonadReader g.TraverseContext m] [MonadState g.TraverseState m]
- (top : Part g) : m (Part g) :=
- part top
+ (top : Doc g) : m (Doc g) :=
+ doc top
where
inline (i : Doc.Inline g) : m (Doc.Inline g) := do
@@ -197,6 +223,7 @@ where
| .emph content => .emph <$> content.mapM inline
| .bold content => .bold <$> content.mapM inline
| .link content ref => (.link · ref) <$> content.mapM inline
+ | .footnote name => pure <| .footnote name
| .image alt ref => pure <| .image alt ref
| .concat content => .concat <$> content.mapM inline
| .other container content => do
@@ -230,3 +257,6 @@ where
p := p'
let .mk title titleString meta content subParts := p
pure <| .mk (← title.mapM inline) titleString meta (← content.mapM block) (← subParts.mapM part)
+
+ doc (d : Doc g) : m (Doc g) := do
+ pure <| .mk (← part d.content) d.linkRefs (← d.footnotes.foldM (fun fs k v => do pure <| fs.insert k (← v.mapM inline)) .empty)
diff --git a/src/leandoc/LeanDoc/Doc/Concrete.lean b/src/leandoc/LeanDoc/Doc/Concrete.lean
index a368472..5a041b5 100644
--- a/src/leandoc/LeanDoc/Doc/Concrete.lean
+++ b/src/leandoc/LeanDoc/Doc/Concrete.lean
@@ -51,14 +51,14 @@ def inlineStr := inStrLit <| textLine
elab "inlines!" s:inlineStr : term => open Lean Elab Term in
match s.raw with
| ` => do
- let tms ← DocElabM.run (.init (← `(foo))) <| out.mapM elabInline
+ let (tms, _) ← DocElabM.run {} (.init (← `(foo))) <| out.mapM elabInline
elabTerm (← `(term| #[ $[$tms],* ] )) none
| _ => throwUnsupportedSyntax
set_option pp.rawOnError true
/--
-info: #[Inline.text "Hello, ", Inline.emph #[Inline.bold #[Inline.text "emph"]]] : Array (Inline ?m.10489)
+info: #[Inline.text "Hello, ", Inline.emph #[Inline.bold #[Inline.text "emph"]]] : Array (Inline ?m.11031)
-/
#guard_msgs in
#check inlines!"Hello, _*emph*_"
@@ -89,14 +89,22 @@ elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:docu
let ⟨`⟩ := title
| dbg_trace "nope {ppSyntax title}" throwUnsupportedSyntax
let titleString := inlinesToString (← getEnv) titleParts
- let ((), st) ← liftTermElabM <| PartElabM.run (.init titleName) <| do
+ let ((), st, st') ← liftTermElabM <| PartElabM.run {} (.init titleName) <| do
setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline)
for b in blocks do partCommand b
closePartsUntil 0 endPos
pure ()
- let finished := st.partContext.toPartFrame.close endPos
+ let finished := st'.partContext.toPartFrame.close endPos
pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
- elabCommand (← `(def $n : Part $genre := $(← finished.toSyntax)))
+ for r in internalRefs st'.linkDefs st.linkRefs do
+ for stx in r.syntax do
+ pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
+ for r in internalRefs st'.footnoteDefs st.footnoteRefs do
+ for stx in r.syntax do
+ pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
+ let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v))
+ let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v))
+ elabCommand (← `(def $n : Doc $genre := {content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs)}))
elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : term => open Lean Elab Term PartElabM DocElabM in do
@@ -107,14 +115,23 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : term
let ⟨`⟩ := title
| dbg_trace "nope {ppSyntax title}" throwUnsupportedSyntax
let titleString := inlinesToString (← getEnv) titleParts
- let ((), st) ← PartElabM.run (.init titleName) <| do
+ let ((), st, st') ← PartElabM.run {} (.init titleName) <| do
setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline)
for b in blocks do partCommand b
closePartsUntil 0 endPos
pure ()
- let finished := st.partContext.toPartFrame.close endPos
+ let finished := st'.partContext.toPartFrame.close endPos
pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
- elabTerm (← `(($(← finished.toSyntax) : Part $genre))) none
+ for r in internalRefs st'.linkDefs st.linkRefs do
+ for stx in r.syntax do
+ pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
+ for r in internalRefs st'.footnoteDefs st.footnoteRefs do
+ for stx in r.syntax do
+ pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
+
+ let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v))
+ let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v))
+ elabTerm (← `(({content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs) : Doc $genre}))) none
macro "%doc" moduleName:ident : term =>
@@ -137,12 +154,21 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : comm
let ⟨`⟩ := title
| dbg_trace "nope {ppSyntax title}" throwUnsupportedSyntax
let titleString := inlinesToString (← getEnv) titleParts
- let ((), st) ← liftTermElabM <| PartElabM.run (.init titleName) <| do
+ let ((), st, st') ← liftTermElabM <| PartElabM.run {} (.init titleName) <| do
setTitle titleString (← liftDocElabM <| titleParts.mapM elabInline)
for b in blocks do partCommand b
closePartsUntil 0 endPos
pure ()
- let finished := st.partContext.toPartFrame.close endPos
+ let finished := st'.partContext.toPartFrame.close endPos
pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
let docName ← mkIdentFrom title <$> currentDocName
- elabCommand (← `(def $docName : Part $genre := $(← finished.toSyntax)))
+ let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v))
+ let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v))
+ for r in internalRefs st'.linkDefs st.linkRefs do
+ for stx in r.syntax do
+ pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
+ for r in internalRefs st'.footnoteDefs st.footnoteRefs do
+ for stx in r.syntax do
+ pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
+
+ elabCommand (← `(def $docName : Doc $genre := {content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs)}))
diff --git a/src/leandoc/LeanDoc/Doc/Elab.lean b/src/leandoc/LeanDoc/Doc/Elab.lean
index 4e07393..cd6b84c 100644
--- a/src/leandoc/LeanDoc/Doc/Elab.lean
+++ b/src/leandoc/LeanDoc/Doc/Elab.lean
@@ -12,6 +12,7 @@ namespace LeanDoc.Doc.Elab
open Lean Elab
open PartElabM
+open DocElabM
open LeanDoc.Syntax
def throwUnexpected [Monad m] [MonadError m] (stx : Syntax) : m α :=
@@ -27,7 +28,6 @@ partial def elabInline (inline : Syntax) : DocElabM (TSyntax `term) :=
for e in exp do
try
let termStx ← withFreshMacroScope <| e stx
-
return termStx
catch
| ex@(.internal id) =>
@@ -118,9 +118,21 @@ def _root_.LeanDoc.Syntax.link.expand : InlineExpander
match dest with
| `(link_target| ( $url )) =>
``(Inline.link #[$[$(← txt.mapM elabInline)],*] (LinkDest.url $url))
+ | `(link_target| [ $ref ]) => do
+ addLinkRef ref
+ -- Round-trip through quote to get rid of source locations, preventing unwanted IDE info
+ ``(Inline.link #[$[$(← txt.mapM elabInline)],*] (LinkDest.ref $(quote ref.getString)))
| _ => withRef dest throwUnsupportedSyntax
| _ => throwUnsupportedSyntax
+@[inline_expander LeanDoc.Syntax.footnote]
+def _root_.LeanDoc.Syntax.link.footnote : InlineExpander
+ | `(inline| [^ $name:str ]) => do
+ addFootnoteRef name
+ ``(Inline.footnote $(quote name.getString))
+ | _ => throwUnsupportedSyntax
+
+
@[inline_expander LeanDoc.Syntax.image]
def _root_.LeanDoc.Syntax.image.expand : InlineExpander
| `(inline| image[ $alt:str* ] $dest:link_target) => do
@@ -184,13 +196,25 @@ where
partial def closePartsUntil (outer : Nat) (endPos : String.Pos) : PartElabM Unit := do
let level ← currentLevel
if outer ≤ level then
- match (← get).partContext.close endPos with
+ match (← getThe PartElabM.State).partContext.close endPos with
| some ctxt' =>
- modify fun st => {st with partContext := ctxt'}
+ modifyThe PartElabM.State fun st => {st with partContext := ctxt'}
if outer < level then
closePartsUntil outer endPos
| none => pure ()
+@[part_command LeanDoc.Syntax.footnote_ref]
+partial def _root_.LeanDoc.Syntax.footnote_ref.command : PartCommand
+ | `(block| [^ $name:str ]: $contents* ) =>
+ addFootnoteDef name =<< contents.mapM (elabInline ·.raw)
+ | _ => throwUnsupportedSyntax
+
+@[part_command LeanDoc.Syntax.link_ref]
+partial def _root_.LeanDoc.Syntax.link_ref.command : PartCommand
+ | `(block| [ $name:str ]: $url:str ) =>
+ addLinkDef name url.getString
+ | stx => dbg_trace "{stx}"; throwUnsupportedSyntax
+
@[part_command LeanDoc.Syntax.header]
partial def _root_.LeanDoc.Syntax.header.command : PartCommand
@@ -305,7 +329,7 @@ def _root_.LeanDoc.Syntax.blockquote.expand : BlockExpander
@[block_expander LeanDoc.Syntax.codeblock]
def _root_.LeanDoc.Syntax.codeblock.expand : BlockExpander
- | ` => do
+ | ` => do
let name ← resolveGlobalConstNoOverloadWithInfo nameStx
let exp ← codeBlockExpandersFor name
-- TODO typed syntax here
@@ -321,7 +345,7 @@ def _root_.LeanDoc.Syntax.codeblock.expand : BlockExpander
| ex => throw ex
dbg_trace "No code block expander for '{nameStx}' ---> '{name}'"
throwUnsupportedSyntax
- | ` =>
+ | ` =>
``(Block.code Option.none #[] $(Syntax.mkNumLit col) $(quote contents))
| _ =>
throwUnsupportedSyntax
diff --git a/src/leandoc/LeanDoc/Doc/Elab/Monad.lean b/src/leandoc/LeanDoc/Doc/Elab/Monad.lean
index e749945..2accb8f 100644
--- a/src/leandoc/LeanDoc/Doc/Elab/Monad.lean
+++ b/src/leandoc/LeanDoc/Doc/Elab/Monad.lean
@@ -136,89 +136,156 @@ def PartContext.close (ctxt : PartContext) (endPos : String.Pos) : Option PartCo
def PartContext.push (ctxt : PartContext) (fr : PartFrame) : PartContext := ⟨fr, ctxt.parents.push ctxt.toPartFrame⟩
+/-- References that must be local to the current blob of concrete document syntax -/
+structure DocDef (α : Type) where
+ defSite : Syntax
+ val : α
+
+structure DocUses where
+ useSites : Array Syntax := {}
+
+def DocUses.add (uses : DocUses) (loc : Syntax) : DocUses := {uses with useSites := uses.useSites.push loc}
+
structure PartElabM.State where
partContext : PartContext
-deriving Repr
+ linkDefs : HashMap String (DocDef String) := {}
+ footnoteDefs : HashMap String (DocDef (Array (TSyntax `term))) := {}
+structure DocElabM.State where
+ linkRefs : HashMap String DocUses := {}
+ footnoteRefs : HashMap String DocUses := {}
-def PartElabM.State.init (title : Syntax) (expandedTitle : Option (String × Array (TSyntax `term)) := none) : PartElabM.State where
- partContext := {titleSyntax := title, expandedTitle, blocks := #[], priorParts := #[], parents := #[]}
+/-- Custom info tree data to save footnote and reflink cross-references -/
+structure DocRefInfo where
+ defSite : Option Syntax
+ useSites : Array Syntax
+deriving TypeName, Repr
-def PartElabM (α : Type) : Type := StateT PartElabM.State TermElabM α
+def DocRefInfo.syntax (dri : DocRefInfo) : Array Syntax :=
+ (dri.defSite.map (#[·])|>.getD #[]) ++ dri.useSites
-def PartElabM.run (st : PartElabM.State) (act : PartElabM α) : TermElabM (α × PartElabM.State) :=
- StateT.run act st
+def internalRefs (defs : HashMap String (DocDef α)) (refs : HashMap String DocUses) : Array DocRefInfo := Id.run do
+ let keys : HashSet String := defs.fold (fun soFar k _ => HashSet.insert soFar k) <| refs.fold (fun soFar k _ => soFar.insert k) {}
+ let mut refInfo := #[]
+ for k in keys do
+ refInfo := refInfo.push ⟨defs.find? k |>.map (·.defSite), refs.find? k |>.map (·.useSites) |>.getD #[]⟩
+ refInfo
+def PartElabM.State.init (title : Syntax) (expandedTitle : Option (String × Array (TSyntax `term)) := none) : PartElabM.State where
+ partContext := {titleSyntax := title, expandedTitle, blocks := #[], priorParts := #[], parents := #[]}
-instance : MonadRef PartElabM := inferInstanceAs <| MonadRef (StateT PartElabM.State TermElabM)
+def PartElabM (α : Type) : Type := StateT DocElabM.State (StateT PartElabM.State TermElabM) α
-instance : AddErrorMessageContext PartElabM := inferInstanceAs <| AddErrorMessageContext (StateT PartElabM.State TermElabM)
+def PartElabM.run (st : DocElabM.State) (st' : PartElabM.State) (act : PartElabM α) : TermElabM (α × DocElabM.State × PartElabM.State) := do
+ let ((res, st), st') ← act st st'
+ pure (res, st, st')
-instance : MonadQuotation PartElabM := inferInstanceAs <| MonadQuotation (StateT PartElabM.State TermElabM)
+instance : MonadRef PartElabM := inferInstanceAs <| MonadRef (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-instance : Monad PartElabM := inferInstanceAs <| Monad (StateT PartElabM.State TermElabM)
+instance : AddErrorMessageContext PartElabM := inferInstanceAs <| AddErrorMessageContext (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-instance : MonadLift TermElabM PartElabM := inferInstanceAs <| MonadLift TermElabM (StateT PartElabM.State TermElabM)
+instance : MonadQuotation PartElabM := inferInstanceAs <| MonadQuotation (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-instance : MonadExceptOf Exception PartElabM := inferInstanceAs <| MonadExceptOf Exception (StateT PartElabM.State TermElabM)
+instance : Monad PartElabM := inferInstanceAs <| Monad (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-instance : MonadState PartElabM.State PartElabM := inferInstanceAs <| MonadState PartElabM.State (StateT PartElabM.State TermElabM)
+instance : MonadLift TermElabM PartElabM where
+ monadLift act := fun st st' => do return ((← act, st), st')
-instance : MonadStateOf PartElabM.State PartElabM := inferInstanceAs <| MonadStateOf PartElabM.State (StateT PartElabM.State TermElabM)
+instance : MonadExceptOf Exception PartElabM := inferInstanceAs <| MonadExceptOf Exception (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-instance : MonadStateOf PartElabM.State PartElabM := inferInstanceAs <| MonadStateOf PartElabM.State (StateT PartElabM.State TermElabM)
+instance : MonadStateOf DocElabM.State PartElabM := inferInstanceAs <| MonadStateOf DocElabM.State (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-instance : MonadFinally PartElabM := inferInstanceAs <| MonadFinally (StateT PartElabM.State TermElabM)
+instance : MonadStateOf PartElabM.State PartElabM := inferInstanceAs <| MonadStateOf PartElabM.State (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-instance : MonadRef PartElabM := inferInstanceAs <| MonadRef (StateT PartElabM.State TermElabM)
+instance : MonadFinally PartElabM := inferInstanceAs <| MonadFinally (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-def DocElabM (α : Type) : Type := ReaderT PartElabM.State TermElabM α
+instance : MonadRef PartElabM := inferInstanceAs <| MonadRef (StateT DocElabM.State (StateT PartElabM.State TermElabM))
-def DocElabM.run (st : PartElabM.State) (act : DocElabM α) : TermElabM α :=
- ReaderT.run act st
+def DocElabM (α : Type) : Type := ReaderT PartElabM.State (StateT DocElabM.State TermElabM) α
-instance : Inhabited (DocElabM α) := inferInstanceAs <| Inhabited (ReaderT PartElabM.State TermElabM α)
+def DocElabM.run (st : DocElabM.State) (st' : PartElabM.State) (act : DocElabM α) : TermElabM (α × DocElabM.State) := do
+ StateT.run (act st') st
-instance : AddErrorMessageContext DocElabM := inferInstanceAs <| AddErrorMessageContext (ReaderT PartElabM.State TermElabM)
+instance : Inhabited (DocElabM α) := ⟨fun _ _ => default⟩
-instance : MonadLift TermElabM DocElabM := inferInstanceAs <| MonadLift TermElabM (ReaderT PartElabM.State TermElabM)
+instance : AddErrorMessageContext DocElabM := inferInstanceAs <| AddErrorMessageContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : MonadRef DocElabM := inferInstanceAs <| MonadRef (ReaderT PartElabM.State TermElabM)
+instance : MonadLift TermElabM DocElabM where
+ monadLift act := fun _ st' => do return (← act, st')
-instance : MonadQuotation DocElabM := inferInstanceAs <| MonadQuotation (ReaderT PartElabM.State TermElabM)
+instance : MonadRef DocElabM := inferInstanceAs <| MonadRef (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : Monad DocElabM := inferInstanceAs <| Monad (ReaderT PartElabM.State TermElabM)
+instance : MonadQuotation DocElabM := inferInstanceAs <| MonadQuotation (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : MonadLift TermElabM DocElabM := inferInstanceAs <| MonadLift TermElabM (ReaderT PartElabM.State TermElabM)
+instance : Monad DocElabM := inferInstanceAs <| Monad (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : MonadExceptOf Exception DocElabM := inferInstanceAs <| MonadExceptOf Exception (ReaderT PartElabM.State TermElabM)
+instance : MonadExceptOf Exception DocElabM := inferInstanceAs <| MonadExceptOf Exception (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : MonadReader PartElabM.State DocElabM := inferInstanceAs <| MonadReader PartElabM.State (ReaderT PartElabM.State TermElabM)
+instance : MonadReader PartElabM.State DocElabM := inferInstanceAs <| MonadReader PartElabM.State (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : MonadReaderOf PartElabM.State DocElabM := inferInstanceAs <| MonadReaderOf PartElabM.State (ReaderT PartElabM.State TermElabM)
+instance : MonadReaderOf PartElabM.State DocElabM := inferInstanceAs <| MonadReaderOf PartElabM.State (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : MonadReaderOf PartElabM.State DocElabM := inferInstanceAs <| MonadReaderOf PartElabM.State (ReaderT PartElabM.State TermElabM)
+instance : MonadStateOf DocElabM.State DocElabM := inferInstanceAs <| MonadStateOf DocElabM.State (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : MonadFinally DocElabM := inferInstanceAs <| MonadFinally (ReaderT PartElabM.State TermElabM)
+instance : MonadFinally DocElabM := inferInstanceAs <| MonadFinally (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
-instance : MonadRecDepth DocElabM := inferInstanceAs <| MonadRecDepth (ReaderT PartElabM.State TermElabM)
+instance : MonadRecDepth DocElabM where
+ withRecDepth n act := fun st st' => MonadRecDepth.withRecDepth n (act st st')
+ getRecDepth := fun _ st' => do return (← MonadRecDepth.getRecDepth, st')
+ getMaxRecDepth := fun _ st' => do return (← MonadRecDepth.getMaxRecDepth, st')
-def PartElabM.liftDocElabM (act : DocElabM α) : PartElabM α := do act.run (← get)
+def PartElabM.liftDocElabM (act : DocElabM α) : PartElabM α := do
+ let (out, st') ← act.run (← getThe DocElabM.State) (← getThe PartElabM.State)
+ set st'
+ pure out
instance : MonadLift DocElabM PartElabM := ⟨PartElabM.liftDocElabM⟩
-def PartElabM.currentLevel : PartElabM Nat := do return (← get).partContext.level
+def PartElabM.currentLevel : PartElabM Nat := do return (← getThe State).partContext.level
-def PartElabM.setTitle (titlePreview : String) (titleInlines : Array (TSyntax `term)) : PartElabM Unit := modify fun st =>
+def PartElabM.setTitle (titlePreview : String) (titleInlines : Array (TSyntax `term)) : PartElabM Unit := modifyThe State fun st =>
{st with partContext.expandedTitle := some (titlePreview, titleInlines)}
-def PartElabM.addBlock (block : TSyntax `term) : PartElabM Unit := modify fun st =>
+def PartElabM.addBlock (block : TSyntax `term) : PartElabM Unit := modifyThe State fun st =>
{st with partContext.blocks := st.partContext.blocks.push block}
-def PartElabM.push (fr : PartFrame) : PartElabM Unit := modify fun st => {st with partContext := st.partContext.push fr}
+def PartElabM.addLinkDef (refName : TSyntax `str) (url : String) : PartElabM Unit := do
+ let strName := refName.getString
+ match (← getThe State).linkDefs.find? strName with
+ | none =>
+ modifyThe State fun st => {st with linkDefs := st.linkDefs.insert strName ⟨refName, url⟩}
+ | some ⟨_, url'⟩ =>
+ throwErrorAt refName "Already defined as '{url'}'"
+
+def DocElabM.addLinkRef (refName : TSyntax `str) : DocElabM Unit := do
+ let strName := refName.getString
+ match (← getThe State).linkRefs.find? strName with
+ | none =>
+ modifyThe State fun st => {st with linkRefs := st.linkRefs.insert strName ⟨#[refName]⟩}
+ | some ⟨uses⟩ =>
+ modifyThe State fun st => {st with linkRefs := st.linkRefs.insert strName ⟨uses.push refName⟩}
+
+def PartElabM.addFootnoteDef (refName : TSyntax `str) (content : Array (TSyntax `term)) : PartElabM Unit := do
+ let strName := refName.getString
+ match (← getThe State).footnoteDefs.find? strName with
+ | none =>
+ modifyThe State fun st => {st with footnoteDefs := st.footnoteDefs.insert strName ⟨refName, content⟩}
+ | some ⟨_, url'⟩ =>
+ throwErrorAt refName "Already defined as '{url'}'"
+
+def DocElabM.addFootnoteRef (refName : TSyntax `str) : DocElabM Unit := do
+ let strName := refName.getString
+ match (← getThe State).footnoteRefs.find? strName with
+ | none =>
+ modifyThe State fun st => {st with footnoteRefs := st.footnoteRefs.insert strName ⟨#[refName]⟩}
+ | some ⟨uses⟩ =>
+ modifyThe State fun st => {st with footnoteRefs := st.footnoteRefs.insert strName ⟨uses.push refName⟩}
+
+
+def PartElabM.push (fr : PartFrame) : PartElabM Unit := modifyThe State fun st => {st with partContext := st.partContext.push fr}
def PartElabM.debug (msg : String) : PartElabM Unit := do
- let st ← get
+ let st ← getThe State
dbg_trace "DEBUG: {msg}"
dbg_trace " partContext: {repr st.partContext}"
dbg_trace ""
@@ -229,8 +296,6 @@ structure DocListInfo where
bullets : Array Syntax
deriving Repr, TypeName
-
-
abbrev InlineExpander := Syntax → DocElabM (TSyntax `term)
initialize inlineExpanderAttr : KeyedDeclsAttribute InlineExpander ←
diff --git a/src/leandoc/LeanDoc/Doc/Html.lean b/src/leandoc/LeanDoc/Doc/Html.lean
index 34963f5..11478e2 100644
--- a/src/leandoc/LeanDoc/Doc/Html.lean
+++ b/src/leandoc/LeanDoc/Doc/Html.lean
@@ -15,13 +15,15 @@ namespace LeanDoc.Doc.Html
open LeanDoc Output Doc Html
-structure Options (m : Type → Type) where
+structure Options (g : Genre) (m : Type → Type) where
/-- The level of the top-level headers -/
headerLevel : Nat := 1
logError : String → m Unit
+ refLinks : Lean.HashMap String String := {}
+ footnotes : Lean.HashMap String (Array (Inline g)) := {}
-abbrev HtmlT (genre : Genre) (m : Type → Type) (α : Type) : Type :=
- ReaderT (Options m × genre.TraverseContext × genre.TraverseState) m α
+abbrev HtmlT (genre : Genre) (m : Type → Type) : Type → Type :=
+ ReaderT (Options genre m × genre.TraverseContext × genre.TraverseState) m
instance [Functor m] : Functor (HtmlT genre m) where
map f act := fun ρ => Functor.map f (act ρ)
@@ -30,17 +32,17 @@ instance [Monad m] : Monad (HtmlT genre m) where
pure x := fun _ => pure x
bind act k := fun ρ => (act ρ >>= fun x => k x ρ)
-instance [Pure m] : MonadReader (Options m × genre.TraverseContext × genre.TraverseState) (HtmlT genre m) where
+instance [Pure m] : MonadReader (Options genre m × genre.TraverseContext × genre.TraverseState) (HtmlT genre m) where
read := fun ρ => pure ρ
-instance : MonadWithReader (Options m × genre.TraverseContext × genre.TraverseState) (HtmlT genre m) where
+instance : MonadWithReader (Options genre m × genre.TraverseContext × genre.TraverseState) (HtmlT genre m) where
withReader f act := fun ρ => act (f ρ)
-def HtmlT.options [Monad m] : HtmlT genre m (Options m) := do
+def HtmlT.options [Monad m] : HtmlT genre m (Options genre m) := do
let (opts, _, _) ← read
pure opts
-def HtmlT.withOptions (opts : Options m → Options m) (act : HtmlT g m α) : HtmlT g m α :=
+def HtmlT.withOptions (opts : Options g m → Options g m) (act : HtmlT g m α) : HtmlT g m α :=
withReader (fun (x, y, z) => (opts x, y, z)) act
def HtmlT.context [Monad m] : HtmlT genre m genre.TraverseContext := do
@@ -68,16 +70,30 @@ class GenreHtml (genre : Genre) (m : Type → Type) where
section
open ToHtml
-defmethod LinkDest.str : LinkDest → String
- | .url addr => addr
- | .ref TODO => TODO
+defmethod LinkDest.str [Monad m] : LinkDest → HtmlT g m String
+ | .url addr => pure addr
+ | .ref name => do
+ let ({refLinks := refs, ..}, _, _) ← read
+ if let some url := refs.find? name then
+ pure url
+ else
+ logError s!"Unknown reference '{name}'"
+ pure ""
partial def Inline.toHtml [Monad m] [GenreHtml g m] : Inline g → HtmlT g m Html
| .text str => pure <| .text str
| .link content dest => do
- pure {{ {{← content.mapM toHtml}} }}
+ pure {{ {{← content.mapM toHtml}} }}
| .image alt dest => do
- pure {{ 
}}
+ pure {{ 
}}
+ | .footnote name => do
+ let ({footnotes := footnotes, ..}, _, _) ← read
+ if let some txt := footnotes.find? name then
+ pure {{ }}
+ else
+ let message := s!"Unknown footnote '{name}' - options were {footnotes.toList.map (·.fst)}"
+ logError message
+ pure {{{{message}}}}
| .linebreak _str => pure .empty
| .emph content => do
pure {{ {{← content.mapM toHtml }} }}
@@ -137,12 +153,15 @@ partial def Part.toHtml [Monad m] [GenreHtml g m] (p : Part g) : HtmlT g m Html
instance [Monad m] [GenreHtml g m] : ToHtml g m (Part g) where
toHtml := Part.toHtml
+instance [Monad m] [GenreHtml g m] : ToHtml g m (Doc g) where
+ toHtml (d : Doc g) := withReader (fun o => {o with fst.refLinks := d.linkRefs, fst.footnotes := d.footnotes}) (Part.toHtml d.content)
+
instance : GenreHtml .none m where
part _ m := nomatch m
block _ x := nomatch x
inline _ x := nomatch x
-defmethod Genre.toHtml (g : Genre) [ToHtml g m α] (options : Options m) (context : g.TraverseContext) (state : g.TraverseState) (x : α) : m Html :=
+defmethod Genre.toHtml (g : Genre) [ToHtml g m α] (options : Options g m) (context : g.TraverseContext) (state : g.TraverseState) (x : α) : m Html :=
ToHtml.toHtml x (options, context, state)
open LeanDoc.Examples
diff --git a/src/leandoc/LeanDoc/Doc/Lsp.lean b/src/leandoc/LeanDoc/Doc/Lsp.lean
index e4cbfba..d4d8a73 100644
--- a/src/leandoc/LeanDoc/Doc/Lsp.lean
+++ b/src/leandoc/LeanDoc/Doc/Lsp.lean
@@ -11,7 +11,7 @@ import Std.CodeAction.Basic
import LeanDoc.Doc.Elab
import LeanDoc.Syntax
-open LeanDoc.Doc.Elab (DocListInfo TOC)
+open LeanDoc.Doc.Elab (DocListInfo DocRefInfo TOC)
open Lean
@@ -96,7 +96,39 @@ partial instance : FromJson Lean.Lsp.DocumentSymbolResult where
pure ⟨syms⟩
open Lean Server Lsp RequestM in
-def handleHl (params : DocumentHighlightParams) (prev : RequestTask DocumentHighlightResult) : RequestM (RequestTask DocumentHighlightResult) := do
+def handleDef (params : TextDocumentPositionParams) (prev : RequestTask (Array LocationLink)) : RequestM (RequestTask (Array LocationLink)) := do
+ let doc ← readDoc
+ let text := doc.meta.text
+ let pos := text.lspPosToUtf8Pos params.position
+ bindWaitFindSnap doc (·.endPos + ' ' >= pos) (notFoundX := pure prev) fun snap => do
+ withFallbackResponse prev <| pure <| Task.spawn <| fun () => do
+ let nodes := snap.infoTree.deepestNodes fun _ctxt info _arr =>
+ match info with
+ | .ofCustomInfo ⟨stx, data⟩ =>
+ if stx.containsPos pos then
+ data.get? DocRefInfo
+ else none
+ | _ => none
+ if nodes.isEmpty then prev.get
+ else
+ let mut locs := #[]
+ for node in nodes do
+ match node with
+ | ⟨some defSite, _⟩ =>
+ let mut origin : Option Range := none
+ for stx in node.syntax do
+ if let some ⟨head, tail⟩ := stx.getRange? then
+ if pos ≥ head && pos ≤ tail then
+ origin := stx.lspRange text
+ break
+ let some target := defSite.lspRange text
+ | continue
+ locs := locs.push {originSelectionRange? := origin, targetRange := target, targetUri := params.textDocument.uri, targetSelectionRange := target}
+ | _ => continue
+ pure locs
+
+open Lean Server Lsp RequestM in
+def handleRefs (params : ReferenceParams) (prev : RequestTask (Array Location)) : RequestM (RequestTask (Array Location)) := do
let doc ← readDoc
let text := doc.meta.text
let pos := text.lspPosToUtf8Pos params.position
@@ -106,17 +138,48 @@ def handleHl (params : DocumentHighlightParams) (prev : RequestTask DocumentHigh
match info with
| .ofCustomInfo ⟨stx, data⟩ =>
if stx.containsPos pos then
- data.get? DocListInfo
+ data.get? DocRefInfo
+ else none
+ | _ => none
+ if nodes.isEmpty then prev.get
+ else
+ let mut locs := #[]
+ for node in nodes do
+ for stx in node.syntax do
+ if let some range := stx.lspRange text then
+ locs := locs.push {uri := params.textDocument.uri, range := range}
+ pure locs
+
+open Lean Server Lsp RequestM in
+def handleHl (params : DocumentHighlightParams) (prev : RequestTask DocumentHighlightResult) : RequestM (RequestTask DocumentHighlightResult) := do
+ let doc ← readDoc
+ let text := doc.meta.text
+ let pos := text.lspPosToUtf8Pos params.position
+ bindWaitFindSnap doc (·.endPos + ' ' >= pos) (notFoundX := pure prev) fun snap => do
+ withFallbackResponse prev <| pure <| Task.spawn <| fun () => do
+ let nodes : List (_ ⊕ _) := snap.infoTree.deepestNodes fun _ctxt info _arr =>
+ match info with
+ | .ofCustomInfo ⟨stx, data⟩ =>
+ if stx.containsPos pos then
+ (.inl <$> data.get? DocListInfo) <|> (.inr <$> data.get? DocRefInfo)
else none
| _ => none
if nodes.isEmpty then prev.get
else
let mut hls := #[]
for node in nodes do
- let ⟨stxs⟩ := node
- for s in stxs do
- if let some r := s.lspRange text then
- hls := hls.push ⟨r, none⟩
+ match node with
+ | .inl ⟨stxs⟩ =>
+ for s in stxs do
+ if let some r := s.lspRange text then
+ hls := hls.push ⟨r, none⟩
+ | .inr ⟨defSite, useSites⟩ =>
+ if let some s := defSite then
+ if let some r := s.lspRange text then
+ hls := hls.push ⟨r, none⟩
+ for s in useSites do
+ if let some r := s.lspRange text then
+ hls := hls.push ⟨r, none⟩
pure hls
open Lean Lsp
@@ -361,6 +424,8 @@ def renumberLists : CodeActionProvider := fun params snap => do
open Lean Server Lsp in
initialize
+ chainLspRequestHandler "textDocument/definition" TextDocumentPositionParams (Array LocationLink) handleDef
+ -- chainLspRequestHandler "textDocument/references" ReferenceParams (Array Location) handleRefs -- TODO make this work - right now it goes through the watchdog so we can't chain it
chainLspRequestHandler "textDocument/documentHighlight" DocumentHighlightParams DocumentHighlightResult handleHl
chainLspRequestHandler "textDocument/documentSymbol" DocumentSymbolParams DocumentSymbolResult handleSyms
chainLspRequestHandler "textDocument/semanticTokens/full" SemanticTokensParams SemanticTokens handleTokensFull
diff --git a/src/leandoc/LeanDoc/Examples.lean b/src/leandoc/LeanDoc/Examples.lean
index 95369c1..75f2cc1 100644
--- a/src/leandoc/LeanDoc/Examples.lean
+++ b/src/leandoc/LeanDoc/Examples.lean
@@ -16,7 +16,12 @@ set_option pp.rawOnError true
:::::::
:::::::
-/-- info: LeanDoc.Doc.Part.mk #[LeanDoc.Doc.Inline.text "Nothing"] "Nothing" none #[] #[] -/
+/--
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk #[LeanDoc.Doc.Inline.text "Nothing"] "Nothing" none #[] #[]
+ Lean.HashMap.ofList []
+ Lean.HashMap.ofList []
+-/
#guard_msgs in
#eval noDoc
@@ -30,12 +35,15 @@ Hello, I'm a paragraph. Yes I am!
/--
-info: LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "My title here"]
- "My title here"
- none
- #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Hello, I'm a paragraph. Yes I am!"]]
- #[]
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "My title here"]
+ "My title here"
+ none
+ #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Hello, I'm a paragraph. Yes I am!"]]
+ #[]
+ Lean.HashMap.ofList []
+ Lean.HashMap.ofList []
-/
#guard_msgs in
#eval a
@@ -48,13 +56,17 @@ info: LeanDoc.Doc.Part.mk
:::::::
/--
-info: LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "My title here"]
- "My title here"
- none
- #[LeanDoc.Doc.Block.ul
- #[{ indent := 0, contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Just a list with one item"]] }]]
- #[]
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "My title here"]
+ "My title here"
+ none
+ #[LeanDoc.Doc.Block.ul
+ #[{ indent := 0,
+ contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Just a list with one item"]] }]]
+ #[]
+ Lean.HashMap.ofList []
+ Lean.HashMap.ofList []
-/
#guard_msgs in
#eval a'
@@ -71,17 +83,20 @@ a paragraph
:::::::
/--
-info: LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "My title here"]
- "My title here"
- none
- #[]
- #[LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "Section 1"]
- "Section 1"
- none
- #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "a paragraph"]]
- #[]]
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "My title here"]
+ "My title here"
+ none
+ #[]
+ #[LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Section 1"]
+ "Section 1"
+ none
+ #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "a paragraph"]]
+ #[]]
+ Lean.HashMap.ofList []
+ Lean.HashMap.ofList []
-/
#guard_msgs in
#eval b
@@ -106,30 +121,33 @@ More text:
:::::::
/--
-info: LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "My title here"]
- "My title here"
- none
- #[]
- #[LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "Section 1"]
- "Section 1"
- none
- #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "a paragraph"]]
- #[LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "Section 1.1"]
- "Section 1.1"
- none
- #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "More text:"],
- LeanDoc.Doc.Block.ul
- #[{ indent := 0, contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "and a list"]] },
- { indent := 0,
- contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "with two"],
- LeanDoc.Doc.Block.ul
- #[{ indent := 1,
- contents := #[LeanDoc.Doc.Block.para
- #[LeanDoc.Doc.Inline.text "and nested"]] }]] }]]
- #[]]]
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "My title here"]
+ "My title here"
+ none
+ #[]
+ #[LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Section 1"]
+ "Section 1"
+ none
+ #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "a paragraph"]]
+ #[LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Section 1.1"]
+ "Section 1.1"
+ none
+ #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "More text:"],
+ LeanDoc.Doc.Block.ul
+ #[{ indent := 0, contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "and a list"]] },
+ { indent := 0,
+ contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "with two"],
+ LeanDoc.Doc.Block.ul
+ #[{ indent := 1,
+ contents := #[LeanDoc.Doc.Block.para
+ #[LeanDoc.Doc.Inline.text "and nested"]] }]] }]]
+ #[]]]
+ Lean.HashMap.ofList []
+ Lean.HashMap.ofList []
-/
#guard_msgs in
#eval c
@@ -149,23 +167,26 @@ Also, 2 > 3.
:::::::
/--
-info: LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "More writing"]
- "More writing"
- none
- #[]
- #[LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "Section 1"]
- "Section 1"
- none
- #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Here's a quote;"],
- LeanDoc.Doc.Block.blockquote
- #[(LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "I like quotes"]),
- (LeanDoc.Doc.Block.ul
- #[{ indent := 2,
- contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Also with lists in them"]] }])],
- LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Also, 2 > 3."]]
- #[]]
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "More writing"]
+ "More writing"
+ none
+ #[]
+ #[LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Section 1"]
+ "Section 1"
+ none
+ #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Here's a quote;"],
+ LeanDoc.Doc.Block.blockquote
+ #[(LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "I like quotes"]),
+ (LeanDoc.Doc.Block.ul
+ #[{ indent := 2,
+ contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Also with lists in them"]] }])],
+ LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Also, 2 > 3."]]
+ #[]]
+ Lean.HashMap.ofList []
+ Lean.HashMap.ofList []
-/
#guard_msgs in
#eval d
@@ -185,18 +206,21 @@ Here's some code
:::::::
/--
-info: LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "More writing"]
- "More writing"
- none
- #[]
- #[LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "Section 1"]
- "Section 1"
- none
- #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Here's some code"],
- LeanDoc.Doc.Block.code none #[] 0 "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n"]
- #[]]
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "More writing"]
+ "More writing"
+ none
+ #[]
+ #[LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Section 1"]
+ "Section 1"
+ none
+ #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Here's some code"],
+ LeanDoc.Doc.Block.code none #[] 0 "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n"]
+ #[]]
+ Lean.HashMap.ofList []
+ Lean.HashMap.ofList []
-/
#guard_msgs in
#eval e
@@ -216,19 +240,88 @@ Here's some `code`!
:::::::
/--
-info: LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "More code writing"]
- "More code writing"
- none
- #[]
- #[LeanDoc.Doc.Part.mk
- #[LeanDoc.Doc.Inline.text "Section 1"]
- "Section 1"
- none
- #[LeanDoc.Doc.Block.para
- #[LeanDoc.Doc.Inline.text "Here's some ", LeanDoc.Doc.Inline.code "code", LeanDoc.Doc.Inline.text "!"],
- LeanDoc.Doc.Block.code none #[] 0 "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n"]
- #[]]
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "More code writing"]
+ "More code writing"
+ none
+ #[]
+ #[LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Section 1"]
+ "Section 1"
+ none
+ #[LeanDoc.Doc.Block.para
+ #[LeanDoc.Doc.Inline.text "Here's some ", LeanDoc.Doc.Inline.code "code", LeanDoc.Doc.Inline.text "!"],
+ LeanDoc.Doc.Block.code none #[] 0 "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n"]
+ #[]]
+ Lean.HashMap.ofList []
+ Lean.HashMap.ofList []
-/
#guard_msgs in
#eval f
+
+#docs (.none) g "Ref link before" :=
+:::::::
+
+# Section 1
+
+[to here]: http://example.com
+
+Here's [a link][to here]!
+
+:::::::
+
+/--
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Ref link before"]
+ "Ref link before"
+ none
+ #[]
+ #[LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Section 1"]
+ "Section 1"
+ none
+ #[LeanDoc.Doc.Block.para
+ #[LeanDoc.Doc.Inline.text "Here's ",
+ LeanDoc.Doc.Inline.link #[(LeanDoc.Doc.Inline.text "a link")] (LeanDoc.Doc.LinkDest.ref "to here"),
+ LeanDoc.Doc.Inline.text "!"]]
+ #[]]
+ Lean.HashMap.ofList [("to here", "http://example.com")]
+ Lean.HashMap.ofList []
+-/
+#guard_msgs in
+ #eval g
+
+#docs (.none) g' "Ref link after" :=
+:::::::
+
+# Section 1
+
+Here's [a link][to here]!
+
+[to here]: http://example.com
+
+:::::::
+
+/--
+info: LeanDoc.Doc.Doc.mk
+ LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Ref link after"]
+ "Ref link after"
+ none
+ #[]
+ #[LeanDoc.Doc.Part.mk
+ #[LeanDoc.Doc.Inline.text "Section 1"]
+ "Section 1"
+ none
+ #[LeanDoc.Doc.Block.para
+ #[LeanDoc.Doc.Inline.text "Here's ",
+ LeanDoc.Doc.Inline.link #[(LeanDoc.Doc.Inline.text "a link")] (LeanDoc.Doc.LinkDest.ref "to here"),
+ LeanDoc.Doc.Inline.text "!"]]
+ #[]]
+ Lean.HashMap.ofList [("to here", "http://example.com")]
+ Lean.HashMap.ofList []
+-/
+#guard_msgs in
+ #eval g'
diff --git a/src/leandoc/LeanDoc/Parser.lean b/src/leandoc/LeanDoc/Parser.lean
index 83b3a9d..6bedd19 100644
--- a/src/leandoc/LeanDoc/Parser.lean
+++ b/src/leandoc/LeanDoc/Parser.lean
@@ -820,11 +820,17 @@ mutual
partial def link (ctxt : InlineCtxt) :=
nodeFn ``link <|
- (atomicFn (notInLink ctxt >> strFn "[" )) >>
+ (atomicFn (notInLink ctxt >> strFn "[" >> notFollowedByFn (chFn '^') "'^'" )) >>
many1Fn (inline {ctxt with inLink := true}) >>
strFn "]" >>
linkTarget
+ partial def footnote (ctxt : InlineCtxt) :=
+ nodeFn ``footnote <|
+ (atomicFn (notInLink ctxt >> strFn "[^" )) >>
+ nodeFn `str (asStringFn (quoted := true) (many1Fn (satisfyEscFn (· != ']')))) >>
+ strFn "]"
+
partial def linkTarget := ref <|> url
where
notUrlEnd := satisfyEscFn (· ∉ ")\n".toList) >> takeUntilEscFn (· ∈ ")\n".toList)
@@ -857,7 +863,7 @@ mutual
s.pushSyntax fakeClose
- partial def delimitedInline (ctxt : InlineCtxt) : ParserFn := emph ctxt <|> bold ctxt <|> code <|> role ctxt <|> image <|> link ctxt
+ partial def delimitedInline (ctxt : InlineCtxt) : ParserFn := emph ctxt <|> bold ctxt <|> code <|> role ctxt <|> image <|> link ctxt <|> footnote ctxt
partial def inline (ctxt : InlineCtxt) : ParserFn :=
text <|> linebreak ctxt <|> delimitedInline ctxt
@@ -1184,6 +1190,22 @@ All input consumed.
#guard_msgs in
#eval role {} |>.test! "{hello world:=gaia}[there *is* _a meaning!_ ]"
+/--
+info: Success! Final stack:
+ (LeanDoc.Syntax.footnote "[^" (str "\"1\"") "]")
+All input consumed.
+-/
+#guard_msgs in
+#eval footnote {} |>.test! "[^1]"
+
+/--
+info: Success! Final stack:
+ (LeanDoc.Syntax.footnote "[^" (str "\"1\"") "]")
+All input consumed.
+-/
+#guard_msgs in
+#eval inline {} |>.test! "[^1]"
+
structure InList where
indentation : Nat
type : OrderedListType ⊕ UnorderedListType
@@ -1526,9 +1548,22 @@ mutual
eatSpaces := takeWhileFn (· == ' ')
intro := guardMinColumn (ctxt.minIndent) >> withCurrentColumn fun c => atomicFn (chFn '{') >> withCurrentColumn fun c' => nameAndArgs (some c') >> nameArgWhitespace (some c) >> chFn '}'
+ partial def linkRef (c : BlockCtxt) : ParserFn :=
+ nodeFn ``link_ref <|
+ atomicFn (ignoreFn (bol >> eatSpaces >> guardMinColumn c.minIndent) >> chFn '[' >> nodeFn strLitKind (asStringFn (quoted := true) (satisfyEscFn nameStart >> manyFn (satisfyEscFn (· != ']')))) >> strFn "]:") >>
+ eatSpaces >>
+ nodeFn strLitKind (asStringFn (quoted := true) (takeWhileFn (· != '\n'))) >>
+ ignoreFn (satisfyFn (· == '\n') "newline" <|> eoiFn)
+ where nameStart c := c != ']' && c != '^'
+
+ partial def footnoteRef (c : BlockCtxt) : ParserFn :=
+ nodeFn ``footnote_ref <|
+ atomicFn (ignoreFn (bol >> eatSpaces >> guardMinColumn c.minIndent) >> strFn "[^" >> nodeFn strLitKind (asStringFn (quoted := true) (many1Fn (satisfyEscFn (· != ']')))) >> strFn "]:") >>
+ eatSpaces >>
+ notFollowedByFn blockOpener "block opener" >> guardMinColumn c.minIndent >> textLine
partial def block (c : BlockCtxt) : ParserFn :=
- block_role c <|> unorderedList c <|> orderedList c <|> definitionList c <|> header c <|> codeBlock c <|> directive c <|> blockquote c <|> para c
+ block_role c <|> unorderedList c <|> orderedList c <|> definitionList c <|> header c <|> codeBlock c <|> directive c <|> blockquote c <|> linkRef c <|> footnoteRef c <|> para c
partial def blocks (c : BlockCtxt) : ParserFn := sepByFn true (block c) (ignoreFn (manyFn blankLine))
@@ -1725,7 +1760,7 @@ All input consumed.
#eval blocks {} |>.test! "* foo\n * bar\n* more outer"
/--
-info: Failure: unexpected end of input; expected ![, [ or expected beginning of line at ⟨2, 15⟩
+info: Failure: unexpected end of input; expected ![, [, [^ or expected beginning of line at ⟨2, 15⟩
Final stack:
[(LeanDoc.Syntax.dl
[(LeanDoc.Syntax.desc
@@ -1737,7 +1772,7 @@ Final stack:
(str "\"Let's say more!\""))]
"=>"
[(LeanDoc.Syntax.para
- [(LeanDoc.Syntax.link )])
+ [(LeanDoc.Syntax.footnote )])
])])]
Remaining: ""
-/
@@ -2273,7 +2308,7 @@ All input consumed.
#guard_msgs in
#eval block {} |>.test! "{\n test\n arg}\nHere's a modified paragraph."
/--
-info: Failure: '{'; expected ![, *, +, - or [
+info: Failure: '{'; expected ![, *, +, -, [ or [^
Final stack:
(LeanDoc.Syntax.block_role
"{"
@@ -2281,7 +2316,7 @@ Final stack:
[(arg.anon `arg)]
"}"
(LeanDoc.Syntax.para
- [(LeanDoc.Syntax.link )]))
+ [(LeanDoc.Syntax.footnote )]))
Remaining: "\n\nHere's a modified paragraph."
-/
#guard_msgs in
@@ -2400,3 +2435,91 @@ All input consumed.
-/
#guard_msgs in
#eval blocks {} |>.test! "[\\[link A\\]](https://example.com) [\\[link B\\]](https://more.example.com)"
+
+
+/--
+info: Success! Final stack:
+ [(LeanDoc.Syntax.para
+ [(LeanDoc.Syntax.link
+ "["
+ [(LeanDoc.Syntax.text (str "\"My link\""))]
+ "]"
+ (LeanDoc.Syntax.ref
+ "["
+ (str "\"lean\"")
+ "]"))])
+ (LeanDoc.Syntax.link_ref
+ "["
+ (str "\"lean\"")
+ "]:"
+ (str "\"https://lean-lang.org\""))]
+All input consumed.
+-/
+#guard_msgs in
+ #eval blocks {} |>.test! "[My link][lean]\n\n[lean]: https://lean-lang.org"
+
+/--
+info: Failure: expected ( or [
+Final stack:
+ [(LeanDoc.Syntax.para
+ [(LeanDoc.Syntax.link
+ "["
+ [(LeanDoc.Syntax.text (str "\"My link\""))]
+ "]"
+ (LeanDoc.Syntax.ref
+ "["
+ (str "\"lean\"")
+ "]"))
+ (LeanDoc.Syntax.linebreak "\n")
+ (LeanDoc.Syntax.link
+ "["
+ [(LeanDoc.Syntax.text (str "\"lean\""))]
+ "]"
+ (LeanDoc.Syntax.url ))])]
+Remaining: ": https://lean-lang.org"
+-/
+-- NB this is correct - blank lines are required here
+#guard_msgs in
+ #eval blocks {} |>.test! "[My link][lean]\n[lean]: https://lean-lang.org"
+
+/--
+info: Success! Final stack:
+ [(LeanDoc.Syntax.para
+ [(LeanDoc.Syntax.link
+ "["
+ [(LeanDoc.Syntax.text (str "\"My link\""))]
+ "]"
+ (LeanDoc.Syntax.ref
+ "["
+ (str "\"lean\"")
+ "]"))])
+ (LeanDoc.Syntax.link_ref
+ "["
+ (str "\"lean\"")
+ "]:"
+ (str "\"https://lean-lang.org\""))
+ (LeanDoc.Syntax.para
+ [(LeanDoc.Syntax.text (str "\"hello\""))])]
+All input consumed.
+-/
+#guard_msgs in
+ #eval blocks {} |>.test! "[My link][lean]\n\n[lean]: https://lean-lang.org\nhello"
+
+/--
+info: Success! Final stack:
+ [(LeanDoc.Syntax.para
+ [(LeanDoc.Syntax.text (str "\"Blah blah\""))
+ (LeanDoc.Syntax.footnote
+ "[^"
+ (str "\"1\"")
+ "]")])
+ (LeanDoc.Syntax.footnote_ref
+ "[^"
+ (str "\"1\"")
+ "]:"
+ [(LeanDoc.Syntax.text
+ (str "\"More can be said\""))])]
+All input consumed.
+-/
+#guard_msgs in
+ #eval blocks {} |>.test! "Blah blah[^1]\n\n[^1]: More can be said"
diff --git a/src/leandoc/LeanDoc/Syntax.lean b/src/leandoc/LeanDoc/Syntax.lean
index 4e65eff..e61a39c 100644
--- a/src/leandoc/LeanDoc/Syntax.lean
+++ b/src/leandoc/LeanDoc/Syntax.lean
@@ -31,6 +31,8 @@ syntax (name:=bold) "*{" inline* "}" : inline
syntax (name:=link) "link[" inline* "]" link_target : inline
/-- Image -/
syntax (name:=image) "image[" str* "]" link_target : inline
+/-- A footnote use -/
+syntax (name:=footnote) "[^" str "]" : inline
/-- Line break -/
syntax (name:=linebreak) "line!" : inline
/-- Literal characters-/
@@ -56,23 +58,13 @@ syntax (name:=ol) "ol{" num list_item* "}" : block
syntax (name:=codeblock) str : block
/-- Quotation -/
syntax (name:=blockquote) str : block
+/-- A link reference definition -/
+syntax (name:=link_ref) "[" str "]:" str : block
+/-- A footnote definition -/
+syntax (name:=footnote_ref) "[^" str "]:" inline* : block
/-- Custom directive -/
syntax (name:=directive) "directive{" ident argument* "}" "[" block* "]": block
/-- A header -/
syntax (name:=header) inline* : block
syntax (name:=block_role) "role{" ident argument* "}" "[" block "]" : block
-
-
-open LeanDoc.SyntaxUtils Lean Elab Term Std in
-macro "#seeStx" tm:term : command =>
- `(#eval (ppSyntax <$> $tm : TermElabM Std.Format) )
-
-#seeStx `(inline| "foo")
-#seeStx `(inline| _{ "foo" "bar" })
-#seeStx `(inline| *{ "foo" "bar" })
-#seeStx `(inline| link[_{"FPiL" line! "book"}]("https://..."))
-#seeStx `(inline| code{ "foo" })
-
-
-end LeanDoc.Syntax