Enabling math symbols and coq syntax highlighting

This post is about the tools used to produce this blog. The blog is freely hosted at blogger.com. MathJax is installed for printing equations like \[ \cos^2\theta-\sin^2\theta=\cos 2\theta. \]

In addition to mathematical equations, coq source code snippets are posted with SyntaxHighlighter. For example,

Lemma Rgt_0_mult_r2n_compat : forall (x r:R)(n:nat), x > 0 -> Rabs r >= 1 -> x * r ^ (2 *n) >= x.
Proof.
  intros.
  apply Ropp_ge_cancel.
  apply Rle_ge.
  rewrite <- 2?Ropp_mult_distr_l_reverse.
  apply Ropp_gt_lt_contravar in H.
  rewrite Ropp_0 in H.
  now apply Rlt_0_mult_r2n_compat.
Qed.

I started using this blog's MathJax installation directions, but it recommends directly editing the template source. That works, but if the template is ever edited with the GUI editor, the custom changes are lost.

Instead, I added two HTML/JavaScript widgets. The first widget is on the top of the page and gets run before the posts are shown. In order for this widget to have a visible artefact on the page, I had to

1. leave the widget untitled (it shows up as HTML/JavaScript when the title is blank)
2. edit the template source to move the widget into the navbar section.

(Click the below image to view it full-size)

Specifically this source code is included in the first widget for MathJax:

<script src='http://cdn.mathjax.org/mathjax/latest/MathJax.js' type='text/javascript'>    
    MathJax.Hub.Config({
        HTML: ["input/TeX","output/HTML-CSS"],
        TeX: { extensions: ["AMSmath.js","AMSsymbols.js"], 
               equationNumbers: { autoNumber: "AMS" } },
        extensions: ["tex2jax.js"],
        jax: ["input/TeX","output/HTML-CSS"],
        tex2jax: { inlineMath: [ ['$','$'], ["\\(","\\)"] ],
                   displayMath: [ ['$$','$$'], ["\\[","\\]"] ],
                   processEscapes: true },
        "HTML-CSS": { availableFonts: ["TeX"],
                      linebreaks: { automatic: true } }
    });
</script>

Beyond using the HTML/JavaScript widget, there is some futher customization for SyntaxHighlighter. Sometimes the blogger website is accessed through HTTPS. The recommended installation suggests using these links:

<link href='http://agorbatchev.typepad.com/pub/sh/3_0_83/styles/shCore.css' rel='stylesheet' type='text/css'/>
<link href='http://agorbatchev.typepad.com/pub/sh/3_0_83/styles/shThemeDefault.css' rel='stylesheet' type='text/css'/>
<script src='http://agorbatchev.typepad.com/pub/sh/3_0_83/scripts/shCore.js' type='text/javascript'/>

Instead I am using the links below, because they still work if http is replaced with https. When the blog is accessed through https, Firefox is implicitly replaces the http with https. Also the source code doesn't stand out enough, so the default style is tweaked slightly to add a border.

<link href='http://alexgorbatchev.com/pub/sh/current/styles/shCore.css' rel='stylesheet' type='text/css'/>
<link href='http://alexgorbatchev.com/pub/sh/current/styles/shThemeDefault.css' rel='stylesheet' type='text/css'/>
<script src='http://alexgorbatchev.com/pub/sh/current/scripts/shCore.js' type='text/javascript'/>

<style>
  .syntaxhighlighter {
    border: 1px solid #DADAD9 !important;
    margin-bottom: 20px !important;
    padding: 1px !important;
  }
</style>

The code to turn on SyntaxHighlighter needs to be separate and after the posts that use the plugin. I included it in a second widget located above the attribution bar. That location is good because it doesn't have visible artefacts and it is after the posts.

SyntaxHighlighter does not have builtin support (called a brush) for Coq's syntax. So in addition to enabling SyntaxHighlighter, a custom brush is defined for Coq that matches coqide's syntax highlighting:

<script language='javascript' type='text/javascript'>
    SyntaxHighlighter.brushes.Coq = function()
    { 
        var definitions = 'Definition Lemma Fixpoint '
                       + 'Variable Lemma Hypothesis';
        var keywords = 'Require Import Proof forall '
                       + 'Qed with as Hint Resolve in '
                       + 'Section Type End Prop';
        this.regexList = [
            { regex:
              /\(\*[\s\S]*?\*\)/gm,
              css: 'comments'
            }, // multiline comments
            { regex: new RegExp(this.getKeywords(keywords), 'gmi'), css: 'keyword' },
            { regex: new RegExp(this.getKeywords(definitions), 'gmi'), css: 'color2' }
        ];
    }; 
    SyntaxHighlighter.brushes.Coq.prototype = new SyntaxHighlighter.Highlighter();  
    SyntaxHighlighter.brushes.Coq.aliases   = ['coq'];

    SyntaxHighlighter.config.bloggerMode = true;
    SyntaxHighlighter.all();
</script>

To insert Coq source code inside of a post, switch to the HTML view for the post editor, then paste something like the following:

<pre class="brush: coq">Lemma Rgt_0_mult_r2n_compat : forall (x r:R)(n:nat), x > 0 -> Rabs r >= 1 -> x * r ^ (2 *n) >= x.
Proof.
  intros.
  apply Ropp_ge_cancel.
  apply Rle_ge.
  rewrite <- 2?Ropp_mult_distr_l_reverse.
  apply Ropp_gt_lt_contravar in H.
  rewrite Ropp_0 in H.
  now apply Rlt_0_mult_r2n_compat.
Qed.
</pre>