From 248962aa288ffd3cad7be0d9411032e28f47ba8d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 17 Dec 2024 14:51:27 +0100 Subject: [PATCH] feat: heuristically render Markdown in docstrings Adds a pass to docstring rendering that tries various approaches to get sensible highlighted Lean code, and that makes many examples look better. --- .github/workflows/ci.yml | 3 + doc/UsersGuide/Basic.lean | 22 + src/verso-manual/VersoManual.lean | 2 +- src/verso-manual/VersoManual/Docstring.lean | 659 ++++++++++++++----- src/verso-manual/VersoManual/Html/Style.lean | 1 + src/verso-manual/VersoManual/Markdown.lean | 68 +- src/verso-manual/VersoManual/TeX.lean | 3 + src/verso/Verso/Code/Highlighted.lean | 35 + src/verso/Verso/Doc/Elab/Monad.lean | 7 + src/verso/Verso/Doc/TeX.lean | 2 +- src/verso/Verso/Output/Html.lean | 9 + 11 files changed, 645 insertions(+), 166 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 380ae3a..5e36313 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -92,6 +92,9 @@ jobs: sourcecodepro sourcesanspro sourceserifpro + fvextra + upquote + lineno - name: Check `tlmgr` version run: tlmgr --version diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index da15dfe..fb6a822 100644 --- a/doc/UsersGuide/Basic.lean +++ b/doc/UsersGuide/Basic.lean @@ -53,6 +53,28 @@ results in {docstring List.forM} +## More Docstring Examples + +{docstring Lean.Syntax} + +{docstring List} + +{docstring String} + +{docstring Subtype} + +{docstring OfNat} + +{docstring Monad} + +:::tactic "induction" +::: + +:::tactic "simp" +::: + +{docstring Nat} + # Index %%% number := false diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean index a9d5489..721c8aa 100644 --- a/src/verso-manual/VersoManual.lean +++ b/src/verso-manual/VersoManual.lean @@ -285,7 +285,7 @@ def page (toc : List Html.Toc) (path : Path) (textTitle : String) (htmlTitle con (extraJsFiles := config.extraJs.toArray ++ state.extraJsFiles.map ("/-verso-js/" ++ ·.1)) def Config.relativize (config : Config) (path : Path) (html : Html) : Html := - if let some _ := config.baseURL then + if config.baseURL.isSome then -- Make all absolute URLS be relative to the site root, because that'll make them `base`-relative Html.relativize #[] html else diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 09b2469..37827db 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -71,7 +71,7 @@ def ppName (c : Name) (showUniverses := true) (showNamespace : Bool := true) (op open Lean.PrettyPrinter Delaborator in def ppSignature (c : Name) (showNamespace : Bool := true) (openDecls : List OpenDecl := []) : MetaM FormatWithInfos := - MonadWithReaderOf.withReader (fun (ρ : Core.Context) => {ρ with openDecls := ρ.openDecls ++ openDecls}) <|do + withTheReader Core.Context (fun ρ => {ρ with openDecls := ρ.openDecls ++ openDecls}) <| do let decl ← getConstInfo c let e := .const c (decl.levelParams.map mkLevelParam) let (stx, infos) ← delabCore e (delab := delabConstWithSignature) @@ -147,6 +147,22 @@ structure FieldInfo where docString? : Option String deriving Inhabited, Repr, ToJson, FromJson +open Syntax (mkCApp) in +open BinderInfo in +instance : Quote BinderInfo where + quote + | .default => mkCApp ``BinderInfo.default #[] + | .implicit => mkCApp ``implicit #[] + | .instImplicit => mkCApp ``instImplicit #[] + | .strictImplicit => mkCApp ``strictImplicit #[] + +open Syntax (mkCApp) in +instance : Quote FieldInfo where + quote + | ⟨fieldName, fieldFrom, type, projFn, subobject?, binderInfo, autoParam, docString⟩ => + mkCApp ``FieldInfo.mk #[quote fieldName, quote fieldFrom, quote type, quote projFn, quote subobject?, quote binderInfo, quote autoParam, quote docString] + + open Syntax (mkCApp) in instance : Quote BinderInfo where quote @@ -211,11 +227,9 @@ def DeclType.label : DeclType → String | .inductive _ _ true => "inductive predicate" | other => "" -set_option pp.fullNames false in -#check List.nil open Meta in -def DocName.ofName (c : Name) (showUniverses := true) (showNamespace := true) (openDecls : List OpenDecl := []) : MetaM DocName := do +def DocName.ofName (c : Name) (ppWidth : Nat := 40) (showUniverses := true) (showNamespace := true) (openDecls : List OpenDecl := []) : MetaM DocName := do let env ← getEnv if let some _ := env.find? c then let ctx := { @@ -230,12 +244,13 @@ def DocName.ofName (c : Name) (showUniverses := true) (showNamespace := true) (o let ⟨fmt, infos⟩ ← withOptions (·.setBool `pp.tagAppFns true) <| ppSignature c (showNamespace := showNamespace) (openDecls := openDecls) - let ttSig := Lean.Widget.TaggedText.prettyTagged (w := 40) fmt + + let ttSig := Lean.Widget.TaggedText.prettyTagged (w := ppWidth) fmt let sig := Lean.Widget.tagCodeInfos ctx infos ttSig let ⟨fmt, infos⟩ ← withOptions (·.setBool `pp.tagAppFns true) <| ppName c (showUniverses := showUniverses) (showNamespace := showNamespace) (openDecls := openDecls) - let ttName := Lean.Widget.TaggedText.prettyTagged (w := 40) fmt + let ttName := Lean.Widget.TaggedText.prettyTagged (w := ppWidth) fmt let name := Lean.Widget.tagCodeInfos ctx infos ttName pure ⟨c, ← renderTagged none name ⟨{}, false⟩, ← renderTagged none sig ⟨{}, false⟩, ← findDocString? env c⟩ @@ -327,7 +342,7 @@ def DeclType.ofName (c : Name) : MetaM DeclType := do return .structure (isClass env c) (← DocName.ofName (showNamespace := true) ctor.name) info.fieldNames fieldInfo parents ancestors else - let ctors ← ii.ctors.mapM (DocName.ofName (showNamespace := false) (openDecls := openDecls)) + let ctors ← ii.ctors.mapM (DocName.ofName (ppWidth := 60) (showNamespace := false) (openDecls := openDecls)) let t ← inferType <| .const c (ii.levelParams.map .param) let t' ← reduceAll t return .inductive ctors.toArray (ii.numIndices + ii.numParams) (isPred t') @@ -352,6 +367,26 @@ def docstring (name : Name) (declType : Docstring.DeclType) (signature : Option name := `Verso.Genre.Manual.Block.docstring data := ToJson.toJson (name, declType, signature) +def docstringSection (header : String) : Block where + name := `Verso.Genre.Manual.Block.docstringSection + data := ToJson.toJson header + +def internalSignature (name : Highlighted) (signature : Option Highlighted) : Block where + name := `Verso.Genre.Manual.Block.internalSignature + data := ToJson.toJson (name, signature) + +def fieldSignature (name : Highlighted) (signature : Highlighted) (inheritedFrom : Option Nat) (inheritance : Array Highlighted) : Block where + name := `Verso.Genre.Manual.Block.fieldSignature + data := ToJson.toJson (name, signature, inheritedFrom, inheritance) + +def inheritance (within : Name) (inheritance : Array Block.Docstring.ParentInfo) : Block where + name := `Verso.Genre.Manual.Block.inheritance + data := ToJson.toJson (within, inheritance) + +def constructorSignature (signature : Highlighted) : Block where + name := `Verso.Genre.Manual.Block.constructorSignature + data := ToJson.toJson signature + end Block @@ -416,25 +451,41 @@ def docstringStyle := r#" font-size: inherit; font-weight: bold; } -.namedocs > .text > .constructors { - text-indent: -1ex; + +.namedocs > .text .constructor { + padding-left: 0.5rem; + padding-top: 0; + padding-right: 0; + padding-bottom: 0; + margin-top: 0.5rem; + margin-bottom: 1.5rem; } -.namedocs > .text > .constructors > li { + +.namedocs > .text .constructor::before { + content: '| '; display: block; + font-family: var(--verso-code-font-family); + font-weight: bold; + float: left; + width: 0.5rem; + white-space: pre; } -.namedocs > .text > .constructors > li::before { - content: '|'; - width: 1ex; - display: inline-block; - font-size: larger; + +.namedocs > .text .constructor .name-and-type { + padding-left: 0.5rem; + float: left; + margin-top: 0; } -.namedocs > .text > .constructors > li > .doc { - text-indent: 0; +.namedocs > .text .constructor .docs { + clear: both; + padding-left: 1rem; } + + .namedocs .methods td, .namedocs .fields td { vertical-align: top; } -.namedocs .inheritance td { +.namedocs .inheritance { vertical-align: top; font-size: smaller; font-family: var(--verso-structure-font-family); @@ -470,7 +521,22 @@ def docstringStyle := r#" padding-right: 1rem; } -.namedocs:has(input[data-parent-idx]) tr[data-inherited-from] { +.namedocs .subdocs .name-and-type { + font-size: 1rem; + margin-left: 0; + margin-top: 0; + margin-right: 0; + margin-bottom: 0.5rem; +} + +.namedocs .subdocs .docs { + margin-left: 1.5rem; + margin-top: 0; + margin-right: 0; + margin-bottom: 0.5rem; +} + +.namedocs:has(input[data-parent-idx]) [data-inherited-from] { transition-property: opacity, display; transition-duration: 0.4s; transition-behavior: allow-discrete; @@ -483,21 +549,137 @@ def docstringStyle := r#" str where mkFilterRule (i : Nat) : String := - ".namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]) tr[data-inherited-from=\"" ++ toString i ++ "\"] { + ".namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]) [data-inherited-from=\"" ++ toString i ++ "\"] { display: none; opacity: 0; } -.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked) tr[data-inherited-from=\"" ++ toString i ++"\"] { +.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked) [data-inherited-from=\"" ++ toString i ++"\"] { display: table-row; transform: none; opacity: 1; } -.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked):has(tr.inheritance[data-inherited-from=\"" ++ toString i ++"\"] .parent:hover) tr[data-inherited-from]:not([data-inherited-from=\"" ++ toString i ++"\"]) { +.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked):has(.inheritance[data-inherited-from=\"" ++ toString i ++"\"]:hover) [data-inherited-from]:not([data-inherited-from=\"" ++ toString i ++"\"]) { opacity: 0.5; } " +@[block_extension Block.docstringSection] +def docstringSection.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := some fun _goI goB _id _info contents => contents.mapM goB + toHtml := some fun _goI goB _id info contents => + open Verso.Doc.Html HtmlT in + open Verso.Output Html in do + let .ok header := FromJson.fromJson? (α := String) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty + return {{ +

