jon.recoil.org
this repo has no description
1<!DOCTYPE html>
2<html xmlns="http://www.w3.org/1999/xhtml">
3<head>
4 <title>notebook.mld</title>
5 <meta charset="utf-8" />
6 <link rel="stylesheet" href="/assets/odoc.css" />
7 <link rel="stylesheet" href="/assets/odoc-notebook.css" />
8 <meta name="generator" content="odoc-notebook ab3675e" />
9 <meta name="viewport" content=
10 "width=device-width,initial-scale=1.0" />
11 <link rel="stylesheet" href="/assets/katex.min.css" />
12 <script src="/assets/katex.min.js"></script>
13 <script>
14 //<![CDATA[
15
16 document.addEventListener("DOMContentLoaded", function () {
17 var elements = Array.from(document.getElementsByClassName("odoc-katex-math"));
18 for (var i = 0; i < elements.length; i++) {
19 var el = elements[i];
20 var content = el.textContent;
21 var new_el = document.createElement("span");
22 new_el.setAttribute("class", "odoc-katex-math-rendered");
23 var display = el.classList.contains("display");
24 katex.render(content, new_el, { throwOnError: false, displayMode: display });
25 el.replaceWith(new_el);
26 }
27 });
28
29//]]>
30</script>
31
32 <style>
33 .cm-editor {
34 border: 1px solid #3e3e42;
35 border-radius: 0;
36 font-size: 14px;
37 }
38
39 .cm-editor.cm-focused {
40 outline: 2px solid #0066cc;
41 outline-offset: -1px;
42 }
43
44 .code-editor-container {
45 margin: 10px 0;
46 border: 1px solid #3e3e42;
47 border-radius: 4px;
48 overflow: hidden;
49 }
50
51 /* Ensure the panel at the top has proper rounded corners */
52 .code-editor-container .cm-panel-top:first-child {
53 border-radius: 4px 4px 0 0;
54 }
55
56 .cm-content {
57 padding: 8px;
58 }
59
60 .cm-scroller {
61 font-family: 'Fira Mono', 'Monaco', 'Consolas', monospace;
62 }
63
64 /* Dark theme overrides for CodeMirror */
65 .cm-editor {
66 border-bottom: none;
67 }
68
69 /* CodeMirror panel button styles */
70 .cm-button-panel button:hover:not(:disabled) {
71 filter: brightness(0.9);
72 }
73
74 .cm-button-panel button:disabled {
75 opacity: 0.6;
76 cursor: not-allowed;
77 }
78
79 /* Status bar styles */
80 .kernel-status-bar {
81 display: flex;
82 align-items: center;
83 padding: 4px 12px;
84 background-color: #252526;
85 border-top: 1px solid #3e3e42;
86 font-size: 12px;
87 color: #cccccc;
88 gap: 8px;
89 }
90
91 .kernel-status-indicator {
92 width: 8px;
93 height: 8px;
94 border-radius: 50%;
95 flex-shrink: 0;
96 }
97
98 .kernel-status-indicator.ready {
99 background-color: #4caf50;
100 }
101
102 .kernel-status-indicator.busy {
103 background-color: #ff9800;
104 animation: pulse 1s infinite;
105 }
106
107 .kernel-status-indicator.disconnected {
108 background-color: #f44336;
109 }
110
111 @keyframes pulse {
112 0% {
113 opacity: 1;
114 }
115 50% {
116 opacity: 0.5;
117 }
118 100% {
119 opacity: 1;
120 }
121 }
122
123 .kernel-status-text {
124 flex: 1;
125 }
126
127 .kernel-exec-time {
128 color: #808080;
129 font-size: 11px;
130 }
131
132 /* CSS3 Keyframes for highlight fade animation */
133 @keyframes highlight-fade {
134 0% {
135 background-color: rgba(255, 0, 0, 1.0);
136 box-shadow: 0 0 20px rgba(255, 0, 0, 0.8);
137 }
138 100% {
139 background-color: rgba(255, 0, 0, 0);
140 box-shadow: 0 0 20px rgba(255, 0, 0, 0);
141 }
142 }
143
144 /* Line highlighting styles */
145 .cm-line-highlight {
146 position: relative;
147 animation: highlight-fade 5s ease-out forwards;
148 background-color: rgba(255, 0, 0, 1.0);
149 }
150
151 /* Dark theme specific highlight - bright red */
152 .cm-editor.cm-dark .cm-line-highlight {
153 animation: highlight-fade 5s ease-out forwards, border-fade 5s ease-out forwards;
154 border-left: 3px solid rgba(255, 0, 0, 1.0);
155 }
156
157 @keyframes border-fade {
158 0% {
159 border-left-color: rgba(255, 0, 0, 1.0);
160 }
161 100% {
162 border-left-color: rgba(255, 0, 0, 0);
163 }
164 }
165
166 /* Read-only line styles */
167 .cm-line-readonly {
168 background-color: rgba(100, 100, 100, 0.2) !important;
169 position: relative;
170 }
171
172 .cm-line-readonly::before {
173 content: "";
174 position: absolute;
175 left: 0;
176 top: 0;
177 bottom: 0;
178 width: 3px;
179 background-color: #666;
180 }
181
182 /* Dark theme read-only lines */
183 .cm-editor.cm-dark .cm-line-readonly {
184 background-color: rgba(50, 50, 50, 0.5) !important;
185 }
186
187 .cm-editor.cm-dark .cm-line-readonly::before {
188 background-color: #888;
189 }
190
191 /* Cursor style for read-only lines */
192 .cm-line-readonly * {
193 cursor: not-allowed !important;
194 }
195 </style>
196</head>
197<body class="odoc">
198 <nav class="odoc-nav"><a href="../index.html">Up</a> - notebooks</nav>
199 <header class="odoc-preamble"><section id="section-odoc-notebook"><h1 id="odoc-notebook"><a href="#odoc-notebook" class="anchor"></a>Odoc Notebook</h1></section><p>Here's an odoc notebook with some code snippets in it.</p>
200
201 <div class="code-editor-container">
202 <div id="editor1"></div>
203 <div class="kernel-status-bar" id="status1">
204 <span class="kernel-status-indicator ready"></span>
205 <span class="kernel-status-text">Kernel ready</span>
206 <span class="kernel-exec-time"></span>
207 </div>
208 </div>
209
210 <p>Here's some more text.</p>
211
212 <div class="code-editor-container">
213 <div id="editor2"></div>
214 <div class="kernel-status-bar" id="status2">
215 <span class="kernel-status-indicator ready"></span>
216 <span class="kernel-status-text">Kernel ready</span>
217 <span class="kernel-exec-time"></span>
218 </div>
219 </div>
220
221 </header>
222 <div class="odoc-tocs">
223 <nav class="odoc-toc odoc-global-toc"><ul><li><a href="/notebook.html">Odoc Notebook</a></li></ul></nav>
224 </div>
225 <div class="odoc-content"></div>
226
227 <script type="module">
228 import {
229 EditorView,
230 EditorState,
231 basicSetup,
232 keymap,
233 indentWithTab,
234 oneDark,
235 Decoration,
236 StateField,
237 StateEffect,
238 showPanel
239 } from './dist/codemirror-bundle.js';
240
241 // Create state effects for highlighting
242 const addHighlight = StateEffect.define();
243 const removeHighlight = StateEffect.define();
244
245 // Create a state field to track highlighted lines
246 const highlightField = StateField.define({
247 create() { return Decoration.none; },
248 update(highlights, tr) {
249 highlights = highlights.map(tr.changes);
250 for (let e of tr.effects) {
251 if (e.is(addHighlight)) {
252 highlights = highlights.update({add: e.value, sort: true});
253 } else if (e.is(removeHighlight)) {
254 highlights = highlights.update({filter: () => false});
255 }
256 }
257 return highlights;
258 },
259 provide: f => EditorView.decorations.from(f)
260 });
261
262 // Kernel state management
263 const KernelState = {
264 READY: 'ready',
265 BUSY: 'busy',
266 DISCONNECTED: 'disconnected'
267 };
268
269 let kernelState = KernelState.READY;
270
271 // State effects for execution state
272 const setExecuting = StateEffect.define();
273 const setExecutionComplete = StateEffect.define();
274
275 // State field to track execution state
276 const executionState = StateField.define({
277 create() { return { executing: false, lastExecutionTime: null }; },
278 update(state, tr) {
279 for (let e of tr.effects) {
280 if (e.is(setExecuting)) {
281 return { executing: true, lastExecutionTime: null };
282 } else if (e.is(setExecutionComplete)) {
283 return { executing: false, lastExecutionTime: e.value };
284 }
285 }
286 return state;
287 }
288 });
289
290 // State effects for read-only lines
291 const setReadOnlyLines = StateEffect.define();
292 const clearReadOnlyLines = StateEffect.define();
293
294 // State field to track read-only line numbers
295 const readOnlyLinesField = StateField.define({
296 create() { return new Set(); },
297 update(lines, tr) {
298 for (let e of tr.effects) {
299 if (e.is(setReadOnlyLines)) {
300 return new Set(e.value);
301 } else if (e.is(clearReadOnlyLines)) {
302 return new Set();
303 }
304 }
305 return lines;
306 }
307 });
308
309 // State field for read-only line decorations
310 const readOnlyDecorations = StateField.define({
311 create(state) {
312 // Return empty decorations initially
313 return Decoration.none;
314 },
315 update(decorations, tr) {
316 // Always rebuild decorations based on current read-only lines
317 const readOnlyLines = tr.state.field(readOnlyLinesField);
318 const newDecorations = [];
319
320 readOnlyLines.forEach(lineNum => {
321 if (lineNum >= 1 && lineNum <= tr.state.doc.lines) {
322 const line = tr.state.doc.line(lineNum);
323 newDecorations.push(
324 Decoration.line({
325 attributes: {class: "cm-line-readonly"}
326 }).range(line.from)
327 );
328 }
329 });
330
331 return Decoration.set(newDecorations);
332 },
333 provide: f => EditorView.decorations.from(f)
334 });
335
336 // Extension that makes certain lines read-only using change filter
337 const readOnlyLineExtension = EditorState.changeFilter.of((tr) => {
338 const readOnlyLines = tr.state.field(readOnlyLinesField);
339 if (readOnlyLines.size === 0) return true; // Allow all changes if no read-only lines
340
341 const doc = tr.state.doc;
342
343 // Build ranges for all read-only lines
344 const readOnlyRanges = [];
345 readOnlyLines.forEach(lineNum => {
346 if (lineNum >= 1 && lineNum <= doc.lines) {
347 const line = doc.line(lineNum);
348 readOnlyRanges.push({from: line.from, to: line.to});
349 }
350 });
351
352 // Check if any changes overlap with read-only ranges
353 let allowed = true;
354 tr.changes.iterChangedRanges((fromA, toA) => {
355 for (const range of readOnlyRanges) {
356 // Check if this change overlaps with a read-only range
357 if (fromA < range.to && toA > range.from) {
358 allowed = false;
359 break;
360 }
361 }
362 });
363
364 return allowed;
365 });
366
367 // Create a panel with buttons
368 function createButtonPanel(editorId, statusId) {
369 return showPanel.of(() => {
370 const dom = document.createElement("div");
371 dom.className = "cm-button-panel";
372 dom.style.cssText = `
373 display: flex;
374 gap: 8px;
375 padding: 6px 12px;
376 background-color: #2d2d30;
377 border-bottom: 1px solid #3e3e42;
378 align-items: center;
379 justify-content: space-between;
380 `;
381
382 const buttonContainer = document.createElement("div");
383 buttonContainer.style.cssText = "display: flex; gap: 8px;";
384
385 // Run button
386 const runButton = document.createElement("button");
387 runButton.className = "cm-run-button";
388 runButton.innerHTML = '<svg viewBox="0 0 24 24" style="width: 14px; height: 14px; fill: currentColor;"><path d="M8 5v14l11-7z"/></svg>Run';
389 runButton.style.cssText = `
390 display: flex;
391 align-items: center;
392 gap: 6px;
393 padding: 4px 12px;
394 background-color: #0066cc;
395 color: white;
396 border: none;
397 border-radius: 3px;
398 font-size: 13px;
399 cursor: pointer;
400 `;
401
402 runButton.onclick = () => {
403 const editor = document.getElementById(editorId).editorView;
404 if (kernelState === KernelState.READY && editor) {
405 executeCode(editorId, statusId, editor);
406 }
407 };
408
409 // Highlight button
410 const highlightButton = document.createElement("button");
411 highlightButton.className = "cm-highlight-button";
412 highlightButton.innerHTML = '<svg viewBox="0 0 24 24" style="width: 14px; height: 14px; fill: currentColor;"><path d="M12 2L2 7v10c0 5.55 3.84 10.74 9 12 5.16-1.26 9-6.45 9-12V7l-10-5z"/></svg>Highlight';
413 highlightButton.style.cssText = `
414 display: flex;
415 align-items: center;
416 gap: 6px;
417 padding: 4px 12px;
418 background-color: #00a67e;
419 color: white;
420 border: none;
421 border-radius: 3px;
422 font-size: 13px;
423 cursor: pointer;
424 `;
425
426 highlightButton.onclick = () => {
427 const editor = document.getElementById(editorId).editorView;
428 if (editor) {
429 const lineCount = editor.state.doc.lines;
430 const linesToHighlight = [];
431 for (let i = 1; i <= Math.min(3, lineCount); i++) {
432 linesToHighlight.push(i);
433 }
434 highlightLines(editorId, linesToHighlight, 5000);
435 }
436 };
437
438 buttonContainer.appendChild(runButton);
439 buttonContainer.appendChild(highlightButton);
440
441 // Shortcut hint
442 const hint = document.createElement("span");
443 hint.textContent = "Shift + Enter to run";
444 hint.style.cssText = "font-size: 11px; color: #a0a0a0;";
445
446 dom.appendChild(buttonContainer);
447 dom.appendChild(hint);
448
449 return {
450 dom,
451 top: true, // Position panel at the top
452 update(update) {
453 // Update button states based on execution state
454 const state = update.state.field(executionState);
455 runButton.disabled = state.executing || kernelState !== KernelState.READY;
456 runButton.textContent = state.executing ? 'Running...' : 'Run';
457 if (!state.executing) {
458 runButton.innerHTML = '<svg viewBox="0 0 24 24" style="width: 14px; height: 14px; fill: currentColor;"><path d="M8 5v14l11-7z"/></svg>Run';
459 }
460 }
461 };
462 });
463 }
464
465 // Define the code snippets with their original content
466 const codeSnippets = [
467 {
468 id: 'editor1',
469 statusId: 'status1',
470 runId: 'run1',
471 highlightId: 'highlight1',
472 content: `let rec fib x =
473 match x with
474 | 0 -> 1
475 | 1 -> 1
476 | n -> fib (n-1) + fib (n-2);;
477val fib : int -> int = <fun>`,
478 readOnly: false
479 },
480 {
481 id: 'editor2',
482 statusId: 'status2',
483 runId: 'run2',
484 highlightId: 'highlight2',
485 content: `fib 10;;
486- : int = 89`,
487 readOnly: false
488 }
489 ];
490
491 // Custom keymap with Shift+Enter for execution
492 function createCustomKeymap(editorId, statusId) {
493 return keymap.of([
494 indentWithTab,
495 {
496 key: "Shift-Enter",
497 run: (view) => {
498 if (kernelState === KernelState.READY) {
499 executeCode(editorId, statusId, view);
500 }
501 return true;
502 }
503 }
504 ]);
505 }
506
507 // Initialize editors
508 codeSnippets.forEach(snippet => {
509 const container = document.getElementById(snippet.id);
510
511 // Create extensions array
512 const extensions = [
513 basicSetup,
514 oneDark,
515 highlightField,
516 executionState,
517 readOnlyLinesField,
518 readOnlyDecorations,
519 readOnlyLineExtension,
520 createButtonPanel(snippet.id, snippet.statusId),
521 createCustomKeymap(snippet.id, snippet.statusId),
522 EditorView.theme({
523 "&": {
524 fontSize: "14px",
525 fontFamily: "'Fira Mono', 'Monaco', 'Consolas', monospace"
526 },
527 ".cm-content": {
528 padding: "8px",
529 minHeight: "auto"
530 },
531 ".cm-line": {
532 paddingLeft: "4px"
533 }
534 }),
535 EditorView.lineWrapping
536 ];
537
538 // Add readonly extension if needed
539 if (snippet.readOnly) {
540 extensions.push(EditorState.readOnly.of(true));
541 }
542
543 const state = EditorState.create({
544 doc: snippet.content,
545 extensions: extensions
546 });
547
548 const view = new EditorView({
549 state,
550 parent: container
551 });
552
553 // Store editor reference for potential future use
554 container.editorView = view;
555 });
556
557 // Make output lines read-only by default after editors are initialized
558 setTimeout(() => {
559 // For editor1, line 6 contains the output "val fib : int -> int = <fun>"
560 makeReadOnlyLines('editor1', [6]);
561
562 // For editor2, line 2 contains the output "- : int = 89"
563 makeReadOnlyLines('editor2', [2]);
564 }, 100);
565
566 // Function to highlight lines with fade animation using decorations API
567 function highlightLines(editorId, lineNumbers, duration = 300000) {
568 const container = document.getElementById(editorId);
569 const editor = container?.editorView;
570 if (!editor) return;
571
572 const doc = editor.state.doc;
573 const decorations = [];
574
575 // Create line decorations
576 lineNumbers.forEach(lineNum => {
577 if (lineNum >= 1 && lineNum <= doc.lines) {
578 const line = doc.line(lineNum);
579 decorations.push(
580 Decoration.line({
581 attributes: {class: "cm-line-highlight"}
582 }).range(line.from)
583 );
584 }
585 });
586
587 // Apply decorations
588 editor.dispatch({
589 effects: addHighlight.of(decorations)
590 });
591
592 // Remove decorations after animation completes
593 setTimeout(() => {
594 editor.dispatch({
595 effects: removeHighlight.of(null)
596 });
597 }, duration);
598 }
599
600 // Alternative approach using a more direct method
601/* window.highlightLines = function(editorId, lineNumbers, duration = 3000) {
602 const container = document.getElementById(editorId);
603 const editor = container?.editorView;
604 if (!editor) return;
605
606 const doc = editor.state.doc;
607
608 // Get line elements and add highlight class
609 lineNumbers.forEach(lineNum => {
610 if (lineNum >= 1 && lineNum <= doc.lines) {
611 const line = doc.line(lineNum);
612 const lineElement = editor.domAtPos(line.from).node.parentElement;
613 if (lineElement && lineElement.classList.contains('cm-line')) {
614 lineElement.classList.add('cm-line-highlight');
615
616 // Remove the highlight after animation
617 setTimeout(() => {
618 lineElement.classList.add('fade-out');
619 setTimeout(() => {
620 lineElement.classList.remove('cm-line-highlight', 'fade-out');
621 }, duration);
622 }, 100);
623 }
624 }
625 });
626 }; */
627
628 // Function to update kernel status globally
629 function updateKernelStatus(state) {
630 kernelState = state;
631 const statusBars = document.querySelectorAll('.kernel-status-bar');
632 statusBars.forEach(bar => {
633 if (!bar.classList.contains('executing')) {
634 updateStatusBar(bar, state, getStatusText(state));
635 }
636 });
637 }
638
639 // Function to update individual status bar
640 function updateStatusBar(statusBar, state, text, execTime = '') {
641 const indicator = statusBar.querySelector('.kernel-status-indicator');
642 const statusText = statusBar.querySelector('.kernel-status-text');
643 const timeText = statusBar.querySelector('.kernel-exec-time');
644
645 // Remove all state classes and add the new one
646 indicator.classList.remove('ready', 'busy', 'disconnected');
647 indicator.classList.add(state);
648
649 statusText.textContent = text;
650 timeText.textContent = execTime;
651 }
652
653 // Get status text for a given state
654 function getStatusText(state) {
655 switch(state) {
656 case KernelState.READY:
657 return 'Kernel ready';
658 case KernelState.BUSY:
659 return 'Kernel busy';
660 case KernelState.DISCONNECTED:
661 return 'Kernel disconnected';
662 default:
663 return 'Unknown state';
664 }
665 }
666
667 // Simulate code execution for a specific editor
668 function executeCode(editorId, statusId, editor) {
669 const statusBar = document.getElementById(statusId);
670
671 // Update state to executing
672 editor.dispatch({
673 effects: setExecuting.of(null)
674 });
675
676 // Mark this cell as executing
677 statusBar.classList.add('executing');
678 updateStatusBar(statusBar, KernelState.BUSY, 'Executing...', '');
679
680 // Highlight the lines being executed (example: highlight lines 1-3)
681 const doc = editor.state.doc;
682 const linesToHighlight = [];
683 for (let i = 1; i <= Math.min(3, doc.lines); i++) {
684 linesToHighlight.push(i);
685 }
686 highlightLines(editorId, linesToHighlight, 3000);
687
688 // Simulate execution time
689 const startTime = Date.now();
690 setTimeout(() => {
691 const execTime = Date.now() - startTime;
692 statusBar.classList.remove('executing');
693 updateStatusBar(statusBar, kernelState, getStatusText(kernelState), `Executed in ${execTime}ms`);
694
695 // Update state to complete
696 editor.dispatch({
697 effects: setExecutionComplete.of(execTime)
698 });
699 }, Math.random() * 2000 + 500); // Random execution time between 0.5-2.5s
700 }
701
702
703 // Simulate kernel connection status changes (for demo)
704 setTimeout(() => {
705 window.updateKernelStatus(KernelState.DISCONNECTED);
706 setTimeout(() => {
707 window.updateKernelStatus(KernelState.READY);
708 }, 3000);
709 }, 5000);
710
711 // Update run button states when kernel status changes
712 function updateRunButtons() {
713 const runButtons = document.querySelectorAll('.run-button');
714 runButtons.forEach(button => {
715 if (!button.disabled || button.textContent === 'Run') {
716 button.disabled = kernelState !== KernelState.READY;
717 }
718 });
719 }
720
721 // Enhance updateKernelStatus to also update buttons
722 const originalUpdateKernelStatus = updateKernelStatus;
723 window.updateKernelStatus = function(state) {
724 kernelState = state;
725 const statusBars = document.querySelectorAll('.kernel-status-bar');
726 statusBars.forEach(bar => {
727 if (!bar.classList.contains('executing')) {
728 updateStatusBar(bar, state, getStatusText(state));
729 }
730 });
731 updateRunButtons();
732 };
733
734 // Function to set read-only lines
735 function makeReadOnlyLines(editorId, lineNumbers) {
736 const container = document.getElementById(editorId);
737 const editor = container?.editorView;
738 if (!editor) return;
739
740 editor.dispatch({
741 effects: setReadOnlyLines.of(lineNumbers)
742 });
743 }
744
745 // Function to clear read-only lines
746 function removeReadOnlyLines(editorId) {
747 const container = document.getElementById(editorId);
748 const editor = container?.editorView;
749 if (!editor) return;
750
751 editor.dispatch({
752 effects: clearReadOnlyLines.of(null)
753 });
754 }
755
756 // Expose functions globally
757 window.highlightLines = highlightLines;
758 window.makeReadOnlyLines = makeReadOnlyLines;
759 window.removeReadOnlyLines = removeReadOnlyLines;
760
761 window.notebookHighlight = {
762 // Highlight specific lines in an editor
763 // Usage: notebookHighlight.lines('editor1', [2, 4, 5])
764 lines: function(editorId, lineNumbers, duration = 300000) {
765 highlightLines(editorId, lineNumbers, duration);
766 },
767
768 // Highlight a range of lines
769 // Usage: notebookHighlight.range('editor1', 2, 5)
770 range: function(editorId, startLine, endLine, duration = 300000) {
771 const lines = [];
772 for (let i = startLine; i <= endLine; i++) {
773 lines.push(i);
774 }
775 highlightLines(editorId, lines, duration);
776 },
777
778 // Highlight all lines
779 // Usage: notebookHighlight.all('editor1')
780 all: function(editorId, duration = 300000) {
781 const editor = document.getElementById(editorId)?.editorView;
782 if (editor) {
783 const lineCount = editor.state.doc.lines;
784 this.range(editorId, 1, lineCount, duration);
785 }
786 }
787 };
788
789 // Read-only lines API
790 window.notebookReadOnly = {
791 // Set specific lines as read-only
792 // Usage: notebookReadOnly.set('editor1', [2, 6])
793 set: function(editorId, lineNumbers) {
794 makeReadOnlyLines(editorId, lineNumbers);
795 },
796
797 // Clear all read-only lines
798 // Usage: notebookReadOnly.clear('editor1')
799 clear: function(editorId) {
800 removeReadOnlyLines(editorId);
801 },
802
803 // Toggle read-only for specific lines
804 // Usage: notebookReadOnly.toggle('editor1', [2, 6])
805 toggle: function(editorId, lineNumbers) {
806 const editor = document.getElementById(editorId)?.editorView;
807 if (!editor) return;
808
809 const currentReadOnly = editor.state.field(readOnlyLinesField);
810 const newReadOnly = new Set(currentReadOnly);
811
812 lineNumbers.forEach(lineNum => {
813 if (newReadOnly.has(lineNum)) {
814 newReadOnly.delete(lineNum);
815 } else {
816 newReadOnly.add(lineNum);
817 }
818 });
819
820 makeReadOnlyLines(editorId, Array.from(newReadOnly));
821 }
822 };
823
824 </script>
825
826</body>
827</html>