diff --git a/src/library/documentation.cpp b/src/library/documentation.cpp index a53f4b6b3d..5c5c63c9ea 100644 --- a/src/library/documentation.cpp +++ b/src/library/documentation.cpp @@ -95,10 +95,38 @@ static std::string unindent(std::string const & s) { } } +static std::string add_lean_suffix_to_code_blocks(std::string const & s) { + std::string r; + unsigned sz = s.size(); + unsigned i = 0; + bool in_block = false; + while (i < sz) { + if (!in_block && s[i] == '`' && sz >= 4 && i < sz - 3 && s[i+1] == '`' && s[i+2] == '`' && isspace(s[i+3])) { + r += "```lean"; + r += s[i+3]; + i += 4; + in_block = true; + } else if (in_block && s[i] == '`' && sz >= 3 && i < sz - 2 && s[i+1] == '`' && s[i+2] == '`') { + r += "```"; + i += 3; + in_block = false; + } else { + r += s[i]; + i++; + } + } + if (in_block) { + std::cout << "------" << r << "-----\n"; + throw exception("invalid doc string, end of code block ``` expected"); + } + return r; +} + static std::string process_doc(std::string s) { remove_blank_lines_begin(s); rtrim(s); - return unindent(s); + s = unindent(s); + return add_lean_suffix_to_code_blocks(s); } environment add_module_doc_string(environment const & env, std::string doc) { diff --git a/src/shell/leandoc.cpp b/src/shell/leandoc.cpp index 44d1d67c6e..2a63507881 100644 --- a/src/shell/leandoc.cpp +++ b/src/shell/leandoc.cpp @@ -131,7 +131,7 @@ static void print_inductive(std::ostream & out, environment const & env, formatt format r = format(c); r += space() + colon() + space(); r += nest(get_pp_indent(o), line() + fmt(env.get(c).get_type())); - out << mk_pair(r, o) << "\n"; + out << mk_pair(group(r), o) << "\n"; } out << "```\n"; } @@ -181,9 +181,9 @@ void gen_doc(environment const & env, options const & _opts, std::ostream & out) if (auto decl_name = entry.get_decl_name()) { gen_decl_doc(out, env, fmt, *decl_name); out << "\n"; - out << entry.get_doc() << "\n"; + out << entry.get_doc(); } else { - out << entry.get_doc() << "\n"; + out << entry.get_doc(); } out << "\n"; }