1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
package main
import "html/template"
// The whole frontend: one page, one EventSource, no build step. State arrives as
// JSON over SSE and is written into the DOM; the SVG is already laid out by
// graphviz, so there is nothing to render client-side.
var indexTemplate = template.Must(template.New("index").Parse(indexHTML))
const indexHTML = `<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>{{.Name}} — alloy-viz</title>
<style>
:root {
--bg:#f5f5f7; --card:#fff; --fg:#1b1b1f; --fg2:#5f6368;
--accent:#2f6fb0; --border:#dcdce0; --bad:#c62828; --good:#2e7d32;
}
@media (prefers-color-scheme: dark) {
:root {
--bg:#161618; --card:#212124; --fg:#e8e8ea; --fg2:#a0a0a6;
--accent:#5aa3dd; --border:#3a3a40; --bad:#e57373; --good:#7bc47f;
}
}
*,*::before,*::after { box-sizing:border-box; }
body { font-family:system-ui,sans-serif; background:var(--bg); color:var(--fg);
margin:0; line-height:1.4; }
header { position:sticky; top:0; z-index:10; background:var(--card);
border-bottom:1px solid var(--border); padding:.6rem 1rem;
display:flex; align-items:center; gap:.75rem; flex-wrap:wrap; }
h1 { font-size:1rem; margin:0; font-weight:600; }
h1 .dir { color:var(--fg2); font-weight:400; }
select, button { font:inherit; padding:.3rem .6rem; border-radius:6px;
border:1px solid var(--border); background:var(--card); color:var(--fg); }
button { cursor:pointer; }
button:hover:not(:disabled) { border-color:var(--accent); color:var(--accent); }
button:disabled { opacity:.45; cursor:default; }
.status { margin-left:auto; display:flex; align-items:center; gap:.6rem;
font-size:.85rem; color:var(--fg2); }
.dot { width:.55rem; height:.55rem; border-radius:50%; background:var(--fg2); flex:none; }
.dot.running { background:var(--accent); animation:pulse 1s ease-in-out infinite; }
.dot.done { background:var(--good); }
.dot.error { background:var(--bad); }
@keyframes pulse { 0%,100%{opacity:1} 50%{opacity:.25} }
main { padding:1rem; }
.graph { background:var(--card); border:1px solid var(--border); border-radius:8px;
padding:1rem; overflow:auto; text-align:center; min-height:60vh; }
.graph svg { max-width:100%; height:auto; }
.empty { color:var(--fg2); padding:3rem 1rem; }
.err { background:var(--card); border:1px solid var(--bad); border-left-width:4px;
border-radius:6px; padding:.75rem 1rem; margin-bottom:1rem; }
.err h2 { margin:0 0 .25rem; font-size:.85rem; color:var(--bad);
text-transform:uppercase; letter-spacing:.03em; }
.err pre { margin:0; white-space:pre-wrap; font-size:.85rem; }
.err .pos { font-family:ui-monospace,monospace; font-size:.8rem; color:var(--fg2); }
details { margin-top:1rem; }
summary { cursor:pointer; color:var(--fg2); font-size:.85rem; }
details pre { background:var(--card); border:1px solid var(--border); border-radius:6px;
padding:.75rem; overflow:auto; max-height:60vh; font-size:.75rem; }
</style>
</head>
<body>
<header>
<h1><span class="dir">{{.Path}}</span></h1>
<select id="cmd" title="command to run"></select>
<button id="rerun">Run</button>
<button id="cancel" disabled>Cancel</button>
<div class="status"><span class="dot" id="dot"></span><span id="status">connecting…</span></div>
</header>
<main>
<div id="error" hidden class="err">
<h2>Error</h2>
<div class="pos" id="errpos"></div>
<pre id="errmsg"></pre>
</div>
<div class="graph" id="graph"><div class="empty">waiting for first solve…</div></div>
<details id="xmlbox" hidden>
<summary>instance XML</summary>
<pre id="xml"></pre>
</details>
</main>
<script>
(function () {
var cmd = document.getElementById('cmd'),
graph = document.getElementById('graph'),
status = document.getElementById('status'),
dot = document.getElementById('dot'),
cancel = document.getElementById('cancel'),
rerun = document.getElementById('rerun'),
errBox = document.getElementById('error'),
errMsg = document.getElementById('errmsg'),
errPos = document.getElementById('errpos'),
xmlBox = document.getElementById('xmlbox'),
xmlPre = document.getElementById('xml');
// Only rebuild the <select> when the command list actually changes, so the
// dropdown does not close under the user mid-interaction.
var lastCommands = '';
function apply(s) {
var sig = JSON.stringify(s.commands || []);
if (sig !== lastCommands) {
lastCommands = sig;
cmd.innerHTML = '';
(s.commands || []).forEach(function (c) {
var o = document.createElement('option');
o.value = c.index;
o.textContent = c.kind + ' ' + c.label + (c.scope ? ' ' + c.scope : '');
cmd.appendChild(o);
});
}
if (s.selected !== undefined && cmd.options.length) cmd.value = s.selected;
var text = s.status || s.state || '';
if (s.running && s.elapsed_ms > 1000) {
text += ' (' + (s.elapsed_ms / 1000).toFixed(1) + 's)';
}
status.textContent = text;
dot.className = 'dot' + (s.running ? ' running' : (s.state === 'done' ? ' done'
: (s.state === 'error' ? ' error' : '')));
cancel.disabled = !s.running;
rerun.disabled = !!s.running;
if (s.error) {
errBox.hidden = false;
errMsg.textContent = s.error;
errPos.textContent = s.error_pos || '';
} else {
errBox.hidden = true;
}
if (s.svg) graph.innerHTML = s.svg;
else if (s.state === 'done') graph.innerHTML = '<div class="empty">' + text + '</div>';
if (s.xml) { xmlBox.hidden = false; xmlPre.textContent = s.xml; }
}
var es = new EventSource('/events');
es.onmessage = function (e) { apply(JSON.parse(e.data)); };
es.onerror = function () {
status.textContent = 'disconnected';
dot.className = 'dot error';
};
function post(url, body) {
return fetch(url, {
method: 'POST',
headers: {'Content-Type': 'application/x-www-form-urlencoded'},
body: body || ''
});
}
cmd.addEventListener('change', function () { post('/run', 'index=' + cmd.value); });
rerun.addEventListener('click', function () { post('/run', 'index=' + cmd.value); });
cancel.addEventListener('click', function () { post('/cancel'); });
// Tick the elapsed time locally: the server only pushes on real state
// changes, and a multi-minute solve would otherwise look frozen.
setInterval(function () {
if (cancel.disabled) return;
var m = /\(([\d.]+)s\)$/.exec(status.textContent);
if (m) {
status.textContent = status.textContent.replace(
/\([\d.]+s\)$/, '(' + (parseFloat(m[1]) + 0.5).toFixed(1) + 's)');
}
}, 500);
})();
</script>
</body>
</html>
`
|