More fixes for issue 57.

- move the selection highlight code to the Text mode.
- store $selectionOccurrences in the editor session.
- add option to toggle selection highlighting. In demo page as well.

demo/demo.js

@@ -257,6 +257,10 @@ exports.launch = function(env) {
         env.editor.renderer.setShowPrintMargin(checked);
     });
 
+    bindCheckbox("highlight_selected_word", function(checked) {
+        env.editor.setHighlightSelectedWord(checked);
+    });
+
     function bindCheckbox(id, callback) {
         var el = document.getElementById(id);
         var onCheck = function() {