Skip to content

Commit 2ffd387

Browse files
rcosta358rcosta358
authored
Webview Navigation (#41)
1 parent 36b652e commit 2ffd387

File tree

10 files changed

+204
-121
lines changed

10 files changed

+204
-121
lines changed

‎client/src/webview/mermaid.ts‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ import type { StateMachine } from "../types/fsm";
66
* @returns Mermaid diagram string
77
*/
88
export function createMermaidDiagram(sm: StateMachine): string {
9+
if (!sm) return '';
10+
911
const lines: string[] = [];
1012

1113
// header

‎client/src/webview/script.ts‎

Lines changed: 28 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,11 @@
1-
import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/derivation-nodes";
2-
import { renderCorrect } from "./views/correct";
1+
import { handleDerivableNodeClick, handleDerivationResetClick } from "./views/verification/derivation-nodes";
32
import { renderLoading } from "./views/loading";
4-
import { renderErrors } from "./views/errors";
5-
import { renderWarnings } from "./views/warnings";
63
import { renderStateMachineView } from "./views/diagram";
74
import { createMermaidDiagram, renderMermaidDiagram } from "./mermaid";
8-
import type { LJError, LJWarning, LJDiagnostic } from "../types/diagnostics";
5+
import type { LJDiagnostic } from "../types/diagnostics";
96
import type { StateMachine } from "../types/fsm";
7+
import type { NavTab } from "./views/sections";
8+
import { renderVerificationView } from "./views/verification/verification";
109

1110
/**
1211
* Initializes the webview script
@@ -16,12 +15,12 @@ import type { StateMachine } from "../types/fsm";
1615
*/
1716
export function getScript(vscode: any, document: any, window: any) {
1817
const root = document.getElementById('root');
19-
let fileErrors: LJError[] = [];
20-
let fileWarnings: LJWarning[] = [];
18+
let diagnostics: LJDiagnostic[] = [];
2119
let showAllDiagnostics = false;
2220
let currentFile: string | undefined;
2321
let expandedErrors = new Set<number>();
24-
let stateMachineView = '';
22+
let stateMachine: StateMachine | undefined;
23+
let selectedTab: NavTab = 'verification';
2524

2625
// initial state
2726
root.innerHTML = renderLoading();
@@ -91,31 +90,34 @@ export function getScript(vscode: any, document: any, window: any) {
9190
}
9291
return;
9392
}
93+
94+
// nav tab click
95+
if (target.classList.contains('nav-tab')) {
96+
e.stopPropagation();
97+
const tab = target.getAttribute('data-tab') as NavTab;
98+
if (tab && tab !== selectedTab) {
99+
selectedTab = tab;
100+
updateView();
101+
}
102+
return;
103+
}
94104
});
95105

96106
window.addEventListener('message', event => {
97107
const msg = event.data;
98108
if (msg.type === 'diagnostics') {
99-
const diagnostics = msg.diagnostics as LJDiagnostic[];
100-
const errors = diagnostics.filter((d: LJDiagnostic) => d.category === 'error') as LJError[];
101-
const warnings = diagnostics.filter((d: LJDiagnostic) => d.category === 'warning') as LJWarning[];
102-
103-
fileErrors = errors;
104-
fileWarnings = warnings;
105-
109+
diagnostics = msg.diagnostics as LJDiagnostic[];
106110
updateView();
107111
} else if (msg.type === 'file') {
108112
currentFile = msg.file;
109113
if (!showAllDiagnostics) updateView();
110114
} else if (msg.type === 'fsm') {
111115
if (!msg.sm) {
112-
stateMachineView = '';
116+
stateMachine = undefined;
113117
updateView();
114118
return;
115119
}
116-
const sm = msg.sm as StateMachine;
117-
const diagram = createMermaidDiagram(sm);
118-
stateMachineView = renderStateMachineView(sm, diagram);
120+
stateMachine = msg.sm as StateMachine;
119121
updateView();
120122
}
121123
});
@@ -124,12 +126,12 @@ export function getScript(vscode: any, document: any, window: any) {
124126
* Updates the webview content based on the current state
125127
*/
126128
function updateView() {
127-
let mainView = fileErrors.length > 0 ? renderErrors(fileErrors, showAllDiagnostics, currentFile, expandedErrors) : renderCorrect(showAllDiagnostics);
128-
let warningsView = fileWarnings.length > 0 ? renderWarnings(fileWarnings, showAllDiagnostics, currentFile) : '';
129-
root.innerHTML = mainView + warningsView + stateMachineView;
130-
131-
// re-render mermaid diagram after DOM update
132-
if (stateMachineView) renderMermaidDiagram(document, window);
129+
if (selectedTab === 'verification') {
130+
root.innerHTML = renderVerificationView(diagnostics, showAllDiagnostics, currentFile, expandedErrors, selectedTab)
131+
} else {
132+
const diagram = createMermaidDiagram(stateMachine);
133+
root.innerHTML = renderStateMachineView(stateMachine, diagram, selectedTab);
134+
if (stateMachine) renderMermaidDiagram(document, window);
135+
}
133136
}
134137
}
135-

‎client/src/webview/styles.ts‎

Lines changed: 60 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,45 @@ export function getStyles(): string {
3333
display: inline;
3434
margin-bottom: 0.5rem;
3535
}
36+
nav ul {
37+
display: flex;
38+
gap: 1rem;
39+
padding: 0;
40+
margin: 0;
41+
justify-content: center;
42+
}
43+
nav ul li {
44+
padding-right: 1rem;
45+
border-right: 1px solid var(--vscode-panel-border);
46+
}
47+
nav ul li:last-child {
48+
border-right: none;
49+
}
50+
nav {
51+
padding-bottom: 1.5rem;
52+
}
53+
nav button {
54+
color: var(--vscode-foreground);
55+
background: none;
56+
border: none;
57+
text-decoration: none;
58+
cursor: pointer;
59+
padding: 0;
60+
opacity: 0.8;
61+
text-transform: uppercase;
62+
font-size: 11px;
63+
}
64+
nav .selected {
65+
opacity: 1;
66+
text-decoration: underline;
67+
text-decoration-color: #0078D5;
68+
text-underline-offset: 6px;
69+
text-decoration-thickness: 1px;
70+
}
71+
nav button:hover {
72+
opacity: 1;
73+
background: none;
74+
}
3675
.container {
3776
margin: 0;
3877
padding: 0.5rem;
@@ -46,28 +85,20 @@ export function getStyles(): string {
4685
overflow: visible;
4786
position: relative;
4887
}
49-
.header {
50-
display: flex;
51-
justify-content: space-between;
52-
align-items: start;
53-
}
54-
.diagnostic-header {
55-
margin: 1rem 0;
56-
}
5788
ul {
5889
list-style-type: none;
5990
padding: 0;
6091
margin: 0;
6192
}
93+
.diagnostic-header {
94+
margin: 1rem 0;
95+
}
6296
.diagnostic-item {
6397
background-color: var(--vscode-textBlockQuote-background);
6498
padding: 0.5rem 1rem;
6599
margin-bottom: 1rem;
66100
border-radius: 4px;
67101
}
68-
.diagnostic-item h3 {
69-
margin-top: 0;
70-
}
71102
.error-item {
72103
border-left: 4px solid var(--vscode-errorForeground);
73104
}
@@ -170,6 +201,21 @@ export function getStyles(): string {
170201
.show-more-button:hover {
171202
background-color: var(--vscode-editor-background);
172203
}
204+
.show-all-button {
205+
text-align: center;
206+
font-size: 0.8rem;
207+
opacity: 0.6;
208+
margin-bottom: 1rem;
209+
padding: 0;
210+
background: none;
211+
display: flex;
212+
justify-content: center;
213+
border: none;
214+
text-decoration: underline;
215+
}
216+
.show-all-button:hover {
217+
background: none;
218+
}
173219
.extra-content {
174220
margin-top: 1rem;
175221
}
@@ -202,15 +248,15 @@ export function getStyles(): string {
202248
z-index: 1000;
203249
pointer-events: none;
204250
}
251+
.info {
252+
margin: 1rem 0;
253+
}
205254
.more-indicator {
206255
text-align: center;
207256
font-size: 0.8rem;
208257
opacity: 0.6;
209258
margin-bottom: 1rem;
210259
}
211-
.info {
212-
margin: 1rem 0;
213-
}
214260
table {
215261
width: 100%;
216262
border-collapse: collapse;

‎client/src/webview/views/correct.ts‎

Lines changed: 0 additions & 13 deletions
This file was deleted.

‎client/src/webview/views/diagram.ts‎

Lines changed: 17 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,23 @@
11
import type { StateMachine } from "../../types/fsm";
2+
import { renderMainHeader, type NavTab } from "./sections";
23

3-
export function renderStateMachineView(sm: StateMachine, diagram: string): string {
4+
export function renderStateMachineView(sm: StateMachine, diagram: string, selectedTab: NavTab = 'state-machine'): string {
45
return /*html*/`
5-
<div class="diagram-section">
6-
<div class="diagram-container">
7-
<pre class="mermaid">${diagram}</pre>
8-
</div>
9-
<div>
10-
<p><strong>States:</strong> ${sm.states.join(', ')}</p>
11-
<p><strong>Initial state:</strong> ${sm.initial}</p>
12-
<p><strong>Number of states:</strong> ${sm.states.length}</p>
13-
<p><strong>Number of transitions:</strong> ${sm.transitions.length + 1}</p>
14-
</div>
6+
<div>
7+
${renderMainHeader("", selectedTab)}
8+
${sm ? /*html*/`
9+
<div class="diagram-section">
10+
<div class="diagram-container">
11+
<pre class="mermaid">${diagram}</pre>
12+
</div>
13+
<div>
14+
<p><strong>States:</strong> ${sm.states.join(', ')}</p>
15+
<p><strong>Initial state:</strong> ${sm.initial}</p>
16+
<p><strong>Number of states:</strong> ${sm.states.length}</p>
17+
<p><strong>Number of transitions:</strong> ${sm.transitions.length + 1}</p>
18+
</div>
19+
</div>`
20+
: 'No state machine available for the current file'}
1521
</div>
1622
`;
1723
}

‎client/src/webview/views/sections.ts‎

Lines changed: 26 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,30 @@
11
import type { LJDiagnostic, TranslationTable } from "../../types/diagnostics";
22

3-
export const renderCustomSection = (title: string, body: string): string =>
3+
export const renderMainHeader = (title: string, selectedTab: NavTab): string => /*html*/`
4+
<div class="header">
5+
${renderNav(selectedTab)}
6+
<h2>${title}</h2>
7+
</div>
8+
`;
9+
10+
export const renderCustomSection = (title: string, body: string): string => /*html*/
411
`<div class="section"><strong>${title}:</strong><div>${body}</div></div>`;
512

6-
export const renderSection = (title: string, body: string): string =>
13+
export const renderSection = (title: string, body: string): string => /*html*/
714
renderCustomSection(title, `<pre>${body}</pre>`);
815

9-
export const renderHeader = (diagnostic: LJDiagnostic): string => {
10-
return `<h3>${diagnostic.title}</h3><div class="diagnostic-header"><p>${diagnostic.message}</p></div>`;
11-
};
16+
export const renderHeader = (diagnostic: LJDiagnostic): string => /*html*/
17+
`<h3>${diagnostic.title}</h3><div class="diagnostic-header"><p>${diagnostic.message}</p></div>`;
1218

1319
export const renderLocation = (diagnostic: LJDiagnostic): string => {
1420
if (!diagnostic.position) return "";
1521
const line = diagnostic.position?.lineStart ?? 0;
1622
const column = diagnostic.position?.colStart ?? 0;
1723
const simpleFile = diagnostic.file.split('/').pop() || diagnostic.file;
18-
const link = `<a href="#" class="link location-link" data-file="${diagnostic.file}" data-line="${line}" data-column="${column}">${simpleFile}:${line}</a>`;
19-
return renderCustomSection("Location", `<pre>${link}</pre>`);
24+
const link = /*html*/`<a href="#" class="link location-link" data-file="${diagnostic.file}" data-line="${line}" data-column="${column}">${simpleFile}:${line}</a>`;
25+
return renderCustomSection("Location", /*html*/`<pre>${link}</pre>`);
2026
};
2127

22-
export function renderShowAllButton(showAll: boolean): string {
23-
return /*html*/`
24-
<button class="show-all-button" title="Toggle filter diagnostics by current file">
25-
${showAll ? 'Show in File' : 'Show All'}
26-
</button>
27-
`;
28-
}
29-
3028
export function renderTranslationTable(translationTable: TranslationTable): string {
3129
const entries = Object.entries(translationTable).sort((a, b) => a[0].localeCompare(b[0])); // sort by variable name
3230
if (entries.length === 0) return '';
@@ -67,4 +65,17 @@ export function renderTranslationTable(translationTable: TranslationTable): stri
6765
</table>
6866
</div>
6967
`;
68+
}
69+
70+
export type NavTab = 'verification' | 'state-machine';
71+
72+
export function renderNav(selectedTab: NavTab): string {
73+
return /*html*/`
74+
<nav>
75+
<ul>
76+
<li><button class="nav-tab ${selectedTab === 'verification' ? 'selected' : ''}" data-tab="verification">Verification</button></li>
77+
<li><button class="nav-tab ${selectedTab === 'state-machine' ? 'selected' : ''}" data-tab="state-machine">State Machine</button></li>
78+
</ul>
79+
</nav>
80+
`;
7081
}

client/src/webview/views/derivation-nodes.ts renamed to client/src/webview/views/verification/derivation-nodes.ts

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
import type { LJError, RefinementError } from "../../types/diagnostics";
2-
import type { DerivationNode, ValDerivationNode } from "../../types/derivation-nodes";
1+
import type { LJError, RefinementError } from "../../../types/diagnostics";
2+
import type { DerivationNode, ValDerivationNode } from "../../../types/derivation-nodes";
33

44
// Handles rendering and interaction of derivation nodes in refinement errors
55

0 commit comments

Comments
 (0)