diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean index 68f87b8d51..ffe8e23546 100644 --- a/src/Lean/DocString/Extension.lean +++ b/src/Lean/DocString/Extension.lean @@ -69,6 +69,11 @@ register_builtin_option doc.verso : Bool := { descr := "whether to use Verso syntax in docstrings" } +register_builtin_option doc.verso.module : Bool := { + defValue := false, + descr := "whether to use Verso syntax in module docstrings (falls back to `doc.verso` if not set)" +} + private builtin_initialize builtinDocStrings : IO.Ref (NameMap String) ← IO.mkRef {} builtin_initialize docStringExt : MapDeclarationExtension String ← mkMapDeclarationExtension diff --git a/src/Lean/DocString/Parser.lean b/src/Lean/DocString/Parser.lean index 7a23556c9b..a1478895b6 100644 --- a/src/Lean/DocString/Parser.lean +++ b/src/Lean/DocString/Parser.lean @@ -1214,6 +1214,35 @@ Parenthesizer for `ifVerso`—parenthesizes according to the underlying parenthe @[combinator_parenthesizer ifVerso, expose] public def ifVerso.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p1 <|> p2 +/-- +Parses as `ifVerso` if module docs should use Verso syntax, or as `ifNotVerso` otherwise. +Checks `doc.verso.module` if explicitly set, otherwise falls back to `doc.verso`. +-/ +public def ifVersoModuleDocsFn (ifVerso ifNotVerso : ParserFn) : ParserFn := fun c s => + let useVerso := + if c.options.contains `doc.verso.module then + c.options.getBool `doc.verso.module + else + c.options.getBool `doc.verso + if useVerso then ifVerso c s + else ifNotVerso c s + +@[inherit_doc ifVersoModuleDocsFn] +public def ifVersoModuleDocs (ifVerso ifNotVerso : Parser) : Parser where + fn := ifVersoModuleDocsFn ifVerso.fn ifNotVerso.fn + +/-- +Formatter for `ifVersoModuleDocs`—formats according to the underlying formatters. +-/ +@[combinator_formatter ifVersoModuleDocs, expose] +public def ifVersoModuleDocs.formatter (f1 f2 : Formatter) : Formatter := f1 <|> f2 + +/-- +Parenthesizer for `ifVersoModuleDocs`—parenthesizes according to the underlying parenthesizers. +-/ +@[combinator_parenthesizer ifVersoModuleDocs, expose] +public def ifVersoModuleDocs.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p1 <|> p2 + /-- Disables the option `doc.verso` while running a parser. -/ diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index a3eb4de825..9c34538a35 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -56,7 +56,7 @@ multiple times in the same file. -/ @[builtin_command_parser] def moduleDoc := leading_parser ppDedent <| - "/-!" >> Doc.Parser.ifVerso versoCommentBody commentBody >> ppLine + "/-!" >> Doc.Parser.ifVersoModuleDocs versoCommentBody commentBody >> ppLine def namedPrio := leading_parser diff --git a/tests/lean/run/versoDocModuleDeclOnly.lean b/tests/lean/run/versoDocModuleDeclOnly.lean new file mode 100644 index 0000000000..9c576889f5 --- /dev/null +++ b/tests/lean/run/versoDocModuleDeclOnly.lean @@ -0,0 +1,45 @@ +/- +Tests that `doc.verso.module false` disables Verso for module docs +while `doc.verso true` keeps declaration docs as Verso. +-/ +import Lean + +-- Module docs use Markdown, declaration docs use Verso +set_option doc.verso true +set_option doc.verso.module false + +/-! +This is a plain Markdown module doc with `code` and **bold**. + +Verso syntax is {here}**visible**. +-/ + +open Lean Elab Term in +/-- +info: Markdown: +This is a plain Markdown module doc with `code` and **bold**. + +Verso syntax is {here}**visible**. + +Verso: +-/ +#guard_msgs in +#eval show TermElabM Unit from do + IO.println "Markdown:" + for modDoc in (Lean.getMainModuleDoc (← getEnv)).toArray do + IO.println modDoc.doc + IO.println "Verso:" + for modDoc in (Lean.getMainVersoModuleDocs (← getEnv)).snippets do + IO.println <| repr modDoc + +/-- +{name}`versoDecl` +-/ +def versoDecl := "hello" + +-- This would show the Verso syntax if it were interpreted as Markdown +open Lean Elab Term in +/-- info: `versoDecl` -/ +#guard_msgs in +#eval show TermElabM Unit from do + (← findDocString? (← getEnv) ``versoDecl).forM (IO.println ·) diff --git a/tests/lean/run/versoDocModuleFallback.lean b/tests/lean/run/versoDocModuleFallback.lean new file mode 100644 index 0000000000..02d9ab5ff1 --- /dev/null +++ b/tests/lean/run/versoDocModuleFallback.lean @@ -0,0 +1,55 @@ +/- +Tests that when `doc.verso.module` is not explicitly set, +module docs fall back to the value of `doc.verso`. +-/ +import Lean + +-- Only set doc.verso, do not set doc.verso.module +set_option doc.verso true + +/-! +Module docs should parse as Verso here (fallback from {option}`doc.verso`). + +*Bold* and _italic_ and [link](example.com) +-/ + +open Lean Elab Term in +/-- +info: Markdown: +Verso: +{ text := #[Lean.Doc.Block.para + #[Lean.Doc.Inline.text "Module docs should parse as Verso here (fallback from ", + Lean.Doc.Inline.other + { name := `Lean.Doc.Data.Option val := Dynamic.mk `Lean.Doc.Data.Option _ } + #[Lean.Doc.Inline.code "doc.verso"], + Lean.Doc.Inline.text ")."], + Lean.Doc.Block.para + #[Lean.Doc.Inline.bold #[Lean.Doc.Inline.text "Bold"], Lean.Doc.Inline.text " and ", + Lean.Doc.Inline.emph #[Lean.Doc.Inline.text "italic"], Lean.Doc.Inline.text " and ", + Lean.Doc.Inline.link #[Lean.Doc.Inline.text "link"] "example.com", Lean.Doc.Inline.linebreak "\n"]], + sections := #[], + declarationRange := { pos := { line := 10, column := 0 }, + charUtf16 := 0, + endPos := { line := 14, column := 2 }, + endCharUtf16 := 2 } } +-/ +#guard_msgs in +#eval show TermElabM Unit from do + IO.println "Markdown:" + for modDoc in (Lean.getMainModuleDoc (← getEnv)).toArray do + IO.println modDoc.doc + IO.println "Verso:" + for modDoc in (Lean.getMainVersoModuleDocs (← getEnv)).snippets do + IO.println <| repr modDoc + + +/-- +{name}`fallbackDecl` +-/ +def fallbackDecl := "hello" + +open Lean Elab Command Term in +/-- info: `fallbackDecl` -/ +#guard_msgs in +#eval show TermElabM Unit from do + (← findDocString? (← getEnv) ``fallbackDecl).forM (IO.println ·) diff --git a/tests/lean/run/versoDocModuleVersoOnly.lean b/tests/lean/run/versoDocModuleVersoOnly.lean new file mode 100644 index 0000000000..c56e2fd74b --- /dev/null +++ b/tests/lean/run/versoDocModuleVersoOnly.lean @@ -0,0 +1,49 @@ +/- +Tests that `doc.verso.module` can independently enable Verso syntax for module docs +while keeping declaration docs as Markdown. +-/ +import Lean + +-- Module docs use Verso, declaration docs use Markdown +set_option doc.verso.module true +set_option doc.verso false + +/-! +Module docs should parse as Verso here. + +*Bold* and _italic_ and [link](example.com) +-/ + +open Lean Elab Term in +/-- +info: Markdown: +Verso: +{ text := #[Lean.Doc.Block.para #[Lean.Doc.Inline.text "Module docs should parse as Verso here."], + Lean.Doc.Block.para + #[Lean.Doc.Inline.bold #[Lean.Doc.Inline.text "Bold"], Lean.Doc.Inline.text " and ", + Lean.Doc.Inline.emph #[Lean.Doc.Inline.text "italic"], Lean.Doc.Inline.text " and ", + Lean.Doc.Inline.link #[Lean.Doc.Inline.text "link"] "example.com", Lean.Doc.Inline.linebreak "\n"]], + sections := #[], + declarationRange := { pos := { line := 11, column := 0 }, + charUtf16 := 0, + endPos := { line := 15, column := 2 }, + endCharUtf16 := 2 } } +-/ +#guard_msgs in +#eval show TermElabM Unit from do + IO.println "Markdown:" + for modDoc in (Lean.getMainModuleDoc (← getEnv)).toArray do + IO.println modDoc.doc + IO.println "Verso:" + for modDoc in (Lean.getMainVersoModuleDocs (← getEnv)).snippets do + IO.println <| repr modDoc + + +/-- This is a plain Markdown docstring with {nonVerso}`code` and **bold**. -/ +def plainMarkdown := "hello" + +open Lean Elab Command Term in +/-- info: "This is a plain Markdown docstring with {nonVerso}`code` and **bold**. " -/ +#guard_msgs in +#eval show TermElabM Unit from do + (← findDocString? (← getEnv) ``plainMarkdown).forM (IO.println ·.quote)