{{header}}

+ {{← contents.mapM goB}} + }} + +@[block_extension Block.internalSignature] +def internalSignature.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := some fun _goI goB _id _ contents => contents.mapM goB -- TODO + toHtml := some fun _goI goB _id info contents => + open Verso.Doc.Html HtmlT in + open Verso.Output Html in do + let .ok (name, signature) := FromJson.fromJson? (α := Highlighted × Option Highlighted) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty + return {{ +
+ 
+            {{← name.toHtml}}
+            {{← if let some s := signature then do
+                  pure {{" : " {{← s.toHtml}} }}
+                else pure .empty}}
+
+
+ {{← contents.mapM goB}} +
+
+ }} + + + +@[block_extension Block.inheritance] +def inheritance.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := some fun _goI goB _id _ contents => contents.mapM goB -- TODO + toHtml := some fun _goI _goB _id info _contents => + open Verso.Doc.Html HtmlT in + open Verso.Output Html in do + let .ok (name, parents) := FromJson.fromJson? (α := Name × Array Block.Docstring.ParentInfo) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring structure inheritance data while generating HTML"; pure .empty + let parentRow ← do + if parents.isEmpty then pure .empty + else pure {{ + + }} + + +@[block_extension Block.fieldSignature] +def fieldSignature.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := some fun _goI goB _id _ contents => contents.mapM goB -- TODO + toHtml := some fun _goI goB _id info contents => + open Verso.Doc.Html HtmlT in + open Verso.Output Html in do + let .ok (name, signature, inheritedFrom, parents) := FromJson.fromJson? (α := Highlighted × Highlighted × Option Nat × Array Highlighted) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty + let inheritedAttr : Array (String × String) := + inheritedFrom.map (fun i => #[("data-inherited-from", toString i)]) |>.getD #[] + return {{ +
+ 
+            {{← name.toHtml}} " : " {{ ← signature.toHtml}}
+
+ {{← if inheritedFrom.isSome then do + pure {{ +
+ "Inherited from " +
    + {{ ← parents.mapM fun p => do + pure {{
  1. {{ ← p.toHtml }}
    2. }} + }} +
+
}} + else pure .empty}} +
+ {{← contents.mapM goB}} +
+
+ }} + +@[block_extension Block.constructorSignature] +def constructorSignature.descr : BlockDescr where + traverse _ _ _ := pure none + toTeX := some fun _goI goB _id _ contents => contents.mapM goB -- TODO + toHtml := some fun _goI goB _id info contents => + open Verso.Doc.Html HtmlT in + open Verso.Output Html in do + let .ok signature := FromJson.fromJson? (α := Highlighted) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty + + return {{ +
+ 
{{← signature.toHtml}}
+
+ {{← contents.mapM goB}} +
+
+ }} + open Verso.Genre.Manual.Markdown in @[block_extension Block.docstring] def docstring.descr : BlockDescr where @@ -563,7 +745,6 @@ def docstring.descr : BlockDescr where 
{{sig}}
{{← contents.mapM goB}} - {{← moreDeclHtml name goB declType}}
}} @@ -573,120 +754,6 @@ def docstring.descr : BlockDescr where extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] extraCssFiles := [("tippy-border.css", tippy.border.css)] where - md2html (goB) (str : String) : Verso.Doc.Html.HtmlT Manual (ReaderT ExtensionImpls IO) Verso.Output.Html := - open Verso.Doc.Html in - open Verso.Output Html in do - let some md := MD4Lean.parse str - | HtmlT.logError "Markdown parsing failed for {str}" - pure <| Html.text true str - match md.blocks.mapM (blockFromMarkdown' · Markdown.strongEmphHeaders') with - | .error e => HtmlT.logError e; pure <| Html.text true str - | .ok blks => blks.mapM goB - moreDeclHtml name (goB) - | .structure isClass ctor _ infos parents ancestors => - open Verso.Doc.Html in - open Verso.Output Html in do - let parentRow ← do - if parents.isEmpty then pure .empty - else pure {{ -

"Extends"

- - }} - let ctorRow ← - if isPrivateName ctor.name then - pure Html.empty - else pure {{ -

{{if isClass then "Instance Constructor" else "Constructor"}}

- - - {{ ← if let some d := ctor.docstring? then do - pure {{}} - else pure Html.empty - }} -
{{← ctor.hlName.toHtml}}
{{← md2html goB d}}
- }} - let infos := infos.filter (·.subobject?.isNone) - pure {{ - {{ ctorRow }} - {{ parentRow }} -

{{if isClass then "Methods" else "Fields"}}

- - {{← infos.mapM fun i => do - let inheritedAttrVal : Option String := - i.fieldFrom.head?.bind (fun n => parents.findIdx? (·.name == n.name)) |>.map toString - let inheritedAttr : Array (String × String) := inheritedAttrVal.map (fun i => #[("data-inherited-from", i)]) |>.getD #[] - - let inheritedRow : Html ← - if i.fieldFrom.isEmpty then pure Html.empty - else - pure {{ - - - - - }} - - let docRow : Html ← - if let some doc := i.docString? then do - let doc ← md2html goB doc - pure {{ - - - - - }} - else - pure Html.empty - - pure <| {{ - - - - - - }} ++ inheritedRow ++ docRow - }} -
- "Inherited from " -
    - {{ ← i.fieldFrom.mapM fun p => do - pure {{
  1. {{ ← p.hlName.toHtml }}
    2. }} - }} -
-
{{ doc }} -
{{← i.fieldName.toHtml}}" : "{{← i.type.toHtml }}
- }} - - | .inductive ctors _ _ => - open Verso.Doc.Html in - open Verso.Output Html in do - pure {{ -

"Constructors"

- - }} - | _ => pure .empty - saveRef (id : InternalId) (name : Name) (subterm : Option (Doc.Inline Manual)) @@ -700,9 +767,250 @@ where } modify (·.saveDomainObject docstringDomain name.toString id) - open Verso.Doc.Elab +def leanFromMarkdown := () + +def Inline.leanFromMarkdown (hls : Highlighted) : Inline where + name := ``Verso.Genre.Manual.leanFromMarkdown + data := ToJson.toJson hls + +def Block.leanFromMarkdown (hls : Highlighted) : Block where + name := ``Verso.Genre.Manual.leanFromMarkdown + data := ToJson.toJson hls + + +@[inline_extension leanFromMarkdown] +def leanFromMarkdown.inlinedescr : InlineDescr where + traverse _id _data _ := pure none + toTeX := + some <| fun go _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] + extraCss := [highlightingStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output Html in + open Verso.Doc.Html in + some <| fun _ _ data _ => do + match FromJson.fromJson? (α := Highlighted) data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err + pure .empty + | .ok (hl : Highlighted) => + hl.inlineHtml "docstring-examples" + +@[block_extension leanFromMarkdown] +def leanFromMarkdown.blockdescr : BlockDescr where + traverse _id _data _ := pure none + toTeX := + some <| fun goI goB _ _ content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← goB b, .raw "\n"] + extraCss := [highlightingStyle] + extraJs := [highlightingJs] + extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)] + extraCssFiles := [("tippy-border.css", tippy.border.css)] + toHtml := + open Verso.Output Html in + open Verso.Doc.Html in + some <| fun _ _ _ data _ => do + match FromJson.fromJson? (α := Highlighted) data with + | .error err => + HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err + pure .empty + | .ok (hl : Highlighted) => + hl.blockHtml "docstring-examples" + +open Lean Elab Term in +def tryElabCodeTermWith (mk : Highlighted → String → DocElabM α) (str : String) : DocElabM α := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + match Parser.runParserCategory (← getEnv) `term str src with + | .error e => throw (.error (← getRef) e) + | .ok stx => + let (newMsgs, tree, e) ← do + let initMsgs ← Core.getMessageLog + try + Core.resetMessageLog + -- TODO open decls/current namespace + let (tree', e') ← fun _ => do + let e ← Elab.Term.elabTerm (catchExPostpone := true) stx none + Term.synthesizeSyntheticMVarsNoPostponing + let e' ← Term.levelMVarToParam (← instantiateMVars e) + Term.synthesizeSyntheticMVarsNoPostponing + let e' ← instantiateMVars e' + let ctx := PartialContextInfo.commandCtx { + env := ← getEnv, fileMap := ← getFileMap, mctx := ← getMCtx, currNamespace := ← getCurrNamespace, + openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen + } + pure (InfoTree.context ctx (.node (Info.ofCommandInfo ⟨`Verso.Genre.Manual.docstring, (← getRef)⟩) (← getInfoState).trees), e') + pure (← Core.getMessageLog, tree', e') + finally + Core.setMessageLog initMsgs + if newMsgs.hasErrors then + for msg in newMsgs.errorsToWarnings.toArray do + logMessage msg + throwError m!"Didn't elaborate {stx} as term" + + let hls := (← highlight stx #[] (PersistentArray.empty.push tree)) + mk hls str + +open Lean Elab Term in +def tryElabInlineCodeTerm : String → DocElabM Term := + tryElabCodeTermWith fun hls str => + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)]) + +open Lean Elab Term in +def tryElabBlockCodeTerm : String → DocElabM Term := + tryElabCodeTermWith fun hls str => + ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)]) + +private def indentColumn (str : String) : Nat := Id.run do + let mut i : Option Nat := none + for line in str.split (· == '\n') do + let leading := line.takeWhile (·.isWhitespace) + if leading == line then continue + if let some i' := i then + if leading.length < i' then i := some leading.length + else i := some leading.length + return i.getD 0 + +/-- info: 0 -/ +#guard_msgs in +#eval indentColumn "" +/-- info: 0 -/ +#guard_msgs in +#eval indentColumn "abc" +/-- info: 3 -/ +#guard_msgs in +#eval indentColumn " abc" +/-- info: 3 -/ +#guard_msgs in +#eval indentColumn " abc\n\n def" +/-- info: 2 -/ +#guard_msgs in +#eval indentColumn " abc\n\n def" +/-- info: 2 -/ +#guard_msgs in +#eval indentColumn " abc\n\n def\n a" + +open Lean Elab Term in +def tryElabBlockCodeCommand (str : String) : DocElabM Term := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + + let ictx := Parser.mkInputContext str src + let cctx : Command.Context := { fileName := ← getFileName, fileMap := FileMap.ofString str, tacticCache? := none, snap? := none, cancelTk? := none} + + let mut cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := [{header := ""}]} + let mut pstate := {pos := 0, recovering := false} + let mut cmds := #[] + + repeat + let scope := cmdState.scopes.head! + let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } + let (cmd, ps', messages) := Parser.parseCommand ictx pmctx pstate cmdState.messages + cmds := cmds.push cmd + pstate := ps' + cmdState := {cmdState with messages := messages} + + cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) do + match (← liftM <| EIO.toIO' <| (Command.elabCommand cmd cctx).run cmdState) with + | Except.error e => Lean.logError e.toMessageData; return cmdState + | Except.ok ((), s) => return s + + if Parser.isTerminalCommand cmd then break + + for msg in cmdState.messages.unreported do + logMessage msg + + if cmdState.messages.hasErrors then + throwError "Errors found in command" + + let mut hls := Highlighted.empty + for cmd in cmds do + hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees) + + hls := hls.deIndent (indentColumn str) + + ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)]) + + + +open Lean Elab Term in +def tryElabInlineCodeName (str : String) : DocElabM Term := do + let str := str.trim + let x := str.toName + if x.toString == str then + let stx := mkIdent x + let n ← realizeGlobalConstNoOverload stx + let hl : Highlighted ← constTok n str + ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) + else + throwError "Not a name: '{str}'" +where + constTok {m} [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m] + (name : Name) (str : String) : + m Highlighted := do + let docs ← findDocString? (← getEnv) name + let sig := toString (← (PrettyPrinter.ppSignature name)).1 + pure <| .token ⟨.const name sig docs false, str⟩ + +open Lean Elab Term in +def tryElabInlineCode (decls : List Name) (str : String) : DocElabM Term := do + match decls with + | decl :: decls => + -- This brings the parameters into scope, so the term elaboration version catches them! + Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ => + tryElabInlineCode decls str + | [] => + try + tryElabInlineCodeName str <|> + tryElabInlineCodeTerm str + catch + | .error ref e => + logWarningAt ref e + ``(Verso.Doc.Inline.code $(quote str)) + | e => + logWarning m!"Internal exception uncaught: {e.toMessageData}" + ``(Verso.Doc.Inline.code $(quote str)) + +open Lean Elab Term in +def tryElabBlockCode (decls : List Name) (str : String) : DocElabM Term := do + match decls with + | decl :: decls => + -- This brings the parameters into scope, so the term elaboration version catches them! + Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ => + tryElabBlockCode decls str + | [] => + try + tryElabBlockCodeCommand str <|> tryElabBlockCodeTerm str + catch + | .error ref e => + logWarningAt ref e + ``(Verso.Doc.Block.code $(quote str)) + | e => + logWarning m!"Internal exception uncaught: {e.toMessageData}" + ``(Verso.Doc.Block.code $(quote str)) + +/-- +Heuristically elaborate Lean fragments in Markdown code. The provided names are used as signatures, +from left to right, with the names bound by the signature being available in the local scope in +which the Lean fragments are elaborated. +-/ +def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM Term := + Markdown.blockFromMarkdown b + (handleHeaders := Markdown.strongEmphHeaders) + (elabInlineCode := tryElabInlineCode names) + (elabBlockCode := tryElabBlockCode names) + @[block_role_expander docstring] def docstring : BlockRoleExpander | args, #[] => do @@ -710,12 +1018,14 @@ def docstring : BlockRoleExpander | #[.anon (.name x)] => let name ← Elab.realizeGlobalConstNoOverloadWithInfo x Doc.PointOfInterest.save (← getRef) name.toString (detail? := some "Documentation") - let blockStx ← match ← Lean.findDocString? (← getEnv) name with - | none => logWarningAt x m!"No docs found for '{x}'"; pure #[] - | some docs => - let some ast := MD4Lean.parse docs - | throwErrorAt x "Failed to parse docstring as Markdown" - ast.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders) + let blockStx ← + match ← Lean.findDocString? (← getEnv) name with + | none => logWarningAt x m!"No docs found for '{x}'"; pure #[] + | some docs => + let some ast := MD4Lean.parse docs + | throwErrorAt x "Failed to parse docstring as Markdown" + + ast.blocks.mapM (blockFromMarkdownWithLean [name]) if Lean.Linter.isDeprecated (← getEnv) name then logInfoAt x m!"'{x}' is deprecated" @@ -735,9 +1045,62 @@ def docstring : BlockRoleExpander } let sig := Lean.Widget.tagCodeInfos ctx infos tt let signature ← some <$> renderTagged none sig ⟨{}, false⟩ - pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature)) #[$blockStx,*])] + let extras ← getExtras name declType + pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature)) #[$(blockStx ++ extras),*])] | _ => throwError "Expected exactly one positional argument that is a name" | _, more => throwErrorAt more[0]! "Unexpected block argument" +where + getExtras (name : Name) (declType : Block.Docstring.DeclType) : DocElabM (Array Term) := + match declType with + | .structure isClass constructor _ fieldInfo parents _ => do + let ctorRow : Term ← do + let header := if isClass then "Instance Constructor" else "Constructor" + let sigDesc ← + if let some docs := constructor.docstring? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (blockFromMarkdownWithLean [name, constructor.name]) + else pure #[] + let sig ← `(Verso.Doc.Block.other (Verso.Genre.Manual.Block.internalSignature $(quote constructor.hlName) none) #[$sigDesc,*]) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$sig]) + let parentsRow : Option Term ← do + if parents.isEmpty then pure none + else + let header := "Extends" + let inh ← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.inheritance $(quote name) $(quote parents)) #[]) + some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$inh]) + + + let fieldsRow : Term ← do + let header := if isClass then "Methods" else "Fields" + let fieldInfo := fieldInfo.filter (·.subobject?.isNone) + let fieldSigs : Array Term ← fieldInfo.mapM fun i => do + let inheritedFrom : Option Nat := + i.fieldFrom.head?.bind (fun n => parents.findIdx? (·.name == n.name)) + let sigDesc : Array Term ← + if let some docs := i.docString? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (blockFromMarkdownWithLean [name, constructor.name]) + else + pure (#[] : Array Term) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.fieldSignature $(quote i.fieldName) $(quote i.type) $(quote inheritedFrom) $(quote <| parents.map (·.parent))) #[$sigDesc,*]) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$fieldSigs,*]) + pure <| #[ctorRow] ++ parentsRow.toArray ++ [fieldsRow] + | .inductive ctors .. => do + let ctorSigs : Array Term ← + -- Elaborate constructor docs in the type's NS + ctors.mapM fun c => withTheReader Core.Context ({· with currNamespace := name}) do + let sigDesc ← + if let some docs := c.docstring? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (blockFromMarkdownWithLean [name, c.name]) + else pure (#[] : Array Term) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.constructorSignature $(quote c.signature)) #[$sigDesc,*]) + pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection "Constructors") #[$ctorSigs,*])] + | _ => pure #[] + def Block.optionDocs (name : Name) (defaultValue : Option Highlighted) : Block where name := `Verso.Genre.Manual.optionDocs @@ -783,7 +1146,7 @@ def optionDocs : BlockRoleExpander Doc.PointOfInterest.save x optDecl.declName.toString let some mdAst := MD4Lean.parse optDecl.descr | throwErrorAt x "Failed to parse docstring as Markdown" - let contents ← mdAst.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders) + let contents ← mdAst.blocks.mapM (blockFromMarkdownWithLean []) pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.optionDocs $(quote x.getId) $(quote <| highlightDataValue optDecl.defValue)) #[$contents,*])] | _, more => throwErrorAt more[0]! "Unexpected block argument" @@ -904,7 +1267,7 @@ def tactic : DirectiveExpander throwError "No `show` option provided, but the tactic has no user-facing token name" let some mdAst := tactic.docString >>= MD4Lean.parse | throwError "Failed to parse docstring as Markdown" - let contents ← mdAst.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders) + let contents ← mdAst.blocks.mapM (blockFromMarkdownWithLean []) let userContents ← more.mapM elabBlock pure #[← ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])] @@ -1034,7 +1397,7 @@ def conv : DirectiveExpander let contents ← if let some d := tactic.docs? then let some mdAst := MD4Lean.parse d | throwError "Failed to parse docstring as Markdown" - mdAst.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders) + mdAst.blocks.mapM (blockFromMarkdownWithLean []) else pure #[] let userContents ← more.mapM elabBlock let some toShow := opts.show diff --git a/src/verso-manual/VersoManual/Html/Style.lean b/src/verso-manual/VersoManual/Html/Style.lean index b1dbdec..dcac66b 100644 --- a/src/verso-manual/VersoManual/Html/Style.lean +++ b/src/verso-manual/VersoManual/Html/Style.lean @@ -104,6 +104,7 @@ pre, code { font-family: var(--verso-code-font-family); font-variant-ligatures: none; overflow-x: auto; + overflow-y: clip; } /******** Page Layout ********/ diff --git a/src/verso-manual/VersoManual/Markdown.lean b/src/verso-manual/VersoManual/Markdown.lean index 74e151b..87d087e 100644 --- a/src/verso-manual/VersoManual/Markdown.lean +++ b/src/verso-manual/VersoManual/Markdown.lean @@ -25,6 +25,11 @@ generate nested `Part`s, but rather some custom node or some formatted text. private structure HeaderHandlers (m : Type u → Type w) (block : Type u) (inline : Type v) : Type (max u v w) where levels : List (Array inline → m block) := [] +structure MDContext (m : Type u → Type w) (block : Type u) (inline : Type u) : Type (max u w) where + headerHandlers : HeaderHandlers m block inline + elabInlineCode : Option (String → m inline) + elabBlockCode : Option (String → m block) + def attrText : AttrText → Except String String | .normal str => pure str | .nullchar => throw "Null character" @@ -40,7 +45,28 @@ def attr' (val : Array AttrText) : Except String String := do | .error e => .error e | .ok s => pure s -partial def inlineFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] : Text → m Term +private structure MDState where + /-- A mapping from document header levels to actual nesting levels -/ + inHeaders : List (Nat × Nat) := [] +deriving Inhabited + +private abbrev MDT m block inline α := ReaderT (MDContext m block inline) (StateT MDState m) α + +instance {block inline} [Monad m] : MonadLift m (MDT m block inline) where + monadLift act := fun _ s => act <&> (·, s) + +instance {block inline} [Monad m] [AddMessageContext m] : AddMessageContext (MDT m block inline) where + addMessageContext msg := (addMessageContext msg : m _) + + +instance {block inline} [AddMessageContext m] [Monad m] [MonadError m] : MonadError (MDT m block inline) where + throw e := throw (m := m) e + tryCatch a b := fun r s => do + tryCatch (a r s) fun e => b e r s + + + +partial def inlineFromMarkdown [Monad m] [MonadQuotation m] [AddMessageContext m] [MonadError m] : Text → MDT m Term Term Term | .normal str | .br str | .softbr str => ``(Verso.Doc.Inline.text $(quote str)) | .nullchar => throwError "Unexpected null character in parsed Markdown" | .del _ => throwError "Unexpected strikethrough in parsed Markdown" @@ -50,7 +76,12 @@ partial def inlineFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] : Tex | .latexMath m => ``(Verso.Doc.Inline.math Verso.Doc.MathMode.inline $(quote <| String.join m.toList)) | .latexMathDisplay m => ``(Verso.Doc.Inline.math Verso.Doc.MathMode.display $(quote <| String.join m.toList)) | .u txt => throwError "Unexpected underline around {repr txt} in parsed Markdown" - | .code str => ``(Verso.Doc.Inline.code $(quote <| String.join str.toList)) + | .code strs => do + let str := String.join strs.toList + if let some f := (← read).elabInlineCode then + f str + else + ``(Verso.Doc.Inline.code $(quote str)) | .entity ent => throwError s!"Unsupported entity {ent} in parsed Markdown" | .img .. => throwError s!"Unexpected image in parsed Markdown" | .wikiLink .. => throwError s!"Unexpected wiki-style link in parsed Markdown" @@ -70,12 +101,6 @@ partial def inlineFromMarkdown' : Text → Except String (Doc.Inline g) | .img .. => .error s!"Unexpected image in parsed Markdown" | .wikiLink .. => .error s!"Unexpected wiki-style link in parsed Markdown" -private structure MDState where - /-- A mapping from document header levels to actual nesting levels -/ - inHeaders : List (Nat × Nat) := [] -deriving Inhabited - -private abbrev MDT m block inline α := ReaderT (HeaderHandlers m block inline) (StateT MDState m) α instance [Monad m] [MonadError m] : MonadError (MDT m b i) where throw ex := fun _ρ _σ => throw ex @@ -102,14 +127,19 @@ private partial def getHeaderLevel [Monad m] (level : Nat) : MDT m b i Nat := do private def getHeader [Monad m] (level : Nat) : MDT m b i (Except String (Array i → m b)) := do let lvl ← getHeaderLevel level - match (← read).levels.get? lvl with + match (← read).headerHandlers.levels.get? lvl with | none => pure (throw s!"Unexpected header with nesting level {lvl} in parsed Markdown") | some f => pure (pure f) -private partial def blockFromMarkdownAux [Monad m] [MonadQuotation m] [MonadError m] : MD4Lean.Block → MDT m Term Term Term +private partial def blockFromMarkdownAux [Monad m] [AddMessageContext m] [MonadQuotation m] [MonadError m] : MD4Lean.Block → MDT m Term Term Term | .p txt => do ``(Verso.Doc.Block.para #[$[$(← txt.mapM (inlineFromMarkdown ·))],*]) | .blockquote bs => do ``(Verso.Doc.Block.blockquote #[$[$(← bs.mapM blockFromMarkdownAux )],*]) - | .code _ _ _ strs => do ``(Verso.Doc.Block.code $(quote <| String.join strs.toList)) + | .code _ _ _ strs => do + let str := String.join strs.toList + if let some f := (← read).elabBlockCode then + f str + else + ``(Verso.Doc.Block.code $(quote str)) | .ul _ _ items => do ``(Verso.Doc.Block.ul #[$[$(← items.mapM itemFromMarkdown)],*]) | .ol _ i _ items => do let itemStx ← items.mapM itemFromMarkdown @@ -129,10 +159,13 @@ where else ``(Verso.Doc.ListItem.mk 0 #[$[$(← item.contents.mapM blockFromMarkdownAux)],*]) -def blockFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] +def blockFromMarkdown [Monad m] [MonadQuotation m] [MonadError m] [AddMessageContext m] (md : MD4Lean.Block) - (handleHeaders : List (Array Term → m Term) := []) : m Term := - (·.fst) <$> blockFromMarkdownAux md ⟨handleHeaders⟩ {} + (handleHeaders : List (Array Term → m Term) := []) + (elabInlineCode : Option (String → m Term) := none) + (elabBlockCode : Option (String → m Term) := none) : m Term := + let ctxt := {headerHandlers := ⟨handleHeaders⟩, elabInlineCode, elabBlockCode} + (·.fst) <$> blockFromMarkdownAux md ctxt {} def strongEmphHeaders [Monad m] [MonadQuotation m] : List (Array Term → m Term) := [ fun stxs => ``(Verso.Doc.Block.para #[Verso.Doc.Inline.bold #[$stxs,*]]), @@ -162,8 +195,11 @@ where def blockFromMarkdown' (md : MD4Lean.Block) - (handleHeaders : List (Array (Doc.Inline g) → Except String (Doc.Block g)) := []) : Except String (Doc.Block g) := - (·.fst) <$> blockFromMarkdownAux' md ⟨handleHeaders⟩ {} + (handleHeaders : List (Array (Doc.Inline g) → Except String (Doc.Block g)) := []) + (elabInlineCode : Option (String → Except String (Doc.Inline g)) := none) + (elabBlockCode : Option (String → Except String (Doc.Block g)) := none) : + Except String (Doc.Block g) := + (·.fst) <$> blockFromMarkdownAux' md ⟨⟨handleHeaders⟩, elabInlineCode, elabBlockCode⟩ {} def strongEmphHeaders' : List (Array (Doc.Inline g) → Except String (Doc.Block g)) := [ fun inls => pure <| .para #[.bold inls], diff --git a/src/verso-manual/VersoManual/TeX.lean b/src/verso-manual/VersoManual/TeX.lean index 845ea43..66cdc9d 100644 --- a/src/verso-manual/VersoManual/TeX.lean +++ b/src/verso-manual/VersoManual/TeX.lean @@ -14,6 +14,9 @@ r##" \usepackage{sourcesanspro} \usepackage{sourceserifpro} +\usepackage{fancyvrb} +\usepackage{fvextra} + \makechapterstyle{lean}{% \renewcommand*{\chaptitlefont}{\sffamily\HUGE} \renewcommand*{\chapnumfont}{\chaptitlefont} diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean index f1ba0f1..77f4636 100644 --- a/src/verso/Verso/Code/Highlighted.lean +++ b/src/verso/Verso/Code/Highlighted.lean @@ -15,6 +15,41 @@ open Verso.Output Html open Lean (Json) open Std (HashMap) +namespace SubVerso.Highlighting +/-- +Remove n levels of indentation from highlighted code. +-/ +partial def Highlighted.deIndent (n : Nat) (hl : Highlighted) : Highlighted := + (remove hl).run' (some n) +where + remove (hl : Highlighted) : StateM (Option Nat) Highlighted := do + match hl with + | .token t => + set (none : Option Nat) + return .token t + | .span i x => .span i <$> remove x + | .seq xs => .seq <$> xs.mapM remove + | .text s => + let mut s' := "" + let mut iter := s.iter + while h : iter.hasNext do + let c := iter.curr' h + iter := iter.next + match c with + | '\n' => + set (some n) + | ' ' => + if let some (i + 1) ← get then + set (some i) + continue + | _ => set (none : Option Nat) + s' := s'.push c + return .text s' + | .point p s => return .point p s + | .tactics gs x y hl => .tactics gs x y <$> remove hl + +end SubVerso.Highlighting + namespace Verso.Code diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean index b2ba9e1..7476d42 100644 --- a/src/verso/Verso/Doc/Elab/Monad.lean +++ b/src/verso/Verso/Doc/Elab/Monad.lean @@ -324,6 +324,9 @@ instance : Inhabited (DocElabM α) := ⟨fun _ _ => default⟩ instance : AddErrorMessageContext DocElabM := inferInstanceAs <| AddErrorMessageContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) +instance [MonadWithReaderOf ρ TermElabM] : MonadWithReaderOf ρ DocElabM := + inferInstanceAs <| MonadWithReaderOf ρ (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) + instance : MonadLift TermElabM DocElabM where monadLift act := fun _ st' => do return (← Term.withDeclName (← currentDocName) act, st') @@ -336,6 +339,10 @@ instance : MonadQuotation DocElabM := inferInstanceAs <| MonadQuotation (ReaderT instance : Monad DocElabM := inferInstanceAs <| Monad (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) +instance : MonadControl TermElabM DocElabM := + let ⟨stM, liftWith, restoreM⟩ := inferInstanceAs <| MonadControlT TermElabM (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) + {stM, liftWith, restoreM := (· >>= restoreM)} + instance : MonadExceptOf Exception DocElabM := inferInstanceAs <| MonadExceptOf Exception (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) instance : MonadAlwaysExcept Exception DocElabM := inferInstanceAs <| MonadAlwaysExcept Exception (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) diff --git a/src/verso/Verso/Doc/TeX.lean b/src/verso/Verso/Doc/TeX.lean index e3c5323..8363d06 100644 --- a/src/verso/Verso/Doc/TeX.lean +++ b/src/verso/Verso/Doc/TeX.lean @@ -74,7 +74,7 @@ partial defmethod Inline.toTeX [Monad m] [GenreTeX g m] : Inline g → TeXT g m | .bold content => do pure \TeX{\textbf{\Lean{← content.mapM toTeX}}} | .code str => do - pure \TeX{s!"\\verb|{str}|"} --- TODO choose delimiter automatically + pure \TeX{s!"\\Verb|{str}|"} --- TODO choose delimiter automatically | .math .inline str => pure <| .raw s!"${str}$" | .math .display str => pure <| .raw s!"\\[{str}\\]" | .concat inlines => inlines.mapM toTeX diff --git a/src/verso/Verso/Output/Html.lean b/src/verso/Verso/Output/Html.lean index 9120467..a5a59b6 100644 --- a/src/verso/Verso/Output/Html.lean +++ b/src/verso/Verso/Output/Html.lean @@ -283,6 +283,15 @@ info: Verso.Output.Html.tag #guard_msgs in #eval test +def leanKwTest : Html := {{ + +}} + +/-- info: Verso.Output.Html.tag "label" #[("for", "foo")] (Verso.Output.Html.text true "Blah") -/ +#guard_msgs in + #eval leanKwTest + + /-- error: 'br' doesn't allow contents -/ #guard_msgs in #eval show Html from {{
"foo" "foo"
}}