Skip to content

Commit f7d8e57

Browse files
authored
Webview & File Event Handling Improvements (#27)
1 parent 6f37efb commit f7d8e57

File tree

5 files changed

+59
-32
lines changed

5 files changed

+59
-32
lines changed
94 Bytes
Binary file not shown.

client/src/webview/renderers/diagnostics/derivation-nodes.ts

Lines changed: 17 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -30,25 +30,21 @@ function renderJsonTree(
3030
// VarDerivationNode
3131
if ("var" in node) {
3232
const placement = error.translationTable?.[node.var];
33+
if (!placement) return `<span class="node-var">${node.var}</span>`;
34+
3335
const filePath = (placement as any)?.file ?? error.file;
34-
const filename = filePath ? filePath.split("/").pop() : "";
35-
const position = placement?.position;
36-
const tooltipData = placement
37-
? `${filename}:${(position?.line ?? 0) + 1}:${(position?.column ?? 0) + 1}`
38-
: "No location available";
39-
const fileAttr = filePath ? `data-file="${filePath}"` : "";
40-
const lineAttr = position ? `data-line="${position.line}"` : "";
41-
const columnAttr = position ? `data-column="${position.column}"` : "";
42-
const clickableClass = hasOrigin ? "derivable-node" : "";
43-
const pathAttr = hasOrigin ? `data-node-path="${path}"` : "";
44-
const idAttr = hasOrigin ? `data-error-id="${errorId}"` : "";
45-
return `<span class="node-var tooltip clickable ${clickableClass}" data-tooltip="${tooltipData}" ${fileAttr} ${lineAttr} ${columnAttr} ${pathAttr} ${idAttr}>${node.var}</span>`;
36+
const filename = filePath.split("/").pop() ?? "";
37+
const tooltipData = `${filename}:${(placement.position?.line ?? 0) + 1}`;
38+
const classes = `node-var tooltip clickable ${hasOrigin ? "derivable-node" : ""}`.trim();
39+
const attrs = hasOrigin ? ` data-node-path="${path}" data-error-id="${errorId}"` : "";
40+
const fileAttr = ` data-file="${filePath}" data-line="${placement.position?.line ?? 0}" data-column="${placement.position?.column ?? 0}"`;
41+
return `<span class="${classes}" data-tooltip="${tooltipData}"${fileAttr}${attrs}>${node.var}</span>`;
4642
}
4743

4844
// ValDerivationNode
4945
if ("value" in node) {
5046
const valueNode = node as ValDerivationNode;
51-
const valClass = typeof valueNode.value === "number" ? "node-number" : "node-value";
47+
const valClass = typeof valueNode.value === "number" ? "node-number" : typeof valueNode.value === "boolean" ? "node-boolean" : "node-value";
5248
const clickableClass = hasOrigin ? "derivable-node clickable" : "";
5349
const pathAttr = hasOrigin ? `data-node-path="${path}"` : "";
5450
const idAttr = hasOrigin ? `data-error-id="${errorId}"` : "";
@@ -65,7 +61,7 @@ function renderJsonTree(
6561
// UnaryDerivationNode
6662
if ("operand" in node) {
6763
const operandHtml = renderJsonTree(error, node.operand, errorId, `${path}.operand`, expandedPaths);
68-
return `${node.op}(${operandHtml})`;
64+
return node.op === "-" ? `(${node.op}${operandHtml})` : `${node.op}${operandHtml}`;
6965
}
7066

7167
// fallback
@@ -116,11 +112,13 @@ export function renderDerivationNode(error: RefinementError, node: ValDerivation
116112
const expansions = getExpansions(errorId);
117113
return /*html*/ `
118114
<div class="container derivation-container" data-error-id="${errorId}">
119-
${renderJsonTree(error, node.origin || node, errorId, "root", expansions)}
120-
${expansions.size === 0 ? '<span class="node-expand-indicator">&nbsp;(click to expand)</span>' : ''}
115+
<div style="flex: 1;">
116+
${renderJsonTree(error, node.origin || node, errorId, "root", expansions)}
117+
${expansions.size === 0 ? '<span class="node-expand-indicator">&nbsp;(click to expand)</span>' : ''}
118+
</div>
119+
<button class="reset-btn derivation-reset-btn" data-error-id="${errorId}" ${expansions.size === 0 ? "disabled" : ""}>
120+
121+
</button>
121122
</div>
122-
<button class="reset-btn derivation-reset-btn" data-error-id="${errorId}" ${expansions.size === 0 ? "disabled" : ""}>
123-
Reset
124-
</button>
125123
`;
126124
}

client/src/webview/renderers/diagnostics/errors.ts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ export function renderError(error: LJError): string {
3838
const e = error as RefinementError;
3939
return /*html*/`
4040
${header}
41-
${renderSection('Expected', renderDerivationNode(e, e.expected))}
41+
${renderSection('Expected', `<pre>${e.expected.value}</pre>`)}
4242
${renderSection('Found', renderDerivationNode(e, e.found))}
4343
${location}
4444
`;

client/src/webview/styles.ts

Lines changed: 19 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -90,35 +90,47 @@ export function getStyles(): string {
9090
position: relative;
9191
}
9292
.node-value {
93-
color: #CE9178;
93+
color: var(--vscode-editor-foreground);
9494
}
9595
.node-number {
9696
color: #B5CEA8;
9797
}
98+
.node-boolean {
99+
color: #569CD6;
100+
}
98101
.node-expand-indicator {
99102
opacity: 0.5;
100103
font-style: italic;
101104
}
102105
.clickable {
103106
cursor: pointer;
104-
}
105-
.clickable:hover {
106107
text-decoration: underline;
107108
text-decoration-style: dotted;
108109
}
110+
.clickable:hover {
111+
font-weight: bold;
112+
}
113+
.derivation-container {
114+
display: flex;
115+
justify-content: space-between;
116+
align-items: center;
117+
gap: 1rem;
118+
}
109119
.reset-btn {
110-
margin: 0.5rem 0;
120+
margin: 0;
111121
padding: 0.4rem 0.8rem;
112-
background-color: var(--vscode-button-background);
122+
background-color: transparent;
113123
color: var(--vscode-button-foreground);
114124
border: none;
115125
border-radius: 4px;
116126
cursor: pointer;
117127
font-family: var(--vscode-font-family);
118-
font-size: var(--vscode-font-size);
128+
font-size: larger;
129+
flex-shrink: 0;
130+
opacity: 0.7;
119131
}
120132
.reset-btn:hover {
121-
background-color: var(--vscode-button-hoverBackground);
133+
font-weight: bold;
122134
}
123135
.reset-btn:disabled {
124136
opacity: 0.5;

server/src/main/java/LJDiagnosticsService.java

Lines changed: 22 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,21 @@ public void generateDiagnostics(String uri) {
7272
sendDiagnosticsNotification(diagnostics);
7373
}
7474

75+
/**
76+
* Checks if a file URI is within the source path
77+
* @param uri the file URI
78+
* @return true if the file is within sourcePath, false otherwise
79+
*/
80+
private boolean isFileInSourcePath(String uri) {
81+
try {
82+
Path filePath = Paths.get(new URI(uri));
83+
Path sourcePathObj = Paths.get(sourcePath);
84+
return filePath.startsWith(sourcePathObj);
85+
} catch (Exception e) {
86+
return false;
87+
}
88+
}
89+
7590
/**
7691
* Clear a diagnostic for a specific URI
7792
* @param uri the URI of the document
@@ -88,8 +103,10 @@ public void clearDiagnostic(String uri) {
88103
*/
89104
@Override
90105
public void didOpen(DidOpenTextDocumentParams params) {
106+
String uri = params.getTextDocument().getUri();
107+
if (!isFileInSourcePath(uri)) return;
91108
System.out.println("Document opened — checking diagnostics");
92-
generateDiagnostics(params.getTextDocument().getUri());
109+
generateDiagnostics(uri);
93110
}
94111

95112
/**
@@ -98,8 +115,9 @@ public void didOpen(DidOpenTextDocumentParams params) {
98115
*/
99116
@Override
100117
public void didSave(DidSaveTextDocumentParams params) {
101-
System.out.println("Document saved — checking diagnostics");
102118
String uri = params.getTextDocument().getUri();
119+
if (!isFileInSourcePath(uri)) return;
120+
System.out.println("Document saved — checking diagnostics");
103121
clearDiagnostic(uri);
104122
generateDiagnostics(uri);
105123
}
@@ -111,16 +129,15 @@ public void didSave(DidSaveTextDocumentParams params) {
111129
@Override
112130
public void didClose(DidCloseTextDocumentParams params) {
113131
String uri = params.getTextDocument().getUri();
132+
if (!isFileInSourcePath(uri)) return;
114133
try {
115134
// check if the file still exists on disk
116135
File file = new File(new URI(uri));
117136
if (!file.exists()) {
118137
System.out.println("File deleted — clearing diagnostic");
119138
clearDiagnostic(uri);
120139
}
121-
} catch (Exception e) {
122-
System.out.println("Error checking if file exists: " + e.getMessage());
123-
}
140+
} catch (Exception e) {}
124141
}
125142

126143
@Override

0 commit comments

Comments
 (0)