Created
October 22, 2018 13:06
-
-
Save lynn/5fa45281b3182808ee152d0759fe4d27 to your computer and use it in GitHub Desktop.
TamperMonkey syntax highlighting userscript for https://tio.run/
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// ==UserScript== | |
// @name TIO Syntax Highlighting | |
// @namespace http://tampermonkey.net/ | |
// @version 0.1 | |
// @description Syntax highlighting for https://tio.run/ | |
// @author Lynn | |
// @match https://tio.run/ | |
// @require https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.2/codemirror.min.js | |
// @require https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.2/mode/haskell/haskell.min.js | |
// @resource codeMirrorCss https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.32.0/codemirror.min.css | |
// @resource themeCss https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.40.2/theme/gruvbox-dark.min.css | |
// @grant GM_addStyle | |
// @grant GM_getResourceText | |
// ==/UserScript== | |
GM_addStyle(GM_getResourceText("codeMirrorCss")); | |
GM_addStyle(GM_getResourceText("themeCss")); | |
// Tweak CodeMirror a little to look like a TIO textarea: | |
GM_addStyle("div.CodeMirror {" | |
+ "font-family: 'DejaVu Sans Mono', monospace;" | |
+ "font-size: 16px;" | |
+ "box-shadow: none !important;" | |
+ "height: auto;" | |
+ "}"); | |
GM_addStyle(".CodeMirror pre { padding: 0 8px; }"); | |
// Hide CodeMirror div when Code toggle is closed. | |
GM_addStyle("input[id^=toggle-]:not(:checked) + h3 + textarea + div.CodeMirror { display: none; }"); | |
(function() { | |
'use strict'; | |
var cm = CodeMirror.fromTextArea(document.getElementById('code'), { | |
smartIndent: true, | |
mode: "text/x-haskell", | |
lineWrapping: true, | |
theme: "gruvbox-dark" | |
}); | |
cm.on("change", function(cm, change) { | |
document.getElementById('code').value = cm.getValue(); | |
document.getElementById('code').oninput(); | |
}); | |
})(); |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment