12345678910111213141516171819202122232425262728293031323334353637383940414243444546 |
- import * as CodeMirror from "codemirror";
- import "codemirror/addon/edit/closebrackets";
- import "codemirror/addon/edit/matchbrackets";
- // import "codemirror/addon/hint/show-hint";
- // import "codemirror/addon/hint/anyword-hint";
- import "codemirror/addon/selection/active-line";
- import { CodeEditorMode } from "./../util/editorMode2"
- CodeEditorMode(CodeMirror);
- let codeEditor = null;
- export function initTextEditor (element) {
- let id = element;
- if (element[0] == '#') {
- id = element.substring(1);
- }
- codeEditor = CodeMirror.fromTextArea(document.getElementById(id), {
- theme: "ttcn",
- value: "",
- mode: "text/x-ivprog",
- indentUnit: 4,
- lineNumbers: true,
- matchBrackets: true,
- autoCloseBrackets: true,
- fixedGutter: true,
- styleActiveLine: true,
- readOnly: true
- });
- }
- export function disable (flag) {
- codeEditor.setOption("readOnly", flag);
- updateEditor();
- }
- export function updateEditor () {
- codeEditor.refresh();
- }
- export function setCode (code) {
- codeEditor.setValue(code);
- }
- export function getCode () {
- return codeEditor.getValue();
- }
|