Replace the [...] syntax from why3doc by a Markdown-like syntax (fix issue #132).
Some why3doc
comments in the gallery contains [i,j[
, which breaks the documentation since it opens a code block that is never closed. The proper way to write it is [\[i,j\[]
, which is not only ugly but also error-prone.
This commit introduces a Markdown-like syntax for embedded code. It uses the backtick as a delimiter: `[i,j[`
. It also supports multi-backticks: you can output `code`
using `` `code` ``
.