Commit f573bbae authored by Phil Jones's avatar Phil Jones

Add background colouring and dump keyword.

parent 2a9a59c5
{ {
"name": "finesse-syntax-jupyterlab", "name": "finesse-syntax-jupyterlab",
"version": "0.1.8", "version": "0.2.0",
"lockfileVersion": 1, "lockfileVersion": 1,
"requires": true, "requires": true,
"dependencies": { "dependencies": {
......
{ {
"name": "finesse-syntax-jupyterlab", "name": "finesse-syntax-jupyterlab",
"version": "0.1.8", "version": "0.2.0",
"description": "Syntax highlighting for kat script within JupyterLab.", "description": "Syntax highlighting for kat script within JupyterLab.",
"keywords": [ "keywords": [
"jupyter", "jupyter",
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
"url": "http://gitlab.sr.bham.ac.uk/pjj/finesse-syntax-jupyterlab.git" "url": "http://gitlab.sr.bham.ac.uk/pjj/finesse-syntax-jupyterlab.git"
}, },
"scripts": { "scripts": {
"build": "tsc", "build": "tsc && cp src/codemirror-multiplex.js lib/",
"clean": "rimraf lib tsconfig.tsbuildinfo", "clean": "rimraf lib tsconfig.tsbuildinfo",
"prepare": "jlpm run clean && jlpm run build", "prepare": "jlpm run clean && jlpm run build",
"watch": "tsc -w" "watch": "tsc -w"
......
import {
Mode
} from '@jupyterlab/codemirror'
import CodeMirror from 'codemirror';
import 'codemirror/mode/python/python';
import './codemirror-multiplex';
import './codemirror-finesse2';
declare module 'codemirror' {
function myMultiplexingMode(outerMode: CodeMirror.Mode<any>, ...others: object[]): CodeMirror.Mode<any>;
}
CodeMirror.defineMode("finesse-python", (config) => {
let pmode = CodeMirror.getMode(config, "python");
return CodeMirror.myMultiplexingMode(
pmode,
{
open: /(?=#kat2code)/,
close: /(?=""")/, // Match string end without consuming it
mode: CodeMirror.getMode(config, "text/x-finesse2"),
delimStyle: "delim"
}
)
});
CodeMirror.defineMIME("text/x-finesse-python", "finesse-python");
Mode.getModeInfo().push({
name: 'Finesse Python',
mime: "text/x-finesse-python",
mode: 'finesse-python',
ext: [],
});
import {
Mode
} from '@jupyterlab/codemirror'
import CodeMirror from 'codemirror'; import CodeMirror from 'codemirror';
import 'codemirror/mode/python/python';
import 'codemirror/addon/mode/multiplex';
declare module 'codemirror' {
// There should be a better way to do this to stop typescript
// complaining....
function multiplexingMode(outerMode: CodeMirror.Mode<any>, ...others: object[]): CodeMirror.Mode<any>;
}
const components = [ const components = [
'bs[12]\?', 'bs[12]\?',
'dbs', 'dbs',
...@@ -90,8 +76,12 @@ const commands = [ ...@@ -90,8 +76,12 @@ const commands = [
'pyterm', 'pyterm',
] ]
const reserved = [
'dump'
]
function wordListRegexp(words: string[]): RegExp { function wordListRegexp(words: string[]): RegExp {
return new RegExp("^((" + words.join(")|(") + "))\\b"); return new RegExp("^((" + words.join(")|(") + "))$");
} }
const regex = { const regex = {
...@@ -100,6 +90,7 @@ const regex = { ...@@ -100,6 +90,7 @@ const regex = {
"detector": wordListRegexp(detectors), "detector": wordListRegexp(detectors),
"name": /[a-zA-Z_][a-zA-Z0-9_-]/, "name": /[a-zA-Z_][a-zA-Z0-9_-]/,
"number": /^(([+-]?inf)|([+-]?(\d+\.\d*|\d*\.\d+|\d+)([eE]-?\d*\.?\d*)?j?([pnumkMGT])?))$/, "number": /^(([+-]?inf)|([+-]?(\d+\.\d*|\d*\.\d+|\d+)([eE]-?\d*\.?\d*)?j?([pnumkMGT])?))$/,
"reserved": wordListRegexp(reserved),
"variable": /\$\w+/ "variable": /\$\w+/
} }
...@@ -132,11 +123,15 @@ const regex = { ...@@ -132,11 +123,15 @@ const regex = {
CodeMirror.defineMode("finesse2", () => { CodeMirror.defineMode("finesse2", () => {
function tokenBase(stream: CodeMirror.StringStream, state: any) { function tokenBase(stream: CodeMirror.StringStream, state: any) {
return "line-background-finesse " + tokenLex(stream, state);
}
function tokenLex(stream: CodeMirror.StringStream, state: any) {
if (stream.sol()) { if (stream.sol()) {
state.firstOnLine = true; state.firstOnLine = true;
} }
if (stream.eatSpace()) { if (stream.eatSpace()) {
return null; return;
} }
if (/[#%]/.test(stream.peek())) { if (/[#%]/.test(stream.peek())) {
stream.skipToEnd(); stream.skipToEnd();
...@@ -145,45 +140,49 @@ CodeMirror.defineMode("finesse2", () => { ...@@ -145,45 +140,49 @@ CodeMirror.defineMode("finesse2", () => {
if (stream.peek() == '$') { if (stream.peek() == '$') {
stream.next(); stream.next();
} }
stream.eatWhile(/\w/); stream.eatWhile(/[^\s]/);
let style = null; let style = null;
let cur = stream.current(); let cur = stream.current();
//console.log(cur, state.prevToken);
if (state.firstOnLine) { if (state.firstOnLine) {
if (regex["component"].test(cur) || regex["detector"].test(cur)) { if (regex["component"].test(cur) || regex["detector"].test(cur)) {
// Component definition // Component definition
style = "keyword"; style = "keyword";
state.nextIsDef = true;
} else if (regex["command"].test(cur)) { } else if (regex["command"].test(cur)) {
// Command // Command
style = "builtin"; style = "builtin";
} }
} else if (state.prevToken == "keyword" && regex["name"].test(cur)) { } else if (state.nextIsDef && regex["name"].test(cur)) {
// Component name // Component name
style = "def"; style = "def";
state.nextIsDef = false;
} else if (regex["number"].test(cur)) { } else if (regex["number"].test(cur)) {
// Number // Number
style = "number"; style = "number";
} else if (regex["reserved"].test(cur)) {
// Reserved keyword
style = "qualifier";
} else if (regex["variable"].test(cur)) { } else if (regex["variable"].test(cur)) {
style = "variable-2"; style = "variable-2";
} }
if (style != null) { if (style != null) {
state.firstOnLine = false; state.firstOnLine = false;
state.prevToken = style;
return style; return style;
} }
stream.next(); stream.next();
} }
return <CodeMirror.Mode<any>> { return {
startState: function() { startState: function() {
return { return {
tokenize: tokenBase, tokenize: tokenBase,
firstOnLine: true, firstOnLine: true,
prevToken: <string> null nextIsDef: false
}; };
}, },
blankLine: function(state: any) { return "line-background-finesse";},
token: function(stream, state) { token: function(stream, state) {
return state.tokenize(stream, state) return state.tokenize(stream, state)
} }
...@@ -192,25 +191,3 @@ CodeMirror.defineMode("finesse2", () => { ...@@ -192,25 +191,3 @@ CodeMirror.defineMode("finesse2", () => {
CodeMirror.defineMIME("text/x-finesse2", "finesse2"); CodeMirror.defineMIME("text/x-finesse2", "finesse2");
CodeMirror.defineMode("finesse-python", (config) => {
let pmode = CodeMirror.getMode(config, "python");
return CodeMirror.multiplexingMode(
pmode,
{
open: /(?=#kat2code)/,
close: /(?=""")/, // Match string end without consuming it
mode: CodeMirror.getMode(config, "text/x-finesse2"),
delimStyle: "delim"
}
)
});
CodeMirror.defineMIME("text/x-finesse-python", "finesse-python");
Mode.getModeInfo().push({
name: 'Finesse Python',
mime: "text/x-finesse-python",
mode: 'finesse-python',
ext: [],
});
// CodeMirror, copyright (c) by Marijn Haverbeke and others
// Distributed under an MIT license: https://codemirror.net/LICENSE
//
// This is a clone of addon/mode/multiplexingMode.js from CodeMirror. The
// original blankLine function doesn't return the style returned by its
// sub-modes, so we have to copy the whole thing in here -_-
import CodeMirror from 'codemirror';
CodeMirror.myMultiplexingMode = function(outer /*, others */) {
// Others should be {open, close, mode [, delimStyle] [, innerStyle]} objects
var others = Array.prototype.slice.call(arguments, 1);
function indexOf(string, pattern, from, returnEnd) {
if (typeof pattern == "string") {
var found = string.indexOf(pattern, from);
return returnEnd && found > -1 ? found + pattern.length : found;
}
var m = pattern.exec(from ? string.slice(from) : string);
return m ? m.index + from + (returnEnd ? m[0].length : 0) : -1;
}
return {
startState: function() {
return {
outer: CodeMirror.startState(outer),
innerActive: null,
inner: null
};
},
copyState: function(state) {
return {
outer: CodeMirror.copyState(outer, state.outer),
innerActive: state.innerActive,
inner: state.innerActive && CodeMirror.copyState(state.innerActive.mode, state.inner)
};
},
token: function(stream, state) {
if (!state.innerActive) {
var cutOff = Infinity, oldContent = stream.string;
for (var i = 0; i < others.length; ++i) {
var other = others[i];
var found = indexOf(oldContent, other.open, stream.pos);
if (found == stream.pos) {
if (!other.parseDelimiters) stream.match(other.open);
state.innerActive = other;
// Get the outer indent, making sure to handle CodeMirror.Pass
var outerIndent = 0;
if (outer.indent) {
var possibleOuterIndent = outer.indent(state.outer, "", "");
if (possibleOuterIndent !== CodeMirror.Pass) outerIndent = possibleOuterIndent;
}
state.inner = CodeMirror.startState(other.mode, outerIndent);
return other.delimStyle && (other.delimStyle + " " + other.delimStyle + "-open");
} else if (found != -1 && found < cutOff) {
cutOff = found;
}
}
if (cutOff != Infinity) stream.string = oldContent.slice(0, cutOff);
var outerToken = outer.token(stream, state.outer);
if (cutOff != Infinity) stream.string = oldContent;
return outerToken;
} else {
var curInner = state.innerActive, oldContent = stream.string;
if (!curInner.close && stream.sol()) {
state.innerActive = state.inner = null;
return this.token(stream, state);
}
var found = curInner.close ? indexOf(oldContent, curInner.close, stream.pos, curInner.parseDelimiters) : -1;
if (found == stream.pos && !curInner.parseDelimiters) {
stream.match(curInner.close);
state.innerActive = state.inner = null;
return curInner.delimStyle && (curInner.delimStyle + " " + curInner.delimStyle + "-close");
}
if (found > -1) stream.string = oldContent.slice(0, found);
var innerToken = curInner.mode.token(stream, state.inner);
if (found > -1) stream.string = oldContent;
if (found == stream.pos && curInner.parseDelimiters)
state.innerActive = state.inner = null;
if (curInner.innerStyle) {
if (innerToken) innerToken = innerToken + " " + curInner.innerStyle;
else innerToken = curInner.innerStyle;
}
return innerToken;
}
},
indent: function(state, textAfter, line) {
var mode = state.innerActive ? state.innerActive.mode : outer;
if (!mode.indent) return CodeMirror.Pass;
return mode.indent(state.innerActive ? state.inner : state.outer, textAfter, line);
},
blankLine: function(state) {
var mode = state.innerActive ? state.innerActive.mode : outer;
var ret = null;
if (mode.blankLine) {
ret = mode.blankLine(state.innerActive ? state.inner : state.outer);
}
if (!state.innerActive) {
for (var i = 0; i < others.length; ++i) {
var other = others[i];
if (other.open === "\n") {
state.innerActive = other;
state.inner = CodeMirror.startState(other.mode, mode.indent ? mode.indent(state.outer, "", "") : 0);
}
}
} else if (state.innerActive.close === "\n") {
state.innerActive = state.inner = null;
}
return ret;
},
electricChars: outer.electricChars,
innerMode: function(state) {
return state.inner ? {state: state.inner, mode: state.innerActive.mode} : {state: state.outer, mode: outer};
}
};
};
CodeMirror.multiplexingMode = function(outer /*, others */) {
// Others should be {open, close, mode [, delimStyle] [, innerStyle]} objects
var others = Array.prototype.slice.call(arguments, 1);
function indexOf(string, pattern, from, returnEnd) {
if (typeof pattern == "string") {
var found = string.indexOf(pattern, from);
return returnEnd && found > -1 ? found + pattern.length : found;
}
var m = pattern.exec(from ? string.slice(from) : string);
return m ? m.index + from + (returnEnd ? m[0].length : 0) : -1;
}
return {
startState: function() {
return {
outer: CodeMirror.startState(outer),
innerActive: null,
inner: null
};
},
copyState: function(state) {
return {
outer: CodeMirror.copyState(outer, state.outer),
innerActive: state.innerActive,
inner: state.innerActive && CodeMirror.copyState(state.innerActive.mode, state.inner)
};
},
token: function(stream, state) {
if (!state.innerActive) {
var cutOff = Infinity, oldContent = stream.string;
for (var i = 0; i < others.length; ++i) {
var other = others[i];
var found = indexOf(oldContent, other.open, stream.pos);
if (found == stream.pos) {
if (!other.parseDelimiters) stream.match(other.open);
state.innerActive = other;
// Get the outer indent, making sure to handle CodeMirror.Pass
var outerIndent = 0;
if (outer.indent) {
var possibleOuterIndent = outer.indent(state.outer, "", "");
if (possibleOuterIndent !== CodeMirror.Pass) outerIndent = possibleOuterIndent;
}
state.inner = CodeMirror.startState(other.mode, outerIndent);
return other.delimStyle && (other.delimStyle + " " + other.delimStyle + "-open");
} else if (found != -1 && found < cutOff) {
cutOff = found;
}
}
if (cutOff != Infinity) stream.string = oldContent.slice(0, cutOff);
var outerToken = outer.token(stream, state.outer);
if (cutOff != Infinity) stream.string = oldContent;
return outerToken;
} else {
var curInner = state.innerActive, oldContent = stream.string;
if (!curInner.close && stream.sol()) {
state.innerActive = state.inner = null;
return this.token(stream, state);
}
var found = curInner.close ? indexOf(oldContent, curInner.close, stream.pos, curInner.parseDelimiters) : -1;
if (found == stream.pos && !curInner.parseDelimiters) {
stream.match(curInner.close);
state.innerActive = state.inner = null;
return curInner.delimStyle && (curInner.delimStyle + " " + curInner.delimStyle + "-close");
}
if (found > -1) stream.string = oldContent.slice(0, found);
var innerToken = curInner.mode.token(stream, state.inner);
if (found > -1) stream.string = oldContent;
if (found == stream.pos && curInner.parseDelimiters)
state.innerActive = state.inner = null;
if (curInner.innerStyle) {
if (innerToken) innerToken = innerToken + " " + curInner.innerStyle;
else innerToken = curInner.innerStyle;
}
return innerToken;
}
},
indent: function(state, textAfter, line) {
var mode = state.innerActive ? state.innerActive.mode : outer;
if (!mode.indent) return CodeMirror.Pass;
return mode.indent(state.innerActive ? state.inner : state.outer, textAfter, line);
},
blankLine: function(state) {
var mode = state.innerActive ? state.innerActive.mode : outer;
if (mode.blankLine) {
mode.blankLine(state.innerActive ? state.inner : state.outer);
}
if (!state.innerActive) {
for (var i = 0; i < others.length; ++i) {
var other = others[i];
if (other.open === "\n") {
state.innerActive = other;
state.inner = CodeMirror.startState(other.mode, mode.indent ? mode.indent(state.outer, "", "") : 0);
}
}
} else if (state.innerActive.close === "\n") {
state.innerActive = state.inner = null;
}
},
electricChars: outer.electricChars,
innerMode: function(state) {
return state.inner ? {state: state.inner, mode: state.innerActive.mode} : {state: state.outer, mode: outer};
}
};
};
CodeMirror.multiplexingMode = function(outer /*, others */) {
// Others should be {open, close, mode [, delimStyle] [, innerStyle]} objects
var others = Array.prototype.slice.call(arguments, 1);
function indexOf(string, pattern, from, returnEnd) {
if (typeof pattern == "string") {
var found = string.indexOf(pattern, from);
return returnEnd && found > -1 ? found + pattern.length : found;
}
var m = pattern.exec(from ? string.slice(from) : string);
return m ? m.index + from + (returnEnd ? m[0].length : 0) : -1;
}
return {
startState: function() {
return {
outer: CodeMirror.startState(outer),
innerActive: null,
inner: null
};
},
copyState: function(state) {
return {
outer: CodeMirror.copyState(outer, state.outer),
innerActive: state.innerActive,
inner: state.innerActive && CodeMirror.copyState(state.innerActive.mode, state.inner)
};
},
token: function(stream, state) {
if (!state.innerActive) {
var cutOff = Infinity, oldContent = stream.string;
for (var i = 0; i < others.length; ++i) {
var other = others[i];
var found = indexOf(oldContent, other.open, stream.pos);
if (found == stream.pos) {
if (!other.parseDelimiters) stream.match(other.open);
state.innerActive = other;
// Get the outer indent, making sure to handle CodeMirror.Pass
var outerIndent = 0;
if (outer.indent) {
var possibleOuterIndent = outer.indent(state.outer, "", "");
if (possibleOuterIndent !== CodeMirror.Pass) outerIndent = possibleOuterIndent;
}
state.inner = CodeMirror.startState(other.mode, outerIndent);
return other.delimStyle && (other.delimStyle + " " + other.delimStyle + "-open");
} else if (found != -1 && found < cutOff) {
cutOff = found;
}
}
if (cutOff != Infinity) stream.string = oldContent.slice(0, cutOff);
var outerToken = outer.token(stream, state.outer);
if (cutOff != Infinity) stream.string = oldContent;
return outerToken;
} else {
var curInner = state.innerActive, oldContent = stream.string;
if (!curInner.close && stream.sol()) {
state.innerActive = state.inner = null;
return this.token(stream, state);
}
var found = curInner.close ? indexOf(oldContent, curInner.close, stream.pos, curInner.parseDelimiters) : -1;
if (found == stream.pos && !curInner.parseDelimiters) {
stream.match(curInner.close);
state.innerActive = state.inner = null;
return curInner.delimStyle && (curInner.delimStyle + " " + curInner.delimStyle + "-close");
}
if (found > -1) stream.string = oldContent.slice(0, found);
var innerToken = curInner.mode.token(stream, state.inner);
if (found > -1) stream.string = oldContent;
if (found == stream.pos && curInner.parseDelimiters)
state.innerActive = state.inner = null;
if (curInner.innerStyle) {
if (innerToken) innerToken = innerToken + " " + curInner.innerStyle;
else innerToken = curInner.innerStyle;
}
return innerToken;
}
},
indent: function(state, textAfter, line) {
var mode = state.innerActive ? state.innerActive.mode : outer;
if (!mode.indent) return CodeMirror.Pass;
return mode.indent(state.innerActive ? state.inner : state.outer, textAfter, line);
},
blankLine: function(state) {
var mode = state.innerActive ? state.innerActive.mode : outer;
if (mode.blankLine) {
mode.blankLine(state.innerActive ? state.inner : state.outer);
}
if (!state.innerActive) {
for (var i = 0; i < others.length; ++i) {
var other = others[i];
if (other.open === "\n") {
state.innerActive = other;
state.inner = CodeMirror.startState(other.mode, mode.indent ? mode.indent(state.outer, "", "") : 0);
}
}
} else if (state.innerActive.close === "\n") {
state.innerActive = state.inner = null;
}
},
electricChars: outer.electricChars,
innerMode: function(state) {
return state.inner ? {state: state.inner, mode: state.innerActive.mode} : {state: state.outer, mode: outer};
}
};
};
CodeMirror.multiplexingMode = function(outer /*, others */) {
// Others should be {open, close, mode [, delimStyle] [, innerStyle]} objects
var others = Array.prototype.slice.call(arguments, 1);
function indexOf(string, pattern, from, returnEnd) {
if (typeof pattern == "string") {
var found = string.indexOf(pattern, from);
return returnEnd && found > -1 ? found + pattern.length : found;
}
var m = pattern.exec(from ? string.slice(from) : string);
return m ? m.index + from + (returnEnd ? m[0].length : 0) : -1;
}
return {
startState: function() {
return {
outer: CodeMirror.startState(outer),
innerActive: null,
inner: null
};
},
copyState: function(state) {
return {
outer: CodeMirror.copyState(outer, state.outer),
innerActive: state.innerActive,
inner: state.innerActive && CodeMirror.copyState(state.innerActive.mode, state.inner)
};
},
token: function(stream, state) {
if (!state.innerActive) {
var cutOff = Infinity, oldContent = stream.string;
for (var i = 0; i < others.length; ++i) {
var other = others[i];
var found = indexOf(oldContent, other.open, stream.pos);
if (found == stream.pos) {
if (!other.parseDelimiters) stream.match(other.open);
state.innerActive = other;
// Get the outer indent, making sure to handle CodeMirror.Pass
var outerIndent = 0;
if (outer.indent) {
var possibleOuterIndent = outer.indent(state.outer, "", "");
if (possibleOuterIndent !== CodeMirror.Pass) outerIndent = possibleOuterIndent;
}
state.inner = CodeMirror.startState(other.mode, outerIndent);
return other.delimStyle && (other.delimStyle + " " + other.delimStyle + "-open");
} else if (found != -1 && found < cutOff) {
cutOff = found;
}
}
if (cutOff != Infinity) stream.string = oldContent.slice(0, cutOff);
var outerToken = outer.token(stream, state.outer);
if (cutOff != Infinity) stream.string = oldContent;
return outerToken;
} else {
var curInner = state.innerActive, oldContent = stream.string;
if (!curInner.close && stream.sol()) {
state.innerActive = state.inner = null;
return this.token(stream, state);
}
var found = curInner.close ? indexOf(oldContent, curInner.close, stream.pos, curInner.parseDelimiters) : -1;
if (found == stream.pos && !curInner.parseDelimiters) {
stream.match(curInner.close);
state.innerActive = state.inner = null;
return curInner.delimStyle && (curInner.delimStyle + " " + curInner.delimStyle + "-close");
}
if (found > -1) stream.string = oldContent.slice(0, found);
var innerToken = curInner.mode.token(stream, state.inner);
if (found > -1) stream.string = oldContent;
if (found == stream.pos && curInner.parseDelimiters)
state.innerActive = state.inner = null;
if (curInner.innerStyle) {
if (innerToken) innerToken = innerToken + " " + curInner.innerStyle;
else innerToken = curInner.innerStyle;
}
return innerToken;
}
},
indent: function(state, textAfter, line) {
var mode = state.innerActive ? state.innerActive.mode : outer;
if (!mode.indent) return CodeMirror.Pass;
return mode.indent(state.innerActive ? state.inner : state.outer, textAfter, line);
},
blankLine: function(state) {
var mode = state.innerActive ? state.innerActive.mode : outer;
if (mode.blankLine) {
mode.blankLine(state.innerActive ? state.inner : state.outer);
}
if (!state.innerActive) {
for (var i = 0; i < others.length; ++i) {
var other = others[i];
if (other.open === "\n") {
state.innerActive = other;
state.inner = CodeMirror.startState(other.mode, mode.indent ? mode.indent(state.outer, "", "") : 0);
}
}
} else if (state.innerActive.close === "\n") {
state.innerActive = state.inner = null;
}
},
electricChars: outer.electricChars,
innerMode: function(state) {
return state.inner ? {state: state.inner, mode: state.innerActive.mode} : {state: state.outer, mode: outer};
}
};
};
...@@ -11,7 +11,7 @@ import { ...@@ -11,7 +11,7 @@ import {
} from '@jupyterlab/cells'; } from '@jupyterlab/cells';
import './codemirror-finesse'; import './codemirror-finesse-python';
const plugin: JupyterFrontEndPlugin<void> = { const plugin: JupyterFrontEndPlugin<void> = {
activate, activate,
...@@ -21,6 +21,10 @@ const plugin: JupyterFrontEndPlugin<void> = { ...@@ -21,6 +21,10 @@ const plugin: JupyterFrontEndPlugin<void> = {
}; };
function activate(app: JupyterFrontEnd, tracker: INotebookTracker) { function activate(app: JupyterFrontEnd, tracker: INotebookTracker) {
let style = document.createElement('style');
style.type = 'text/css';
style.innerHTML = '.finesse { background-color: rgba(0, 0, 0, 0.04); }';
document.getElementsByTagName('head')[0].appendChild(style);
tracker.widgetAdded.connect(activate_finesse) tracker.widgetAdded.connect(activate_finesse)
}; };
...@@ -58,6 +62,8 @@ function activate_finesse(sender: INotebookTracker, panel: NotebookPanel): void ...@@ -58,6 +62,8 @@ function activate_finesse(sender: INotebookTracker, panel: NotebookPanel): void
// the syntax highlighting to change on startup without selecting a // the syntax highlighting to change on startup without selecting a
// different cell // different cell
setTimeout(() => {check_all(panel)}, 500); setTimeout(() => {check_all(panel)}, 500);
setTimeout(() => {check_all(panel)}, 2000);
setTimeout(() => {check_all(panel)}, 5000);
}; };
export default plugin; export default plugin;
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment