${content}
-
- ${renderHighlightedInlineExpression(renderAlias(alias))}
-
- |
- alias |
-
No aliases declared in the project
'} -No context information available at the cursor position
' - : `${renderContextAliases(aliases, sectionState.aliases)} - ${renderContextGhosts(ghosts, sectionState.ghosts)} - ${renderContextVariables(allVars, sectionState.vars, errorAtCursor)} - `} -${renderHighlightedInlineExpression(renderGhost(ghost))} |
- ${ghost.isState ? 'state' : 'ghost'} |
-
No ghosts or states declared in the current file
'} -| Name | -Refinement | -
|---|---|
| ${renderVariableHighlightButton(variable)} | -${renderHighlightedInlineExpression(variable.refinement)} |
-
No variables declared at the cursor position
'} -${infoMessage}
- ${ - diagnostics.length === 0 ? '' : /*html*/` - - ` - } -(+${hiddenErrors} error${hiddenErrors !== 1 ? 's' : ''})
- ` : ''} -${diagram}
- States: ${sm.states.join(', ')}
-Initial state${initialStateNames.length > 1 ? 's' : ''}: ${initialStateNames.join(', ')}
-Number of states: ${sm.states.length}
-Number of transitions: ${sm.transitions.length + sm.initialTransitions.length}
-Running the LiquidJava verification...
-${body}`);
-
-export const renderExpressionSection = (title: string, expression: string): string => /*html*/
- renderCustomSection(title, renderHighlightedExpression(expression));
-
-export const renderToggleSection = (title: string, targetId: string, isExpanded: boolean = true): string => /*html*/`
-
- `;
-
-export const renderDiagnosticHeader = (title: string, message: string): string => /*html*/
- `${message}
${renderLocationLink(diagnostic.position)}`);
-};
-
-export function renderVariableHighlightButton(variable: LJVariable): string {
- const displayName = getSimpleName(variable.name);
- const position = variable.position;
- if (!position || !position.file) return `${displayName}`;
- return /*html*/`
-
- `;
-}
-
-export function renderDiagnosticContextButton(position?: SourcePosition | null): string {
- if (!position?.file) return "";
- return renderCodiconButton("symbol-variable", {
- className: "diagnostic-context-btn",
- title: "View related context",
- attributes: `data-diagnostic-target="${getDiagnosticRevealTargetKey({ file: position.file, position })}"`,
- });
-}
-
-export function renderDiagnosticRevealButton(position: SourcePosition, content: string): string {
- if (!position.file) return `${content}`
- return /*html*/`
-
- `;
-}
-
-export function renderLocationLink(position?: SourcePosition): string {
- if (!position) return 'No location';
- return /*html*/`${escapeHtml(getFile(position))}`;
-}
-
-function getFile(position: SourcePosition): string {
- return `${position.file?.split('/').pop()?.trim() || position.file}:${position.lineStart + 1}`;
-}
-
-export type NavTab = 'diagnostics' | 'fsm' | 'context';
-
-export function renderNav(selectedTab: NavTab): string {
- return /*html*/`
-
- `;
-}
diff --git a/client/src/webview/views/stopped.ts b/client/src/webview/views/stopped.ts
deleted file mode 100644
index 7f228aa8..00000000
--- a/client/src/webview/views/stopped.ts
+++ /dev/null
@@ -1,23 +0,0 @@
-type StoppedViewStatus = "stopped" | "crashed";
-
-const stoppedViewContent: RecordLiquidJava: Start from the command palette.`,
- },
- crashed: {
- title: "LiquidJava Crashed",
- message: /*html*/`LiquidJava could not verify this project. LiquidJava: Show Logs from the command palette.`,
- },
-};
-
-export function renderStopped(status: StoppedViewStatus): string {
- const { title, message } = stoppedViewContent[status];
- return /*html*/`
- ${message}
-