Skip to content

Commit ab18fa6

Browse files
jackeownjackeown
committed
latest
1 parent b528d36 commit ab18fa6

File tree

2 files changed

+156
-52
lines changed

2 files changed

+156
-52
lines changed

‎docusaurus-site/src/components/VampireRunner.jsx‎

Lines changed: 144 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,13 @@ async function findWorkingBaseUrl(){
3030
const baseTag = typeof document!=='undefined' ? document.querySelector('base')?.getAttribute('href') : null;
3131
if (baseTag) candidates.push(baseTag);
3232

33+
// Prefer the known site root before falling back to the current page path (e.g. /docs/)
34+
candidates.push('/vampireGuide/');
35+
3336
if (typeof location !== 'undefined') {
3437
candidates.push(new URL('./', location.href).pathname);
3538
}
3639

37-
candidates.push('/vampireGuide/');
3840
candidates.push('/');
3941

4042
const seen = new Set();
@@ -100,20 +102,48 @@ fof(b, conjecture, p).`,
100102
const [out, setOut] = useState('Ready.');
101103
const [pendingPrompt, setPendingPrompt] = useState(null);
102104
const [pendingInput, setPendingInput] = useState('');
105+
const [pendingInline, setPendingInline] = useState(false);
106+
const [pendingSpacer, setPendingSpacer] = useState('');
107+
const [pendingMatchText, setPendingMatchText] = useState('');
103108
const pendingResolveRef = useRef(null);
104109
const [running, setRunning] = useState(false);
110+
const outWrapRef = useRef(null);
105111
const outCodeRef = useRef(null);
106112
const latestOutRef = useRef('Ready.');
113+
const cancelRunRef = useRef(null);
114+
const runIdRef = useRef(0);
115+
116+
useEffect(() => {
117+
latestOutRef.current = out;
118+
}, [out]);
107119

108120
// Re-highlight output whenever it changes (or when Prism arrives)
109121
useEffect(() => {
110122
if (typeof window === 'undefined') return;
111123
highlightNowOrWhenReady(outCodeRef.current);
112-
}, [out, outputLanguage]);
124+
}, [out, outputLanguage, pendingPrompt, pendingInput, pendingInline]);
113125

114126
useEffect(() => {
115-
latestOutRef.current = out;
116-
}, [out]);
127+
if (!outWrapRef.current) return;
128+
outWrapRef.current.scrollTop = outWrapRef.current.scrollHeight;
129+
}, [out, pendingPrompt, pendingInput, pendingInline]);
130+
131+
useEffect(() => {
132+
if (!pendingPrompt) return;
133+
outWrapRef.current?.focus({ preventScroll: true });
134+
}, [pendingPrompt]);
135+
136+
const visibleOut = (() => {
137+
if (!pendingPrompt) return out;
138+
const lastLineRaw = out.split('\n').slice(-1)[0] || '';
139+
const lastLine = lastLineRaw.replace(/\s+$/, '');
140+
const forceInline = pendingMatchText && lastLine.endsWith(pendingMatchText);
141+
if (pendingInline || forceInline) {
142+
return out + pendingSpacer + pendingInput;
143+
}
144+
const sep = out ? '\n' : '';
145+
return out + sep + (pendingPrompt || '> ') + pendingInput;
146+
})();
117147

118148
// Append a line to the transcript (one big string for highlighting)
119149
const appendLine = (text) => {
@@ -124,10 +154,27 @@ fof(b, conjecture, p).`,
124154
});
125155
};
126156

