Remove editor folding and restore diagnostic navigation

Co-authored-by: Codex <codex@openai.com>

Author: rcosta358

package-lock.json

@@ -12,11 +12,15 @@
     "z3-solver": "4.16.0"
   },
   "dependencies": {
+    "@codemirror/autocomplete": "6.20.3",
+    "@codemirror/commands": "6.11.1",
     "@codemirror/lang-java": "6.0.2",
     "@codemirror/language": "6.12.4",
     "@codemirror/lint": "6.8.5",
+    "@codemirror/search": "6.7.2",
+    "@codemirror/state": "6.7.6",
+    "@codemirror/view": "6.43.13",
     "@lezer/highlight": "1.2.5",
-    "ansi_up": "6.0.6",
-    "codemirror": "6.0.2"
+    "ansi_up": "6.0.6"
   }
 }

package.json

@@ -31,6 +31,9 @@
 #lj-status[data-state="warning"] { color: #f6c177; }
 #lj-status:not(.sr-only) + #lj-results:not(:empty) { border-top: 1px solid #ffffff1a; }
 .main-content #lj-results pre { margin: 0; }
+.main-content #lj-results a { color: #e6edf7; text-decoration: underline; text-underline-offset: .2em; }
+.main-content #lj-results a:hover { color: #e6edf7; }
+.main-content #lj-results a:focus-visible { outline: 2px solid #7dd3fc; outline-offset: 3px; }
 #lj-results .ansi-black-fg { color: #111827; }
 #lj-results .ansi-bright-black-fg { color: #9ca3af; }
 #lj-status[data-state="error"],

playground/editor.css

@@ -13,5 +13,7 @@ export function editorDiagnostic(issue, length) {
 export function diagnosticHtml(output) {
   const ansi = new AnsiUp();
   ansi.use_classes = true;
-  return ansi.ansi_to_html(shortenLocations(output).replace(/^(?:\r?\n)+/, ''));
+  return ansi.ansi_to_html(shortenLocations(output).replace(/^(?:\r?\n)+/, ''))
+    .replace(/^(\/playground\/[^<\r\n]+:(\d+))(?=\r?\n|$|<\/span>)/gm,
+      '<a href="#lj-editor" data-line="$2">$1</a>');
 }

scripts/playground/diagnostics.mjs

@@ -2,6 +2,13 @@ import test from 'node:test';
 import assert from 'node:assert/strict';
 import { diagnosticHtml, editorDiagnostic } from './diagnostics.mjs';
 
+test('make diagnostic and declaration locations editor links without linking source excerpts', () => {
+  const html = diagnosticHtml('Error\n6 | String path = "/playground/Example.java:99";\n\n/files/playground/Example.java:6\u001b[0m\n\n--> Refinement declared here:\n/files/playground/Example.java:5\u001b[0m\n');
+  assert.match(html, /<a href="#lj-editor" data-line="6">\/playground\/Example.java:6<\/a>/);
+  assert.match(html, /<a href="#lj-editor" data-line="5">\/playground\/Example.java:5<\/a>/);
+  assert.equal((html.match(/<a /g) || []).length, 2);
+});
+
 test('omit leading CLI blank lines while preserving diagnostic spacing and colors', () => {
   const diagnostic = '\u001b[31mError\u001b[0m\n6 | code\n  | ^^^\n\nExample.java:6\n';
   assert.equal(diagnosticHtml('\n\n' + diagnostic), diagnosticHtml(diagnostic));

scripts/playground/diagnostics.test.mjs

@@ -0,0 +1,33 @@
+import { EditorState } from '@codemirror/state';
+import { lineNumbers, highlightActiveLineGutter, highlightSpecialChars, drawSelection, dropCursor, rectangularSelection, crosshairCursor, highlightActiveLine, keymap } from '@codemirror/view';
+import { indentOnInput, bracketMatching } from '@codemirror/language';
+import { history, defaultKeymap, historyKeymap } from '@codemirror/commands';
+import { highlightSelectionMatches, searchKeymap } from '@codemirror/search';
+import { closeBrackets, autocompletion, closeBracketsKeymap, completionKeymap } from '@codemirror/autocomplete';
+import { lintKeymap } from '@codemirror/lint';
+
+export const editorSetup = [
+  lineNumbers(),
+  highlightActiveLineGutter(),
+  highlightSpecialChars(),
+  history(),
+  drawSelection(),
+  dropCursor(),
+  EditorState.allowMultipleSelections.of(true),
+  indentOnInput(),
+  bracketMatching(),
+  closeBrackets(),
+  autocompletion(),
+  rectangularSelection(),
+  crosshairCursor(),
+  highlightActiveLine(),
+  highlightSelectionMatches(),
+  keymap.of([
+    ...closeBracketsKeymap,
+    ...defaultKeymap,
+    ...searchKeymap,
+    ...historyKeymap,
+    ...completionKeymap,
+    ...lintKeymap
+  ])
+];

scripts/playground/editor-setup.mjs

@@ -1,4 +1,4 @@
-import { EditorView } from 'codemirror';
+import { EditorView } from '@codemirror/view';
 import { javaLanguage } from '@codemirror/lang-java';
 import { HighlightStyle, LanguageSupport, syntaxHighlighting } from '@codemirror/language';
 import { styleTags, tags } from '@lezer/highlight';

scripts/playground/editor-theme.mjs

@@ -1,8 +1,9 @@
-import { EditorView, basicSetup } from 'codemirror';
+import { EditorView } from '@codemirror/view';
 import { setDiagnostics } from '@codemirror/lint';
 import { examples } from './examples.mjs';
 import { diagnosticHtml, editorDiagnostic } from './diagnostics.mjs';
 import { editorJava, editorTheme } from './editor-theme.mjs';
+import { editorSetup } from './editor-setup.mjs';
 
 const root = document.querySelector('#lj-playground');
 const example = document.querySelector('#lj-example');
@@ -18,7 +19,7 @@ let source;
 let timer;
 const view = new EditorView({
   doc: examples.positive,
-  extensions: [basicSetup, editorJava, editorTheme, EditorView.contentAttributes.of({ 'aria-label': 'Java source code' }),
+  extensions: [editorSetup, editorJava, editorTheme, EditorView.contentAttributes.of({ 'aria-label': 'Java source code' }),
     EditorView.updateListener.of(update => {
       if (update.docChanged) {
         queueMicrotask(() => view.dispatch(setDiagnostics(view.state, [])));
@@ -57,6 +58,20 @@ function render(result) {
     const pre = document.createElement('pre');
     const code = document.createElement('code');
     code.innerHTML = diagnosticHtml(issues.map(issue => issue.output).join('\n') + (result.details || ''));
+    for (const link of code.querySelectorAll('a[data-line]')) {
+      const lineNumber = Number(link.dataset.line);
+      if (lineNumber < 1 || lineNumber > view.state.doc.lines) continue;
+      link.onclick = event => {
+        event.preventDefault();
+        const issue = issues.find(issue => issue.line === lineNumber);
+        const mark = issue && editorDiagnostic(issue, view.state.doc.length);
+        const line = view.state.doc.line(lineNumber);
+        const anchor = mark?.from ?? line.from + line.text.search(/\S|$/);
+        view.dom.scrollIntoView({ block: 'center', inline: 'nearest' });
+        view.dispatch({ selection: { anchor }, effects: EditorView.scrollIntoView(anchor, { y: 'center' }) });
+        view.focus();
+      };
+    }
     pre.append(code);
     results.append(pre);
   }