chore: split blog genre into independent library

leanprover · Dec 6, 2023 · 2ff3351 · 2ff3351
1 parent 558ae83
commit 2ff3351
Show file tree

Hide file tree

Showing 42 changed files with 58 additions and 59 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -1,5 +1,4 @@
 import BlogContents
-import LeanDoc
 
 open LeanDoc.Genre.Blog
 

diff --git a/LeanDoc/Basic.lean b/LeanDoc/Basic.lean
diff --git a/LeanDoc/Genre/Blog.lean b/LeanDoc/Genre/Blog.lean
diff --git 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
@@ -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 → src/leanblog/LeanDoc/Genre/Blog.lean b/LeanDoc/Genre.lean → 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 → src/leanblog/LeanDoc/Genre/Blog/Basic.lean b/LeanDoc/Genre/Blog/Basic.lean → src/leanblog/LeanDoc/Genre/Blog/Basic.lean
diff --git a/LeanDoc/Genre/Blog/Generate.lean → ...leanblog/LeanDoc/Genre/Blog/Generate.lean b/LeanDoc/Genre/Blog/Generate.lean → ...leanblog/LeanDoc/Genre/Blog/Generate.lean
diff --git a/LeanDoc/Genre/Blog/HighlightCode.lean → ...log/LeanDoc/Genre/Blog/HighlightCode.lean b/LeanDoc/Genre/Blog/HighlightCode.lean → ...log/LeanDoc/Genre/Blog/HighlightCode.lean
diff --git a/LeanDoc/Genre/Blog/Highlighted.lean → ...nblog/LeanDoc/Genre/Blog/Highlighted.lean b/LeanDoc/Genre/Blog/Highlighted.lean → ...nblog/LeanDoc/Genre/Blog/Highlighted.lean
diff --git a/LeanDoc/Genre/Blog/Site.lean → src/leanblog/LeanDoc/Genre/Blog/Site.lean b/LeanDoc/Genre/Blog/Site.lean → src/leanblog/LeanDoc/Genre/Blog/Site.lean
diff --git a/LeanDoc/Genre/Blog/Site/Syntax.lean → ...nblog/LeanDoc/Genre/Blog/Site/Syntax.lean b/LeanDoc/Genre/Blog/Site/Syntax.lean → ...nblog/LeanDoc/Genre/Blog/Site/Syntax.lean
diff --git a/LeanDoc/Genre/Blog/Template.lean → ...leanblog/LeanDoc/Genre/Blog/Template.lean b/LeanDoc/Genre/Blog/Template.lean → ...leanblog/LeanDoc/Genre/Blog/Template.lean
diff --git a/LeanDoc/Genre/Blog/Theme.lean → src/leanblog/LeanDoc/Genre/Blog/Theme.lean b/LeanDoc/Genre/Blog/Theme.lean → src/leanblog/LeanDoc/Genre/Blog/Theme.lean
diff --git a/LeanDoc.lean → src/leandoc/LeanDoc.lean b/LeanDoc.lean → src/leandoc/LeanDoc.lean
@@ -1,11 +1,10 @@
--- 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
 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
@@ -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 → src/leandoc/LeanDoc/Doc.lean b/LeanDoc/Doc.lean → src/leandoc/LeanDoc/Doc.lean
diff --git a/LeanDoc/Doc/Concrete.lean → src/leandoc/LeanDoc/Doc/Concrete.lean b/LeanDoc/Doc/Concrete.lean → src/leandoc/LeanDoc/Doc/Concrete.lean
diff --git a/LeanDoc/Doc/Elab.lean → src/leandoc/LeanDoc/Doc/Elab.lean b/LeanDoc/Doc/Elab.lean → src/leandoc/LeanDoc/Doc/Elab.lean
diff --git a/LeanDoc/Doc/Elab/ExpanderAttribute.lean → ...c/LeanDoc/Doc/Elab/ExpanderAttribute.lean b/LeanDoc/Doc/Elab/ExpanderAttribute.lean → ...c/LeanDoc/Doc/Elab/ExpanderAttribute.lean
diff --git a/LeanDoc/Doc/Elab/InlineString.lean → ...eandoc/LeanDoc/Doc/Elab/InlineString.lean b/LeanDoc/Doc/Elab/InlineString.lean → ...eandoc/LeanDoc/Doc/Elab/InlineString.lean
diff --git a/LeanDoc/Doc/Elab/Monad.lean → src/leandoc/LeanDoc/Doc/Elab/Monad.lean b/LeanDoc/Doc/Elab/Monad.lean → src/leandoc/LeanDoc/Doc/Elab/Monad.lean
diff --git a/LeanDoc/Doc/Html.lean → src/leandoc/LeanDoc/Doc/Html.lean b/LeanDoc/Doc/Html.lean → src/leandoc/LeanDoc/Doc/Html.lean
diff --git a/LeanDoc/Doc/Lsp.lean → src/leandoc/LeanDoc/Doc/Lsp.lean b/LeanDoc/Doc/Lsp.lean → src/leandoc/LeanDoc/Doc/Lsp.lean
diff --git a/LeanDoc/Examples.lean → src/leandoc/LeanDoc/Examples.lean b/LeanDoc/Examples.lean → src/leandoc/LeanDoc/Examples.lean
diff --git a/LeanDoc/Method.lean → src/leandoc/LeanDoc/Method.lean b/LeanDoc/Method.lean → src/leandoc/LeanDoc/Method.lean
diff --git a/LeanDoc/Output.lean → src/leandoc/LeanDoc/Output.lean b/LeanDoc/Output.lean → src/leandoc/LeanDoc/Output.lean
diff --git a/LeanDoc/Output/Html.lean → src/leandoc/LeanDoc/Output/Html.lean b/LeanDoc/Output/Html.lean → src/leandoc/LeanDoc/Output/Html.lean
diff --git a/LeanDoc/Parser.lean → src/leandoc/LeanDoc/Parser.lean b/LeanDoc/Parser.lean → src/leandoc/LeanDoc/Parser.lean
diff --git a/LeanDoc/Parser/Lean.lean → src/leandoc/LeanDoc/Parser/Lean.lean b/LeanDoc/Parser/Lean.lean → src/leandoc/LeanDoc/Parser/Lean.lean
diff --git a/LeanDoc/Syntax.lean → src/leandoc/LeanDoc/Syntax.lean b/LeanDoc/Syntax.lean → src/leandoc/LeanDoc/Syntax.lean
diff --git a/LeanDoc/SyntaxUtils.lean → src/leandoc/LeanDoc/SyntaxUtils.lean b/LeanDoc/SyntaxUtils.lean → src/leandoc/LeanDoc/SyntaxUtils.lean