diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index 0a05403..0aa9444 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -10,8 +10,8 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do let name := i.name.toString return
  • {shortName} : [←infoFormatToHtml i.type]
    • -def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do - #[Html.element "ul" false #[("class", "constructors")] (←i.ctors.toArray.mapM ctorToHtml)] +def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := + return #[] end Output end DocGen4 diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 6a2e07a..fee4598 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -13,16 +13,10 @@ namespace Output open Lean open scoped DocGen4.Jsx -def moduleListFile (file : Name) : HtmlM Html := do - let attributes := match ←getCurrentName with - | some name => - if file == name then - #[("class", "nav_link"), ("visible", "")] - else - #[("class", "nav_link")] - | none => #[("class", "nav_link")] - let nodes := #[{file.toString}] - return Html.element "div" false attributes nodes +def moduleListFile (file : Name) : HtmlM Html := + return
    + {file.toString} +
    partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) @@ -31,24 +25,19 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let dirNodes ← (dirs.mapM moduleListDir) let fileNodes ← (files.mapM moduleListFile) let moduleLink ← moduleNameToLink h.getName - let attributes := match ←getCurrentName with - | some name => - if h.getName.isPrefixOf name then - #[("class", "nav_sect"), ("data-path", moduleLink), ("open", "")] - else - #[("class", "nav_sect"), ("data-path", moduleLink)] - | none => - #[("class", "nav_sect"), ("data-path", moduleLink)] - let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes - return Html.element "details" false attributes nodes + return
    + {h.getName.toString} + [dirNodes] + [fileNodes] +
    -def moduleList : HtmlM (Array Html) := do +def moduleList : HtmlM Html := do let hierarchy := (←getResult).hierarchy let mut list := Array.empty for (n, cs) in hierarchy.getChildren do - list := list.push

    {n.toString}

    list := list.push $ ←moduleListDir cs - list + return
    [list]
    def navbar : HtmlM Html := do end Output diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index e0fbfaf..253de07 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -53,9 +53,6 @@ open Parser PrettyPrinter declare_syntax_cat jsxElement declare_syntax_cat jsxChild -def jsxAttrVal : Parser := strLit <|> group ("{" >> termParser >> "}") -def jsxAttr : Parser := ident >> "=" >> jsxAttrVal - -- JSXTextCharacter : SourceCharacter but not one of {, <, > or } def jsxText : Parser := withAntiquot (mkAntiquot "jsxText" `jsxText) { @@ -67,41 +64,57 @@ def jsxText : Parser := @[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure () @[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure () -scoped syntax "<" ident jsxAttr* "/>" : jsxElement -scoped syntax "<" ident jsxAttr* ">" jsxChild* "" : jsxElement +syntax jsxAttrName := ident <|> strLit +syntax jsxAttrVal := strLit <|> group("{" term "}") +syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal +syntax jsxAttrSpread := "[" term "]" +syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread -scoped syntax jsxText : jsxChild -scoped syntax "{" term "}" : jsxChild -scoped syntax "[" term "]" : jsxChild -scoped syntax jsxElement : jsxChild +syntax "<" ident jsxAttr* "/>" : jsxElement +syntax "<" ident jsxAttr* ">" jsxChild* "" : jsxElement + +syntax jsxText : jsxChild +syntax "{" term "}" : jsxChild +syntax "[" term "]" : jsxChild +syntax jsxElement : jsxChild scoped syntax:max jsxElement : term +def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do + let mut as ← `(#[]) + for attr in attrs do + as ← match attr with + | `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) => + let n ← match n with + | `(jsxAttrName| $n:strLit) => n + | `(jsxAttrName| $n:ident) => quote (toString n.getId) + | _ => Macro.throwUnsupported + let v ← match v with + | `(jsxAttrVal| {$v}) => v + | `(jsxAttrVal| $v:strLit) => v + | _ => Macro.throwUnsupported + `(($as).push ($n, ($v : String))) + | `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String))) + | _ => Macro.throwUnsupported + return as + macro_rules - | `(<$n $[$ns = $vs]* />) => - let ns := ns.map (quote <| toString ·.getId) - let vs := vs.map fun - | `(jsxAttrVal| $s:strLit) => s - | `(jsxAttrVal| { $t:term }) => t - | _ => unreachable! - `(Html.element $(quote <| toString n.getId) false #[ $[($ns, $vs)],* ] #[]) - | `(<$n $[$ns = $vs]* >$cs*) => - if n.getId == m.getId then do - let ns := ns.map (quote <| toString ·.getId) - let vs := vs.map fun - | `(jsxAttrVal| $s:strLit) => s - | `(jsxAttrVal| { $t:term }) => t - | _ => unreachable! - let cs ← cs.mapM fun - | `(jsxChild|$t:jsxText) => `(#[Html.text $(quote t[0].getAtomVal!)]) - -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t` - | `(jsxChild|{$t}) => `(#[$t]) - | `(jsxChild|[$t]) => `($t) - | `(jsxChild|$e:jsxElement) => `(#[$e:jsxElement]) - | _ => unreachable! - let tag := toString n.getId - `(Html.element $(quote tag) false #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ])) - else Macro.throwError ("expected ") + | `(<$n $attrs* />) => do + `(Html.element $(quote (toString n.getId)) true $(← translateAttrs attrs) #[]) + | `(<$n $attrs* >$children*) => do + unless n.getId == m.getId do + withRef m <| Macro.throwError s!"expected " + let mut cs ← `(#[]) + for child in children do + cs ← match child with + | `(jsxChild|$t:jsxText) => `(($cs).push (Html.text $(quote t[0].getAtomVal!))) + -- TODO(WN): elab as list of children if type is `t Html` where `Foldable t` + | `(jsxChild|{$t}) => `(($cs).push ($t : Html)) + | `(jsxChild|[$t]) => `($cs ++ ($t : Array Html)) + | `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html)) + | _ => Macro.throwUnsupported + let tag := toString n.getId + `(Html.element $(quote tag) false $(← translateAttrs attrs) $cs) end Jsx diff --git a/Main.lean b/Main.lean index 7f527a4..13e530b 100644 --- a/Main.lean +++ b/Main.lean @@ -4,6 +4,10 @@ import Lean open DocGen4 Lean IO def main (args : List String) : IO Unit := do + if args.isEmpty then + IO.println "Usage: doc-gen4 root/url/ Module1 Module2 ..." + IO.Process.exit 1 + return let root := args.head! let modules := args.tail! let path ← lakeSetupSearchPath (←getLakePath) modules.toArray diff --git a/static/style.css b/static/style.css index 727ba48..958eb2f 100644 --- a/static/style.css +++ b/static/style.css @@ -268,6 +268,11 @@ nav { margin-bottom: 1ex; } +/* top-level modules in left navbar */ +.nav .module_list > details { + margin-top: 1ex; +} + .nav details > * { padding-left: 2ex; } @@ -287,10 +292,6 @@ nav { margin-block-end: 4px; } -.nav h4 { - margin-bottom: 1ex; -} - /* People use way too long declaration names. */ .internal_nav, .decl_name { overflow-wrap: break-word;