Skip to content

Commit

Permalink
feat: footnotes and ref-style links
Browse files Browse the repository at this point in the history
  • Loading branch information
@david-christiansen
david-christiansen committed Dec 11, 2023
1 parent a913d09 commit f739898
Show file tree
Hide file tree
Showing 14 changed files with 650 additions and 209 deletions.
9 changes: 8 additions & 1 deletion Main.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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" =>
Expand Down Expand Up @@ -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
7 changes: 2 additions & 5 deletions src/leanblog/LeanDoc/Genre/Blog/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
8 changes: 4 additions & 4 deletions src/leanblog/LeanDoc/Genre/Blog/Generate.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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



Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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 "<!DOCTYPE html>"
Expand Down
8 changes: 4 additions & 4 deletions src/leanblog/LeanDoc/Genre/Blog/Site.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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'}

Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/leanblog/LeanDoc/Genre/Blog/Theme.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,12 +31,12 @@ def dirLinks : Dir Page → TemplateM (Array Html)
| .pages subs =>
subs.filterMapM fun
| .page name _id txt .. =>
pure <| some {{<li><a href={{"/" ++ name}}>{{txt.titleString}}</a></li>}}
pure <| some {{<li><a href={{"/" ++ name}}>{{txt.content.titleString}}</a></li>}}
| .static .. => pure none
| .blog subs =>
subs.mapM fun s => do
let url ← mkLink [(← currentConfig).postName s.date s.content.titleString]
return {{<li><a href={{url}}>{{s.content.titleString}}</a></li>}}
let url ← mkLink [(← currentConfig).postName s.date s.content.content.titleString]
return {{<li><a href={{url}}>{{s.content.content.titleString}}</a></li>}}
where
mkLink dest := do
let dest' ← relative dest
Expand Down Expand Up @@ -91,7 +91,7 @@ def archiveEntry : Template := do
| Date.mk y m d => {{<span class="date"> s!"{y}-{m}-{d}" </span>}}
}}
" — "
<span class="name">{{post.content.titleString}}</span>
<span class="name">{{post.content.content.titleString}}</span>
</a>
</li>
}}]
Expand Down
34 changes: 32 additions & 2 deletions src/leandoc/LeanDoc/Doc.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -54,16 +54,27 @@ 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))

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 :=
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)
48 changes: 37 additions & 11 deletions src/leandoc/LeanDoc/Doc/Concrete.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,14 +51,14 @@ def inlineStr := inStrLit <| textLine
elab "inlines!" s:inlineStr : term => open Lean Elab Term in
match s.raw with
| `<low| [~_ ~(.node _ _ out) ] > => 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*_"
Expand Down Expand Up @@ -89,14 +89,22 @@ elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:docu
let ⟨`<low| [~_ ~(titleName@(.node _ _ titleParts))]>⟩ := 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
Expand All @@ -107,14 +115,23 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : term
let ⟨`<low| [~_ ~(titleName@(.node _ _ titleParts))]>⟩ := 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 =>
Expand All @@ -137,12 +154,21 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : comm
let ⟨`<low| [~_ ~(titleName@(.node _ _ titleParts))]>⟩ := 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)}))
Loading

0 comments on commit f739898

Please sign in to comment.