Bitbucket Markdown Syntax

Posted on by



  1. Markdown Syntax Documentation
  2. Markdown Syntax Cheat Sheet
  • Bitbucket can parse and display Markdown, reStructuredText, Textile, and plain text README files. With a syntax like Markdown, you can emphasize text, include screen captures, and more. For a tutorial on Bitbucket's Markdown support and syntax examples, see our Markdown demo repository. Extensions and Languages.
  • Markdown Viewer / Browser Extension. Contribute to simov/markdown-viewer development by creating an account on GitHub.
Markdown editor

Wouldn’t it be nice to just include snippets of Isabelle code in markdown or html and have them show up rendered with symbols and highlighting?

Markdown is a way of formatting text and inserting images. It can be used with the following features of Habitica: Titles, notes, and checklists for tasks and Rewards (including tasks and Rewards.

For instance on a blog? Or a list like the Top 100 theorems? Or on github?

Set your quick_and_dirty flags and read on.

The Short Version

The syntax highlighter pygments now supports Isabelle.

You can use it together with tools like pandoc to embed Isabelle code in markdown, html, or other pandoc source languages. You can even generate RTF documents with highlighted Isabelle code and talk to people who speak MS Word.

Example

In markdown source, text like the following

turns into nicely rendered HTML:

Sample text with inline Γ⊢e::t Isabelle formulas and a fenced Isabelle code block.

Since pygments is fairly comfortable with Unicode, you can even just copy source from Isabelle/jEdit, including already rendered symbols, and paste it into markdown:

becomes

Cool! What do I need to do?

The basics first:

  • The current release version of pygments has support for highlighting, but not yet for symbols and sub/super scripts. If you want the latter, you will need to run the source version from my pygments development branch https://bitbucket.org/lsf37/pygments-main (pull requests are submitted to the pygments team, so hopefully this won’t be necessary any more in the not too distant future):

    hg clone https://bitbucket.org/lsf37/pygments-main

  • Make sure you’re on the all branch:

    hg up all

  • Add pygmentize to your PATH

    export PATH=~/pygments-main/:$PATH

  • Run it on a theory file to test. E.g.:

    pygmentize ~/isabelle/src/HOL/Taylor.thy This should print the theory file highlighted on the terminal. You might need additional python packages. Any easy way to get them is to install standard pygments first on your system (e.g. through ports or homebrew on the Mac, or your system package manager in Linux).

  • If your terminal font has Unicode symbols and you run

    pygmentize -F symbols ~/isabelle/src/HOL/Taylor.thy you should now see those symbols show up. If not, you’ll probably see boxes. (-F is the command line option for running a filter. The symbols filter replaces Isabelle symbol sequences with their Unicode counterparts.)

If the last two steps worked, you now have a working pygments install that understands Isabelle. Download whatsapp desktop for mac.

Syntax

Markdown and HTML

Now, there is a lot of choice. You could run any markdown engine that natively supports pygments, there are plenty of these. You could also run pygments directly in html generators like jekyll.

I happen to like pandoc for markdown rendering, but you first have to tell it to use pygments instead of its own syntax highlighter. Which you can do by putting something like the following into a file pygdoc.hs:

(I did say quick and dirty. Feel free to improve…). Compile it with

And run pandoc with something like

The options mean:

  • -s: produce a standalone html file with headers etc
  • --css hilite.css: include a link to the style file hilite.css
  • --filter ./pygdoc: this slots in our pygments filter
  • -o README.html: the output file
  • README.md: the input file

You don’t have to write hilite.css yourself. You can generate it with pygments for the theme you like (here default) with

Markdown Syntax Documentation

Font

With Isabelle symbols, you might not want to trust that every user’s browser and its fonts support all Unicode symbols in exactly the way Isabelle/jEdit renders them. Luckily, the Isabelle font is part of the Isabelle distribution (lib/fonts/IsabelleText.ttf), and you can just include it in your own CSS with the @font-face directive. For instance:

Github

Github now also recognizes Isabelle syntax and performs at least rudimentary highlighting (no symbol and sub/super script support here yet). For example, have a look at the List theory on github.

The highlighting is based on a TextMate grammar definition that I maintain on github. Of course, you can also just use this bundle to highlight Isabelle files in TextMate.

If you have ideas how to implement support symbols and sub/super scripts on github, let me know. It would definitely improve readability of Isabelle sources there.

Limitations

Obviously, an external highlighter like pygments will never have as much semantic information available as Isabelle itself (or any, really). The highlighting is mostly based on keywords and a few regular expressions, so don’t expect too much of it. It will passably recognize most of outer syntax, it won’t have any idea about inner syntax, type information, free or bound variables, declared constants or other semantic concepts. The idea is to increase readability a bit, not to rebuild an IDE in Python.

The inline code block support in the Haskell/pandoc filter above is a bit patchy: it expects an outer syntax entity like a definition (because pygments expects to render a .thy file), but often what you will want to mention in inline code blocks is actually a term fragment with a few symbols. In the form above, you’d have to at least sometimes include string quotes to indicate that pygments should render inner syntax (mostly just symbols). You could tweak the Haskell code to do that automatically for you if that is something that occurs frequently in your text.

The highlighter also renders RTF, LaTeX and other formats. RTF works surprisingly well. LaTeX support is less stellar (no sybmols at the moment), but for LaTeX you should use Isabelle’s excellent builtin antiquotations and formally checked sources for document generation anyway.

Feedback and improvements are welcome.

Markdown Syntax Cheat Sheet

Happy highlighting!