157+
const appendInline = (text) => {
158+
setOut(prev => {
159+
const next = (prev || '') + text;
160+
latestOutRef.current = next;
161+
return next;
162+
});
163+
};
164+
127165
const handleRequestInput = (promptText) => {
128-
const promptLine = promptText || '>';
129-
appendLine(promptLine);
166+
const raw = String(promptText ?? '');
167+
const trimmed = raw.replace(/\s+$/, '');
168+
const lastLineRaw = (latestOutRef.current || '').split('\n').slice(-1)[0] || '';
169+
const lastLine = lastLineRaw.replace(/\r/g, '').trim();
170+
const normalizedPrompt = trimmed.replace(/\r/g, '').trim();
171+
const inline = Boolean(normalizedPrompt) && lastLine.endsWith(normalizedPrompt);
172+
const spacer = inline && !/\s$/.test(lastLineRaw) ? ' ' : '';
173+
const promptLine = inline ? '' : (normalizedPrompt ? (normalizedPrompt + ' ') : '> ');
130174
setPendingPrompt(promptLine);
175+
setPendingInline(inline);
176+
setPendingSpacer(spacer);
177+
setPendingMatchText(normalizedPrompt);
131178
setPendingInput('');
132179
return new Promise((resolve) => {
133180
pendingResolveRef.current = resolve;
@@ -137,27 +184,61 @@ fof(b, conjecture, p).`,
137184
const submitPromptResponse = () => {
138185
if (!pendingResolveRef.current) return;
139186
const answer = pendingInput;
140-
appendLine(`> ${answer}`);
187+
const lastLineRaw = (latestOutRef.current || '').split('\n').slice(-1)[0] || '';
188+
const lastLine = lastLineRaw.replace(/\s+$/, '');
189+
const forceInline = pendingMatchText && lastLine.endsWith(pendingMatchText);
190+
if (pendingInline || forceInline) {
191+
appendInline(`${pendingSpacer}${answer}`);
192+
} else {
193+
appendLine(`${pendingPrompt ?? '> '}${answer}`);
194+
}
141195
pendingResolveRef.current(answer);
142196
pendingResolveRef.current = null;
143197
setPendingPrompt(null);
144198
setPendingInput('');
199+
setPendingInline(false);
200+
setPendingSpacer('');
201+
setPendingMatchText('');
145202
};
146203

147204
const handleKeyDown = (ev) => {
205+
if (!pendingPrompt) return;
148206
if (ev.key === 'Enter') {
149207
ev.preventDefault();
150208
submitPromptResponse();
209+
return;
210+
}
211+
if (ev.key === 'Backspace') {
212+
ev.preventDefault();
213+
setPendingInput(prev => prev.slice(0, -1));
214+
return;
215+
}
216+
if (ev.key.length === 1 && !ev.ctrlKey && !ev.metaKey && !ev.altKey) {
217+
ev.preventDefault();
218+
setPendingInput(prev => prev + ev.key);
151219
}
152220
};
153221

222+
const handlePaste = (ev) => {
223+
if (!pendingPrompt) return;
224+
const text = ev.clipboardData?.getData('text');
225+
if (!text) return;
226+
ev.preventDefault();
227+
setPendingInput(prev => prev + text.replace(/\r/g, ''));
228+
};
229+
154230
async function onRun() {
231+
const newRunId = runIdRef.current + 1;
232+
runIdRef.current = newRunId;
233+
if (cancelRunRef.current) {
234+
cancelRunRef.current();
235+
cancelRunRef.current = null;
236+
}
155237
setRunning(true);
156238
setOut('Running…');
157239
setPendingPrompt(null);
158240
setPendingInput('');
159241
if (pendingResolveRef.current) {
160-
pendingResolveRef.current('');
161242
pendingResolveRef.current = null;
162243
}
163244
try {
@@ -173,12 +254,33 @@ fof(b, conjecture, p).`,
173254
const { code } = await runRaw({
174255
tptp,
175256
args,
176-
onStdout: (msg) => String(msg ?? '').split('\n').forEach(appendLine),
177-
onStderr: (msg) => String(msg ?? '').split('\n').forEach(line => appendLine(`[err] ${line}`)),
178-
requestInput: handleRequestInput,
257+
onStdout: (msg) => {
258+
if (runIdRef.current !== newRunId) return;
259+
String(msg ?? '').split('\n').forEach(appendLine);
260+
},
261+
onStderr: (msg) => {
262+
if (runIdRef.current !== newRunId) return;
263+
String(msg ?? '').split('\n').forEach(line => appendLine(`[err] ${line}`));
264+
},
265+
requestInput: (promptText) => {
266+
if (runIdRef.current !== newRunId) return new Promise(() => {});
267+
return handleRequestInput(promptText);
268+
},
269+
onReady: (instance) => {
270+
if (runIdRef.current !== newRunId) {
271+
return;
272+
}
273+
cancelRunRef.current = () => {
274+
if (pendingResolveRef.current) {
275+
pendingResolveRef.current = null;
276+
}
277+
};
278+
},
179279
});
180-
const exitCode = typeof code === 'number' ? code : 0;
181-
appendLine(`(exit ${exitCode})`);
280+
if (runIdRef.current === newRunId) {
281+
const exitCode = typeof code === 'number' ? code : 0;
282+
appendLine(`(exit ${exitCode})`);
283+
}
182284

183285
// Best-effort clipboard copy to speed up sharing logs
184286
if (navigator?.clipboard?.writeText) {
@@ -189,13 +291,15 @@ fof(b, conjecture, p).`,
189291
} catch (e) {
190292
setOut(`Error: ${e?.message || e}`);
191293
} finally {
192-
if (pendingResolveRef.current) {
193-
pendingResolveRef.current('');
194-
pendingResolveRef.current = null;
294+
if (runIdRef.current === newRunId) {
295+
if (pendingResolveRef.current) {
296+
pendingResolveRef.current = null;
297+
}
298+
setPendingPrompt(null);
299+
setPendingInput('');
300+
setRunning(false);
301+
cancelRunRef.current = null;
195302
}
196-
setPendingPrompt(null);
197-
setPendingInput('');
198-
setRunning(false);
199303
}
200304
}
201305

@@ -228,34 +332,29 @@ fof(b, conjecture, p).`,
228332
)}
229333
</div>
230334

231-
<p><button className="vr-run" onClick={onRun} disabled={running}>Run Vampire</button></p>
232-
233-
{pendingPrompt && (
234-
<div style={{ marginBottom: '0.75rem' }}>
235-
<label>Input required (prompt: {pendingPrompt})</label>
236-
<input
237-
type="text"
238-
value={pendingInput}
239-
onChange={e => setPendingInput(e.target.value)}
240-
onKeyDown={handleKeyDown}
241-
style={{ width: '100%', padding: '0.4rem', fontFamily: 'monospace' }}
242-
autoFocus
243-
/>
244-
<button className="vr-run" onClick={submitPromptResponse} style={{ marginTop: '0.35rem' }}>
245-
Send
246-
</button>
247-
</div>
248-
)}
335+
<p><button className="vr-run" onClick={onRun}>Run Vampire</button></p>
249336

250337
<label>Output</label>
251-
<pre style={{ maxHeight: outputMaxHeight, overflow: 'auto', marginTop: 0 }}>
252-
<code
253-
ref={outCodeRef}
254-
className={`language-${outputLanguage}`}
255-
>
256-
{out}
257-
</code>
258-
</pre>
338+
<div
339+
ref={outWrapRef}
340+
tabIndex={0}
341+
onKeyDown={handleKeyDown}
342+
onPaste={handlePaste}
343+
onClick={() => outWrapRef.current?.focus()}
344+
style={{
345+
padding: '0.5rem',
346+
background: 'var(--prism-background-color, transparent)'
347+
}}
348+
>
349+
<pre style={{ margin: 0, maxHeight: outputMaxHeight, overflow: 'auto' }}>
350+
<code
351+
ref={outCodeRef}
352+
className={`language-${outputLanguage}`}
353+
>
354+
{visibleOut}
355+
</code>
356+
</pre>
357+
</div>
259358
</div>
260359
);
261360
}

