diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index cde0bde..fb6a822 100644 --- a/doc/UsersGuide/Basic.lean +++ b/doc/UsersGuide/Basic.lean @@ -73,7 +73,7 @@ results in :::tactic "simp" ::: - +{docstring Nat} # Index %%% diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 7011238..37827db 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -775,6 +775,10 @@ 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 @@ -798,8 +802,30 @@ def leanFromMarkdown.inlinedescr : InlineDescr where | .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 tryElabInlineCodeTerm (str : String) : DocElabM Term := do +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!"" @@ -832,10 +858,91 @@ def tryElabInlineCodeTerm (str : String) : DocElabM Term := do throwError m!"Didn't elaborate {stx} as term" let hls := (← highlight stx #[] (PersistentArray.empty.push tree)) + mk hls str - logInfoAt (← getRef) m!"Elaborated {stx} -> {e}" +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 @@ -875,6 +982,24 @@ def tryElabInlineCode (decls : List Name) (str : String) : DocElabM Term := do 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 @@ -884,6 +1009,7 @@ def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM Markdown.blockFromMarkdown b (handleHeaders := Markdown.strongEmphHeaders) (elabInlineCode := tryElabInlineCode names) + (elabBlockCode := tryElabBlockCode names) @[block_role_expander docstring] def docstring : BlockRoleExpander diff --git a/src/verso-manual/VersoManual/Markdown.lean b/src/verso-manual/VersoManual/Markdown.lean index 9c91e3e..87d087e 100644 --- a/src/verso-manual/VersoManual/Markdown.lean +++ b/src/verso-manual/VersoManual/Markdown.lean @@ -136,7 +136,10 @@ private partial def blockFromMarkdownAux [Monad m] [AddMessageContext m] [MonadQ | .blockquote bs => do ``(Verso.Doc.Block.blockquote #[$[$(← bs.mapM blockFromMarkdownAux )],*]) | .code _ _ _ strs => do let str := String.join strs.toList - ``(Verso.Doc.Block.code $(quote str)) + 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 diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean index 2d7be7c..a2040b8 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/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"
}}