language-web/src/main/webapp/script.js


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

var baseUrl = window.location.pathname;
var fileIndex = baseUrl.indexOf("index.html");
if (fileIndex > 0)
    baseUrl = baseUrl.slice(0, fileIndex)
require.config({
    baseUrl: baseUrl,
    paths: {
        "text": "webjars/requirejs-text/2.26.0.M1/text",
        "jquery": "webjars/jquery/3.6.0/jquery.min",
        "xtext/xtext-codemirror": "xtext/2.26.0.M1/xtext-codemirror",
    },
    packages: [{
        name: "codemirror",
        location: "webjars/codemirror/5.52.2",
        main: "lib/codemirror"
    }]
});
require(["xtext-resources/generated/mode-problem", "xtext/xtext-codemirror"], function(mode, xtext) {
	xtext.createEditor({baseUrl: baseUrl, indentUnit: 4,});
});