IHaskell/html/custom.js

74 lines
2.6 KiB
JavaScript
Raw Normal View History

$([IPython.events]).on('app_initialized.NotebookApp', function(){
// add here logic that shoudl be run once per **page load**
// like adding specific UI, or changing the default value
// of codecell highlight.
// Set tooltips to be triggered after 800ms
IPython.tooltip.time_before_tooltip = 800;
2014-03-18 22:51:56 -07:00
// IPython keycodes.
2014-11-22 21:39:18 -08:00
var space = 32;
var downArrow = 40;
IPython.keyboard.keycodes.down = downArrow; // space
IPython.CodeCell.options_default['cm_config']['mode'] = 'haskell';
CodeMirror.requireMode('haskell', function(){
// Create a multiplexing mode that uses Haskell highlighting by default but
// doesn't highlight command-line directives.
CodeMirror.defineMode("ihaskell", function(config) {
return CodeMirror.multiplexingMode(
CodeMirror.getMode(config, "haskell"),
{
open: /:(?=!)/, // Matches : followed by !, but doesn't consume !
close: /^(?!!)/, // Matches start of line not followed by !, doesn't consume character
mode: CodeMirror.getMode(config, "text/plain"),
delimStyle: "delimit"
}
);
});
cells = IPython.notebook.get_cells();
for(var i in cells){
c = cells[i];
if (c.cell_type === 'code') {
// Force the mode to be Haskell
// This is necessary, otherwise sometimes highlighting just doesn't happen.
// This may be an IPython bug.
c.code_mirror.setOption('mode', 'ihaskell');
c.auto_highlight()
}
}
});
2014-01-07 22:48:01 -05:00
// Prevent the pager from surrounding everything with a <pre>
IPython.Pager.prototype.append_text = function (text) {
this.pager_element.find(".container").append($('<div/>').html(IPython.utils.autoLinkUrls(text)));
2014-01-07 22:48:01 -05:00
};
});
2014-01-05 14:35:22 -05:00
$([IPython.events]).on('shell_reply.Kernel', function() {
// Add logic here that should be run once per reply.
2014-01-05 19:01:04 -05:00
// Highlight things with a .highlight-code class
// The id is the mode with with to highlight
2013-12-30 17:18:10 -05:00
$('.highlight-code').each(function() {
var $this = $(this),
$code = $this.html(),
$unescaped = $('<div/>').html($code).text();
$this.empty();
2013-12-30 17:18:10 -05:00
// Never highlight this block again.
this.className = "";
CodeMirror(this, {
value: $unescaped,
2013-12-30 17:18:10 -05:00
mode: this.id,
lineNumbers: false,
readOnly: true
});
});
2014-01-05 14:35:22 -05:00
});