diff --git a/BlogContents.lean b/BlogContents.lean index ee0c363..4b95008 100644 --- a/BlogContents.lean +++ b/BlogContents.lean @@ -1,6 +1,5 @@ -import LeanDoc import LeanDoc.Doc.Html -import LeanDoc.Genre +import LeanDoc.Genre.Blog import BlogContents.Pages.Front import BlogContents.Pages.Mission diff --git a/BlogContents/Pages/Blog.lean b/BlogContents/Pages/Blog.lean index 8042888..dc3c679 100644 --- a/BlogContents/Pages/Blog.lean +++ b/BlogContents/Pages/Blog.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre (Blog) open LeanDoc.Genre.Blog (page_link) diff --git a/BlogContents/Pages/Contact.lean b/BlogContents/Pages/Contact.lean index d0258ea..1ff10d8 100644 --- a/BlogContents/Pages/Contact.lean +++ b/BlogContents/Pages/Contact.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre (Blog) diff --git a/BlogContents/Pages/Front.lean b/BlogContents/Pages/Front.lean index 5b3857f..629b984 100644 --- a/BlogContents/Pages/Front.lean +++ b/BlogContents/Pages/Front.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre (Blog) diff --git a/BlogContents/Pages/Links.lean b/BlogContents/Pages/Links.lean index c7d5524..77b60b8 100644 --- a/BlogContents/Pages/Links.lean +++ b/BlogContents/Pages/Links.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre (Blog) open LeanDoc.Genre.Blog (page_link) diff --git a/BlogContents/Pages/Mission.lean b/BlogContents/Pages/Mission.lean index 421091b..7329c5e 100644 --- a/BlogContents/Pages/Mission.lean +++ b/BlogContents/Pages/Mission.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre (Blog) open LeanDoc.Genre.Blog (page_link) diff --git a/BlogContents/Pages/Roadmap.lean b/BlogContents/Pages/Roadmap.lean index 3cbd3b1..17274bf 100644 --- a/BlogContents/Pages/Roadmap.lean +++ b/BlogContents/Pages/Roadmap.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre (Blog) diff --git a/BlogContents/Pages/Team.lean b/BlogContents/Pages/Team.lean index e09f832..194a741 100644 --- a/BlogContents/Pages/Team.lean +++ b/BlogContents/Pages/Team.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre (Blog) open LeanDoc.Genre.Blog (page_link htmlSpan htmlDiv blob) diff --git a/BlogContents/Posts/AnExcellentPost.lean b/BlogContents/Posts/AnExcellentPost.lean index 87fa6be..33e20ef 100644 --- a/BlogContents/Posts/AnExcellentPost.lean +++ b/BlogContents/Posts/AnExcellentPost.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre diff --git a/BlogContents/Posts/AnotherPost.lean b/BlogContents/Posts/AnotherPost.lean index 5ae69e4..4913751 100644 --- a/BlogContents/Posts/AnotherPost.lean +++ b/BlogContents/Posts/AnotherPost.lean @@ -1,4 +1,4 @@ -import LeanDoc +import LeanDoc.Genre.Blog open LeanDoc.Genre open LeanDoc.Genre.Blog (label ref lean leanInit) @@ -83,8 +83,8 @@ Pellentesque dapibus suscipit ligula. Donec posuere augue in quam. Etiam vel t Pellentesque dapibus suscipit ligula. Donec posuere augue in quam. Etiam vel tortor sodales tellus ultricies commodo. Suspendisse potenti. Aenean in sem ac leo mollis blandit. Donec neque quam, dignissim in, mollis nec, sagittis eu, wisi. Phasellus lacus. Etiam laoreet quam sed arcu. Phasellus at dui in ligula mollis ultricies. Integer placerat tristique nisl. Praesent augue. Fusce commodo. Vestibulum convallis, lorem a tempus semper, dui dui euismod elit, vitae placerat urna tortor vitae lacus. Nullam libero mauris, consequat quis, varius et, dictum id, arcu. Mauris mollis tincidunt felis. Aliquam feugiat tellus ut neque. Nulla facilisis, risus a rhoncus fermentum, tellus tellus lacinia purus, et dictum nunc justo sit amet elit. -* Praesent fermentum tempor tellus. -* Pellentesque tristique imperdiet tortor. -* Nam euismod tellus id erat. -* Lorem ipsum dolor sit amet, consectetuer adipiscing elit. -* Nullam tempus. +1. Praesent fermentum tempor tellus. +2. Pellentesque tristique imperdiet tortor. +3. Nam euismod tellus id erat. +4. Lorem ipsum dolor sit amet, consectetuer adipiscing elit. +5. Nullam tempus. diff --git a/DemoBlog.lean b/DemoBlog.lean index 18c5da4..6a2bc92 100644 --- a/DemoBlog.lean +++ b/DemoBlog.lean @@ -1,5 +1,4 @@ import BlogContents -import LeanDoc open LeanDoc.Genre.Blog diff --git a/LeanDoc/Basic.lean b/LeanDoc/Basic.lean deleted file mode 100644 index 9d28725..0000000 --- a/LeanDoc/Basic.lean +++ /dev/null @@ -1,7 +0,0 @@ -/- -Copyright (c) 2023 Lean FRO LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: David Thrane Christiansen --/ - -def hello := "world" diff --git a/LeanDoc/Genre/Blog.lean b/LeanDoc/Genre/Blog.lean deleted file mode 100644 index 8c3f8ef..0000000 --- a/LeanDoc/Genre/Blog.lean +++ /dev/null @@ -1,5 +0,0 @@ -import LeanDoc.Genre.Blog.Basic -import LeanDoc.Genre.Blog.Generate -import LeanDoc.Genre.Blog.Site -import LeanDoc.Genre.Blog.Template -import LeanDoc.Genre.Blog.Theme diff --git a/Main.lean b/Main.lean index ca58b36..1dc5ed6 100644 --- a/Main.lean +++ b/Main.lean @@ -3,7 +3,11 @@ Copyright (c) 2023 Lean FRO LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: David Thrane Christiansen -/ -import LeanDoc +import LeanDoc.Doc.Elab +import LeanDoc.Doc.Html +import LeanDoc.Output +import LeanDoc.Output.Html +import LeanDoc.Doc.Concrete open LeanDoc Doc Output Html Concrete ToHtml Elab Monad open Lean Elab Term diff --git a/lakefile.lean b/lakefile.lean index ded605e..232d712 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,9 +6,15 @@ require std from git "https://github.com/leanprover/std4" @ "main" package «leandoc» where -- add package configuration options here -lean_lib «LeanDoc» where +lean_lib LeanDoc where + srcDir := "src/leandoc" + roots := #[`LeanDoc.Doc, `LeanDoc.Output, `LeanDoc.Parser, `LeanDoc.Examples, `LeanDoc.Method, `LeanDoc.Syntax, `LeanDoc.SyntaxUtils] -- add library configuration options here +lean_lib LeanBlog where + srcDir := "src/leanblog" + roots := #[`LeanDoc.Genre.Blog] + @[default_target] lean_exe «leandoc» where root := `Main diff --git a/LeanDoc/Genre.lean b/src/leanblog/LeanDoc/Genre/Blog.lean similarity index 96% rename from LeanDoc/Genre.lean rename to src/leanblog/LeanDoc/Genre/Blog.lean index a05bc97..50f9232 100644 --- a/LeanDoc/Genre.lean +++ b/src/leanblog/LeanDoc/Genre/Blog.lean @@ -1,27 +1,15 @@ -import Lean.Data.RBMap - -import LeanDoc.Doc -import LeanDoc.Doc.Html - -import LeanDoc.Genre.Blog +import LeanDoc.Genre.Blog.Basic +import LeanDoc.Genre.Blog.Generate +import LeanDoc.Genre.Blog.Highlighted import LeanDoc.Genre.Blog.HighlightCode +import LeanDoc.Genre.Blog.Site import LeanDoc.Genre.Blog.Site.Syntax - -import LeanDoc.Output.Html - - -open LeanDoc.Doc (Genre Part) -open LeanDoc.Doc.Html - -namespace LeanDoc.Genre - - -namespace Blog - +import LeanDoc.Genre.Blog.Template +import LeanDoc.Genre.Blog.Theme open LeanDoc.Output Html open Lean (RBMap) -section +namespace LeanDoc.Genre.Blog open Lean Elab open LeanDoc Doc Elab @@ -158,8 +146,6 @@ def lean : CodeBlockExpander pure #[← ``(Block.other (Blog.BlockExt.highlightedCode $(quote x.getId) $(quote hls)) #[Block.code none #[] 0 $(quote str.getString)])] | otherArgs, str => throwErrorAt str "Unexpected arguments {repr otherArgs}" -end - private def filterString (p : Char → Bool) (str : String) : String := Id.run <| do let mut out := "" for c in str.toList do @@ -183,8 +169,3 @@ where | ("--drafts"::more) => opts {cfg with showDrafts := true} more | (other :: _) => throw (↑ s!"Unknown option {other}") | [] => pure cfg - -end Blog -namespace Manual - -end Manual diff --git a/LeanDoc/Genre/Blog/Basic.lean b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean similarity index 100% rename from LeanDoc/Genre/Blog/Basic.lean rename to src/leanblog/LeanDoc/Genre/Blog/Basic.lean diff --git a/LeanDoc/Genre/Blog/Generate.lean b/src/leanblog/LeanDoc/Genre/Blog/Generate.lean similarity index 100% rename from LeanDoc/Genre/Blog/Generate.lean rename to src/leanblog/LeanDoc/Genre/Blog/Generate.lean diff --git a/LeanDoc/Genre/Blog/HighlightCode.lean b/src/leanblog/LeanDoc/Genre/Blog/HighlightCode.lean similarity index 100% rename from LeanDoc/Genre/Blog/HighlightCode.lean rename to src/leanblog/LeanDoc/Genre/Blog/HighlightCode.lean diff --git a/LeanDoc/Genre/Blog/Highlighted.lean b/src/leanblog/LeanDoc/Genre/Blog/Highlighted.lean similarity index 100% rename from LeanDoc/Genre/Blog/Highlighted.lean rename to src/leanblog/LeanDoc/Genre/Blog/Highlighted.lean diff --git a/LeanDoc/Genre/Blog/Site.lean b/src/leanblog/LeanDoc/Genre/Blog/Site.lean similarity index 100% rename from LeanDoc/Genre/Blog/Site.lean rename to src/leanblog/LeanDoc/Genre/Blog/Site.lean diff --git a/LeanDoc/Genre/Blog/Site/Syntax.lean b/src/leanblog/LeanDoc/Genre/Blog/Site/Syntax.lean similarity index 100% rename from LeanDoc/Genre/Blog/Site/Syntax.lean rename to src/leanblog/LeanDoc/Genre/Blog/Site/Syntax.lean diff --git a/LeanDoc/Genre/Blog/Template.lean b/src/leanblog/LeanDoc/Genre/Blog/Template.lean similarity index 100% rename from LeanDoc/Genre/Blog/Template.lean rename to src/leanblog/LeanDoc/Genre/Blog/Template.lean diff --git a/LeanDoc/Genre/Blog/Theme.lean b/src/leanblog/LeanDoc/Genre/Blog/Theme.lean similarity index 100% rename from LeanDoc/Genre/Blog/Theme.lean rename to src/leanblog/LeanDoc/Genre/Blog/Theme.lean diff --git a/LeanDoc.lean b/src/leandoc/LeanDoc.lean similarity index 76% rename from LeanDoc.lean rename to src/leandoc/LeanDoc.lean index ffbdee8..4011db8 100644 --- a/LeanDoc.lean +++ b/src/leandoc/LeanDoc.lean @@ -1,4 +1,4 @@ --- This module serves as the root of the `Leandoc` library. +-- This module serves as the root of the `LeanDoc` library. -- Import modules here that should be built as part of the library. import LeanDoc.Basic import LeanDoc.Doc.Concrete @@ -6,6 +6,5 @@ import LeanDoc.Doc.Elab import LeanDoc.Doc.Elab.Monad import LeanDoc.Doc.Html import LeanDoc.Doc.Lsp -import LeanDoc.Genre import LeanDoc.Parser import LeanDoc.Output.Html diff --git a/src/leandoc/LeanDoc/Build.lean b/src/leandoc/LeanDoc/Build.lean new file mode 100644 index 0000000..1930e8e --- /dev/null +++ b/src/leandoc/LeanDoc/Build.lean @@ -0,0 +1,23 @@ +import Lean + +import LeanDoc.Doc + +namespace LeanDoc.Build + +namespace Traverse +-- In the traverse pass, we propagate information between nodes in the +-- document Additionally, nodes may transform themselves in response +-- to the information that's been gained. + +-- A given genre will fix its type of traversal values. Additionally, +-- all genres support dynamically-typed entries to facilitate +-- cross-genre libraries. + +structure TraversalState.{u} where + Value : Type u + contents : Lean.RBMap String (Value ⊕ Dynamic) compare + + + + +end Traverse diff --git a/LeanDoc/Doc.lean b/src/leandoc/LeanDoc/Doc.lean similarity index 100% rename from LeanDoc/Doc.lean rename to src/leandoc/LeanDoc/Doc.lean diff --git a/LeanDoc/Doc/Concrete.lean b/src/leandoc/LeanDoc/Doc/Concrete.lean similarity index 100% rename from LeanDoc/Doc/Concrete.lean rename to src/leandoc/LeanDoc/Doc/Concrete.lean diff --git a/LeanDoc/Doc/Elab.lean b/src/leandoc/LeanDoc/Doc/Elab.lean similarity index 100% rename from LeanDoc/Doc/Elab.lean rename to src/leandoc/LeanDoc/Doc/Elab.lean diff --git a/LeanDoc/Doc/Elab/ExpanderAttribute.lean b/src/leandoc/LeanDoc/Doc/Elab/ExpanderAttribute.lean similarity index 100% rename from LeanDoc/Doc/Elab/ExpanderAttribute.lean rename to src/leandoc/LeanDoc/Doc/Elab/ExpanderAttribute.lean diff --git a/LeanDoc/Doc/Elab/InlineString.lean b/src/leandoc/LeanDoc/Doc/Elab/InlineString.lean similarity index 100% rename from LeanDoc/Doc/Elab/InlineString.lean rename to src/leandoc/LeanDoc/Doc/Elab/InlineString.lean diff --git a/LeanDoc/Doc/Elab/Monad.lean b/src/leandoc/LeanDoc/Doc/Elab/Monad.lean similarity index 100% rename from LeanDoc/Doc/Elab/Monad.lean rename to src/leandoc/LeanDoc/Doc/Elab/Monad.lean diff --git a/LeanDoc/Doc/Html.lean b/src/leandoc/LeanDoc/Doc/Html.lean similarity index 100% rename from LeanDoc/Doc/Html.lean rename to src/leandoc/LeanDoc/Doc/Html.lean diff --git a/LeanDoc/Doc/Lsp.lean b/src/leandoc/LeanDoc/Doc/Lsp.lean similarity index 100% rename from LeanDoc/Doc/Lsp.lean rename to src/leandoc/LeanDoc/Doc/Lsp.lean diff --git a/LeanDoc/Examples.lean b/src/leandoc/LeanDoc/Examples.lean similarity index 100% rename from LeanDoc/Examples.lean rename to src/leandoc/LeanDoc/Examples.lean diff --git a/LeanDoc/Method.lean b/src/leandoc/LeanDoc/Method.lean similarity index 100% rename from LeanDoc/Method.lean rename to src/leandoc/LeanDoc/Method.lean diff --git a/LeanDoc/Output.lean b/src/leandoc/LeanDoc/Output.lean similarity index 100% rename from LeanDoc/Output.lean rename to src/leandoc/LeanDoc/Output.lean diff --git a/LeanDoc/Output/Html.lean b/src/leandoc/LeanDoc/Output/Html.lean similarity index 100% rename from LeanDoc/Output/Html.lean rename to src/leandoc/LeanDoc/Output/Html.lean diff --git a/LeanDoc/Parser.lean b/src/leandoc/LeanDoc/Parser.lean similarity index 100% rename from LeanDoc/Parser.lean rename to src/leandoc/LeanDoc/Parser.lean diff --git a/LeanDoc/Parser/Lean.lean b/src/leandoc/LeanDoc/Parser/Lean.lean similarity index 100% rename from LeanDoc/Parser/Lean.lean rename to src/leandoc/LeanDoc/Parser/Lean.lean diff --git a/LeanDoc/Syntax.lean b/src/leandoc/LeanDoc/Syntax.lean similarity index 100% rename from LeanDoc/Syntax.lean rename to src/leandoc/LeanDoc/Syntax.lean diff --git a/LeanDoc/SyntaxUtils.lean b/src/leandoc/LeanDoc/SyntaxUtils.lean similarity index 100% rename from LeanDoc/SyntaxUtils.lean rename to src/leandoc/LeanDoc/SyntaxUtils.lean