‎docusaurus-site/static/vampire-runner/script.js‎

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,7 @@ export function shellQuote(argv) {
6060
}
6161

6262
// ---------- Runner APIs ----------
63-
export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInput }) {
63+
export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInput, onReady }) {
6464
const base = getBaseUrl();
6565

6666
const glueUrl = base + 'vampire-runner/vampire.js';
@@ -81,8 +81,11 @@ export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInp
8181
});
8282
};
8383

84+
const isInteractive = typeof requestInput === 'function';
8485
const Module = {
8586
noInitialRun: true,
87+
// Keep the runtime alive during interactive runs; allow exit otherwise
88+
noExitRuntime: isInteractive,
8689
locateFile: (path) => base + 'vampire-runner/' + path,
8790
print: (s) => {
8891
const msg = String(s);
@@ -108,6 +111,9 @@ export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInp
108111

109112
try {
110113
const mod = await createVampire(Module);
114+
if (typeof onReady === 'function') {
115+
onReady(mod);
116+
}
111117

112118
try { mod.FS.mkdir('/work'); } catch {}
113119
mod.FS.writeFile('/work/input.p', new TextEncoder().encode(String(tptp ?? '')));
@@ -117,13 +123,12 @@ export async function runVampireRaw({ tptp, args, onStdout, onStderr, requestInp
117123
argv.push('/work/input.p');
118124
}
119125

120-
const runner = mod.Asyncify?.handleAsync
121-
? mod.Asyncify.handleAsync(() => mod.callMain(argv))
122-
: mod.callMain(argv);
123-
126+
const ret = mod.callMain(argv);
124127
try {
125-
const ret = await runner;
126-
finish(typeof ret === 'number' ? ret : 0);
128+
const awaited = ret && typeof ret.then === 'function' ? await ret : ret;
129+
if (!isInteractive) {
130+
finish(typeof awaited === 'number' ? awaited : 0);
131+
}
127132
} catch (e) {
128133
if (e && e.name === 'ExitStatus' && typeof e.status === 'number') {
129134
finish(e.status);

0 commit comments

Comments
 (0)