From 18b701fdce6c9810c92f03f4d8fcfaa86c2ebd7f Mon Sep 17 00:00:00 2001
From: Rob Simmons <robsimmons@gmail.com>
Date: Tue, 14 Nov 2023 20:01:42 -0500
Subject: [PATCH] Overhaul for some mobile friendliness and just-keep-running

---
 index.html      |   6 +-
 src/Config.tsx  |   4 +-
 src/Program.tsx | 204 ++++++++++++++++++-----------------------
 src/Tabs.tsx    |  20 ++--
 src/View.tsx    |  94 +++++++++++++++++++
 src/dusa.css    | 239 ++++++++++++++++++++++++++++++++++++------------
 src/main.tsx    |  10 +-
 src/sessions.ts | 127 +++++++++++++------------
 src/worker.ts   | 147 +++++++++++++++--------------
 9 files changed, 527 insertions(+), 324 deletions(-)
 create mode 100644 src/View.tsx

diff --git a/index.html b/index.html
index 252409c..0d3f48a 100644
--- a/index.html
+++ b/index.html
@@ -26,10 +26,10 @@
             <a href="https://github.com/robsimmons/dusa/blob/main/README.md">Dusa</a>
           </div>
         </div>
-        <div id="session" class="dk-session">
-          <div id="codemirror-root" class="dk-edit"></div>
+        <div id="session" class="mobile-view-editor">
+          <div id="codemirror-root"></div>
           <div id="session-divider"></div>
-          <div id="react-root" class="dk-view"></div>
+          <div id="react-root"></div>
         </div>
       </div>
     </main>
diff --git a/src/Config.tsx b/src/Config.tsx
index 56b13f0..8c40341 100644
--- a/src/Config.tsx
+++ b/src/Config.tsx
@@ -28,7 +28,7 @@ export default function Config(props: Props) {
       <div className="bottom-config">
         <Tooltip.Root>
           <Tooltip.Trigger asChild className="dk-trigger-button">
-            <button className="dk-icon-button" onClick={() => props.share()}>
+            <button onClick={() => props.share()}>
               <Share1Icon width={ICON_SIZE} height={ICON_SIZE} />
             </button>
           </Tooltip.Trigger>
@@ -38,7 +38,7 @@ export default function Config(props: Props) {
         </Tooltip.Root>
         <Tooltip.Root>
           <Tooltip.Trigger asChild className="dk-trigger-button">
-            <button id="themeswitcher" className="dk-icon-button" onClick={toggle}>
+            <button id="themeswitcher" onClick={toggle}>
               {mode === 'light' && <SunIcon width={ICON_SIZE} height={ICON_SIZE} />}
               {mode === 'dark' && <MoonIcon width={ICON_SIZE} height={ICON_SIZE} />}{' '}
             </button>
diff --git a/src/Program.tsx b/src/Program.tsx
index acb1870..41f154a 100644
--- a/src/Program.tsx
+++ b/src/Program.tsx
@@ -1,105 +1,106 @@
-import { EnterIcon, PauseIcon, ResumeIcon } from '@radix-ui/react-icons';
+import {
+  EnterIcon,
+  MagnifyingGlassIcon,
+  PauseIcon,
+  PlayIcon,
+  ReaderIcon,
+} from '@radix-ui/react-icons';
 import { Session } from './sessions';
 import { ICON_SIZE } from './constants';
+import View from './View';
 
 interface Props {
   session: Session;
   load: () => void;
   run: () => void;
   pause: () => void;
+  setSolution: (index: number | null) => void;
 }
 
-export default function Program({ load, run, pause, session }: Props) {
-  if (session.status === 'unconnected') {
-    return (
-      <>
-        <div className="dk-view-header">
+export default function Program({ load, run, pause, setSolution, session }: Props) {
+  const shouldReload =
+    session.status !== 'unconnected' && session.status !== 'load-error' && session.textModified;
+
+  return (
+    <>
+      <div id="explorer-header">
+        <button
+          id="explorer-load-program"
+          title="Load program"
+          className={shouldReload ? 'urgent' : ''}
+          onClick={(event) => {
+            event.preventDefault();
+            document.getElementById('session')!.className = 'mobile-view-explorer';
+            load();
+          }}
+        >
+          <EnterIcon width={ICON_SIZE} height={ICON_SIZE} />{' '}
+          {session.status === 'unconnected' || session.status === 'load-error'
+            ? 'load program'
+            : shouldReload
+            ? 'program changed! reload?'
+            : 'reload'}
+        </button>
+        <button
+          id="explorer-view-code"
+          title="View code"
+          onClick={(event) => {
+            event.preventDefault();
+            document.getElementById('session')!.className = 'mobile-view-editor';
+          }}
+        >
+          <ReaderIcon width={ICON_SIZE} height={ICON_SIZE} /> view program
+        </button>
+        {session.status !== 'unconnected' && session.status !== 'load-error' && (
           <button
-            title="Load program"
+            id="explorer-explore-solutions"
+            title="Explore solutions (without reloading)"
             onClick={(event) => {
               event.preventDefault();
-              load();
+              document.getElementById('session')!.className = 'mobile-view-explorer';
             }}
           >
-            <EnterIcon width={ICON_SIZE} height={ICON_SIZE} />
+            <MagnifyingGlassIcon width={ICON_SIZE} height={ICON_SIZE} /> explore
           </button>
-          <span className="dk-view-status">program not loaded</span>
-        </div>
-      </>
-    );
-  }
-
-  const loadButton = (
-    <button
-      title="Reset and reoad program"
-      onClick={(event) => {
-        event.preventDefault();
-        load();
-      }}
-    >
-      <EnterIcon width={ICON_SIZE} height={ICON_SIZE} />
-    </button>
-  );
-
-  const reloadBar = session.textModified ? (
-    <div className="dk-view-edit-warning">
-      The program has been modified!{' '}
-      <a
-        href=""
-        onClick={(event) => {
-          event.preventDefault();
-          load();
-        }}
-      >
-        Reload
-      </a>
-    </div>
-  ) : (
-    <div></div>
-  );
-
-  const solutionDescription =
-    session.status === 'error'
-      ? session.errorMessage
-      : session.status === 'done'
-      ? session.facts.length === 0
-        ? 'Done, no solutions.'
-        : session.facts.length === 1
-        ? 'Done, unique solution found.'
-        : `Done, ${session.facts.length} solutions found.`
-      : session.facts.length === 0
-      ? 'No solutions found (yet).'
-      : `${session.facts.length} solution${session.facts.length === 1 ? '' : 's'} found (so far).`;
-
-  const stats = (
-    <div className="dk-view-status">
-      {solutionDescription}
-      {session.stats && session.stats.cycles > 0 && (
-        <>
-          {' '}
-          {session.stats.cycles} step{session.stats.cycles !== 1 && 's'}
-          {session.stats && session.stats.deadEnds > 0 ? (
+        )}
+        {session.status === 'paused' && (
+          <button title="Search for more solutions" onClick={() => run()}>
+            <PlayIcon width={ICON_SIZE} height={ICON_SIZE} /> resume
+          </button>
+        )}
+        {session.status === 'running' && (
+          <button title="Pause searching for solutions" onClick={() => pause()}>
+            <PauseIcon width={ICON_SIZE} height={ICON_SIZE} /> pause
+          </button>
+        )}
+        <div id="explorer-status">
+          {session.status === 'unconnected' || session.status === 'load-error' ? null : (
             <>
-              , {session.stats.deadEnds} backtrack{session.stats.deadEnds !== 1 && 's.'}{' '}
+              <span className="basic-status">
+                {session.status === 'done' && session.stats.error
+                  ? 'done with errors'
+                  : session.status}
+              </span>
+              <span className="extended-status">
+                {session.stats.cycles > 0 && (
+                  <>
+                    , {session.stats.cycles} step{session.stats.cycles !== 1 && 's'}
+                  </>
+                )}
+                {session.stats.deadEnds > 0 && (
+                  <>
+                    , {session.stats.deadEnds} backtrack{session.stats.deadEnds !== 1 && 's'}
+                  </>
+                )}
+              </span>
             </>
-          ) : (
-            '.'
           )}
-        </>
-      )}
-    </div>
-  );
-
-  if (session.status === 'error') {
-    return (
-      <>
-        <div className="dk-view-header">
-          {loadButton}
-          {stats}
         </div>
-        {reloadBar}
-        <div className="dk-view-errors">
+      </div>
+      {session.status === 'load-error' && (
+        <div id="explorer-view" className="errors">
           <div className="dk-view-scroller">
+            {session.errorMessage}
             <ul>
               {' '}
               {session.issues.map((issue, i) => (
@@ -111,38 +112,15 @@ export default function Program({ load, run, pause, session }: Props) {
             </ul>
           </div>
         </div>
-      </>
-    );
-  }
-
-  return (
-    <>
-      <div className="dk-view-header">
-        {loadButton}
-        {session.status === 'paused' && (
-          <button title="Search for more solutions" onClick={() => run()}>
-            <ResumeIcon width={ICON_SIZE} height={ICON_SIZE} />
-          </button>
-        )}
-        {session.status === 'running' && (
-          <button title="Pause searching for solutions" onClick={() => pause()}>
-            <PauseIcon width={ICON_SIZE} height={ICON_SIZE} />
-          </button>
-        )}
-        {stats}
-      </div>
-      {reloadBar}
-      {session.facts.length > 0 && (
-        /* TODO: make dk-scroller end --dk-medium-padding above the bottom */
-        <div className="dk-view-solutions">
-          <div className="dk-view-scroller">
-            <div>Result #{session.facts.length}</div>
-            <ul>
-              {session.facts[session.facts.length - 1].sort().map((fact, i) => (
-                <li key={i}>{fact}</li>
-              ))}
-            </ul>
-          </div>
+      )}
+      {session.status !== 'load-error' && session.status !== 'unconnected' && (
+        <div id="explorer-view">
+          <View
+            status={session.status}
+            stats={session.stats}
+            query={session.query}
+            setSolution={setSolution}
+          />
         </div>
       )}
     </>
diff --git a/src/Tabs.tsx b/src/Tabs.tsx
index be87145..310cf1f 100644
--- a/src/Tabs.tsx
+++ b/src/Tabs.tsx
@@ -46,15 +46,17 @@ export default function Tabs({
           }
         </div>
       ))}
-      <button
-        className="dk-new-tab"
-        onClick={(event) => {
-          event.preventDefault();
-          addSession();
-        }}
-      >
-        <PlusIcon width={ICON_SIZE} height={ICON_SIZE} />
-      </button>
+      <div className="dk-tab">
+        <button
+          className="dk-new-tab"
+          onClick={(event) => {
+            event.preventDefault();
+            addSession();
+          }}
+        >
+          <PlusIcon width={ICON_SIZE} height={ICON_SIZE} />
+        </button>
+      </div>
     </>
   );
 }
diff --git a/src/View.tsx b/src/View.tsx
new file mode 100644
index 0000000..5182755
--- /dev/null
+++ b/src/View.tsx
@@ -0,0 +1,94 @@
+import {
+  ChevronLeftIcon,
+  ChevronRightIcon,
+  DoubleArrowLeftIcon,
+  DoubleArrowRightIcon,
+} from '@radix-ui/react-icons';
+import { WorkerQuery, WorkerStats } from './worker';
+import { ICON_SIZE } from './constants';
+
+interface Props {
+  status: 'done' | 'running' | 'paused';
+  stats: WorkerStats;
+  query: null | WorkerQuery;
+  setSolution: (index: number | null) => void;
+}
+
+export default function View(props: Props) {
+  const reportedSolutionNumber = (props.query?.solution ?? props.stats.solutions - 1) + 1;
+
+  return (
+    <>
+      <div id="explorer-view-header">
+        <div className="explorer-view-header">
+          <button
+            disabled={props.stats.solutions < 2 || reportedSolutionNumber === 1}
+            onClick={() => props.setSolution(0)}
+          >
+            <DoubleArrowLeftIcon width={ICON_SIZE} height={ICON_SIZE} />
+          </button>
+          <button
+            disabled={props.stats.solutions < 2 || reportedSolutionNumber === 1}
+            onClick={() => props.setSolution(reportedSolutionNumber - 2)}
+          >
+            <ChevronLeftIcon width={ICON_SIZE} height={ICON_SIZE} />
+          </button>
+          <div className="status">
+            {props.query === null && (
+              <>
+                {props.status === 'done' && 'no solutions'}
+                {props.status !== 'done' && 'no solutions yet'}
+              </>
+            )}
+            {props.query !== null && (
+              <>
+                {props.status === 'done' && (
+                  <>
+                    {props.stats.solutions === 1 && 'unique solution found'}
+                    {props.stats.solutions > 1 &&
+                      `solution ${reportedSolutionNumber} of ${props.stats.solutions}`}
+                  </>
+                )}
+                {props.status !== 'done' && (
+                  <>
+                    {props.query.solution === null && `solution ${reportedSolutionNumber} of ?`}
+                    {props.query.solution !== null &&
+                      `solution ${reportedSolutionNumber} of ${props.stats.solutions}+`}
+                  </>
+                )}
+              </>
+            )}
+          </div>
+          <button
+            disabled={
+              props.query?.solution == null || props.query.solution + 1 === props.stats.solutions
+            }
+            onClick={() => props.setSolution(reportedSolutionNumber)}
+          >
+            <ChevronRightIcon width={ICON_SIZE} height={ICON_SIZE} />
+          </button>
+          <button
+            disabled={
+              props.query?.solution == null ||
+              (props.status === 'done' && props.query.solution + 1 === props.stats.solutions)
+            }
+            onClick={() => props.setSolution(null)}
+          >
+            <DoubleArrowRightIcon width={ICON_SIZE} height={ICON_SIZE} />
+          </button>
+        </div>
+      </div>
+
+      <div id="explorer-view-data">
+        <div style={{ color: 'var(--oksolar-text-red)' }}>{props.stats.error}</div>
+        {props.query !== null && (
+          <ul>
+            {props.query.value.map((fact, i) => (
+              <li key={i}>{fact}</li>
+            ))}
+          </ul>
+        )}
+      </div>
+    </>
+  );
+}
diff --git a/src/dusa.css b/src/dusa.css
index b8a8e53..692d3a2 100644
--- a/src/dusa.css
+++ b/src/dusa.css
@@ -7,6 +7,7 @@ body {
   --dk-small-padding: 8px;
   --dk-small-radius: 8px;
   --dk-medium-padding: 12px;
+  --dk-large-padding: 16px;
 
   --text-editor-panel-width: 1fr;
 
@@ -30,9 +31,18 @@ body {
   --oksolar-text-violet: oklch(57% 0.15 280);
   --oksolar-text-pink: oklch(57% 0.15 330);
   --oksolar-text-red: oklch(57% 0.15 20);
+  --oksolar-text-red-highlight: oklch(57% 0.15 20);
   --oksolar-text-orange: oklch(57% 0.15 60);
 }
 
+@media (max-width: 650px) {
+  body {
+    --dk-outer-padding: 4px;
+    --dk-small-padding: 6px;
+    --dk-medium-padding: 10px;
+  }
+}
+
 body.theme-dark {
   --oksolar-background: oklch(27% 0 0);
   --oksolar-background-highlight: oklch(32% 0 0);
@@ -78,18 +88,21 @@ main {
 .dk-config div {
   display: flex;
   flex-direction: column;
-  gap: var(--dk-medium-padding);
+  gap: var(--dk-large-padding);
 }
 
-.dk-config .dk-icon-button {
+.dk-config button {
   height: 2rem;
   border: 0;
   background: var(--oksolar-background);
   color: var(--oksolar-text);
   border-radius: var(--dk-small-radius);
+  display: grid;
+  justify-content: center;
+  align-items: center;
 }
 
-.dk-config .dk-icon-button:hover {
+.dk-config button:hover {
   color: var(--oksolar-text-highlight);
   background-color: var(--oksolar-background-highlight);
 }
@@ -158,6 +171,7 @@ main {
 .dk-tab {
   display: flex;
   flex-direction: row;
+  min-width: fit-content;
 }
 
 /* Regular tab button styles */
@@ -210,16 +224,40 @@ main {
 
 #session {
   display: none; /* JS sets as 'grid' to avoid resize flash */
-  grid-template-columns: var(--text-editor-panel-width) 10px minmax(200px, 1fr);
+  grid-template-rows: 1fr;
+  grid-template-columns: var(--text-editor-panel-width) 10px minmax(250px, 1fr);
+  grid-template-areas: 'editor divider viewer';
+}
+
+@media (max-width: 650px) {
+  #session {
+    grid-template-columns: 1fr;
+    grid-template-areas: 'viewer' 'divider' 'editor';
+  }
+
+  #session.mobile-view-editor {
+    grid-template-rows: calc(2rem + var(--dk-small-padding)) 0 1fr;
+  }
+
+  #session.mobile-view-explorer {
+    grid-template-rows: 1fr 0 0;
+  }
 }
 
 #session-divider {
   cursor: ew-resize;
+  grid-area: divider;
+}
+
+@media (max-width: 650px) {
+  #session-divider {
+    display: none;
+  }
 }
 
 /** THE TEXT EDITOR **/
 
-.dk-edit {
+#codemirror-root {
   background-color: var(--oksolar-background);
   box-shadow: 0 0 0.3rem 0 var(--oksolar-text-deemph);
   border-radius: var(--dk-small-radius);
@@ -227,103 +265,188 @@ main {
   padding-left: var(--dk-small-padding);
   padding-right: 0;
   display: grid;
+  grid-area: editor;
 }
 
-#codemirror-root.dk-edit .cm-editor {
+div#codemirror-root .cm-editor {
   height: calc(
     100vh - 2 * var(--dk-outer-padding) - 2 * var(--dk-small-padding) - 2 * var(--dk-medium-padding) -
       3rem
   );
 }
 
-/** THE ENGINE VIEW **/
+@media (max-width: 650px) {
+  .mobile-view-explorer #codemirror-root {
+    display: none;
+  }
 
-.dk-view {
-  box-shadow: 0 0 0.3rem 0 var(--oksolar-text-deemph);
-  border-radius: var(--dk-small-radius);
+  div#codemirror-root .cm-editor {
+    height: calc(
+      100vh - 2 * var(--dk-outer-padding) - 2 * var(--dk-small-padding) - 2 *
+        var(--dk-medium-padding) - 3rem - 2rem - var(--dk-small-padding)
+    );
+  }
+}
+
+/** THE EXPLORER VIEW **/
+
+#react-root {
   display: grid;
-  grid-template-rows: calc(2rem + 1px) min-content 1fr;
+  grid-template-rows: calc(2rem) 1fr;
+  gap: var(--dk-small-padding);
   height: calc(100vh - 2 * var(--dk-outer-padding) - 2 * var(--dk-small-padding) - 3rem);
+  grid-area: viewer;
+}
+
+@media (max-width: 650px) {
+  .mobile-view-editor #react-root {
+    height: 2rem;
+  }
+
+  .mobile-view-editor #explorer-view {
+    display: none;
+  }
 }
 
-.dk-view-header {
+/** Explorer header (treated differently by mobile view) **/
+
+#explorer-header {
+  box-shadow: 0 0 0.3rem 0 var(--oksolar-text-deemph);
+  border-radius: var(--dk-small-radius);
   background-color: var(--oksolar-background);
-  display: grid;
-  border-top-right-radius: var(--dk-small-radius);
-  border-top-left-radius: var(--dk-small-radius);
-  justify-items: left;
-  border-bottom: solid 1px var(--oksolar-text-deemph-2);
   display: flex;
   flex-direction: row;
+  overflow-x: hidden;
 }
 
-.dk-view-header button {
-  width: 2rem;
+#explorer-header button {
   height: 2rem;
+  display: flex;
+  align-items: center;
+  gap: 4px;
+  background: transparent;
   border: none;
   border-radius: var(--dk-small-radius);
-  background-color: transparent;
   color: var(--oksolar-text);
-  display: grid;
-  align-items: center;
-  justify-content: center;
+  padding-right: var(--dk-small-padding);
+  white-space: nowrap;
+  min-width: fit-content;
+  flex-grow: 0;
 }
 
-.dk-view-header button:hover {
+#explorer-header button#explorer-view-code,
+#explorer-header button#explorer-explore-solutions {
+  display: none;
+}
+
+#explorer-header button.urgent {
+  color: var(--oksolar-text-red);
+}
+
+#explorer-header button.urgent:hover {
+  color: var(--oksolar-text-red-highlight);
+}
+
+#explorer-header #explorer-status {
+  margin-top: auto;
+  margin-bottom: auto;
+  text-align: right;
+  padding-inline: var(--dk-large-padding);
+  white-space: nowrap;
+  flex-grow: 1;
+}
+
+@media (max-width: 650px) {
+  .mobile-view-explorer #explorer-header button#explorer-load-program {
+    display: none;
+  }
+
+  .mobile-view-explorer #explorer-header button#explorer-view-code {
+    display: flex;
+  }
+
+  .mobile-view-editor #explorer-header button#explorer-explore-solutions {
+    display: flex;
+  }
+
+  #explorer-header #explorer-status .extended-status {
+    display: none;
+  }
+}
+
+#explorer-header button:hover {
   color: var(--oksolar-text-highlight);
   background-color: var(--oksolar-background-highlight);
 }
 
-.dk-view-status {
-  flex-grow: 1;
-  display: flex;
-  flex-direction: row;
-  align-items: center;
-  justify-content: right;
-  padding-right: var(--dk-medium-padding);
+/** Explorer view **/
+
+#explorer-view {
+  box-shadow: 0 0 0.3rem 0 var(--oksolar-text-deemph);
+  border-radius: var(--dk-small-radius);
 }
 
-.dk-view-errors {
+#explorer-view.errors {
   background-color: var(--oksolar-background-red);
-  border-bottom-left-radius: var(--dk-small-radius);
-  border-bottom-right-radius: var(--dk-small-radius);
+  border-radius: var(--dk-small-radius);
   padding: var(--dk-medium-padding);
   padding-top: var(--dk-small-padding);
   color: var(--oksolar-text-red);
   overflow-y: scroll;
 }
 
-.dk-view-edit-warning {
+#explorer-view-header {
+  background-color: var(--oksolar-background);
+  border-top-left-radius: var(--dk-small-radius);
+  border-top-right-radius: var(--dk-small-radius);
+  overflow-x: hidden;
+  height: 2rem;
+  max-width: 100%;
+}
+
+.explorer-view-header {
+  display: flex;
+  flex-direction: row;
+  height: 2rem;
+  min-width: 0;
   border-bottom: 1px solid var(--oksolar-text-deemph-2);
-  text-align: center;
-  color: var(--oksolar-text-red);
-  background-color: var(--oksolar-background-red);
 }
 
-.dk-view-edit-warning a {
-  text-decoration-color: var(--oksolar-text-emph);
-  text-decoration-line: underline;
-  text-decoration-style: solid;
-  color: var(--oksolar-text-emph);
+#explorer-view-header button {
+  min-width: 2rem;
+  background-color: transparent;
+  border: none;
+  border-radius: var(--dk-small-radius);
+  color: var(--oksolar-text);
 }
 
-.dk-view-solutions {
-  display: grid;
-  background-color: var(--oksolar-background);
-  border-bottom-left-radius: var(--dk-small-radius);
-  border-bottom-right-radius: var(--dk-small-radius);
-  padding: var(--dk-medium-padding);
-  padding-top: var(--dk-small-padding);
-  padding-bottom: var(--dk-medium-padding);
-  overflow-y: scroll;
+#explorer-view-header button:hover {
+  background-color: var(--oksolar-background-highlight);
+  color: var(--oksolar-text-highlight);
 }
 
-.dk-icon-button {
-  display: grid;
-  justify-content: center;
-  align-items: center;
+#explorer-view-header button:disabled {
+  color: var(--oksolar-text-deemph-2);
+}
+
+#explorer-view-header .status {
+  margin-block: auto;
+  width: fit-content;
+  min-width: 9rem;
+  text-align: center;
+  flex-shrink: 1;
+  overflow-x: hidden;
+  text-wrap: nowrap;
 }
 
-#sharebutton {
-  position: relative;
+#explorer-view-data {
+  padding-top: var(--dk-medium-padding);
+  overflow-y: scroll;
+  background-color: var(--oksolar-background);
+  height: calc(
+    100vh - 2 * var(--dk-outer-padding) - 2 * var(--dk-small-padding) - 2 * var(--dk-medium-padding) -
+      3rem - 2rem - var(--dk-small-padding) * 2
+  );
+  border-bottom-left-radius: var(--dk-small-radius);
+  border-bottom-right-radius: var(--dk-small-radius);
 }
diff --git a/src/main.tsx b/src/main.tsx
index 08d5617..8a25942 100644
--- a/src/main.tsx
+++ b/src/main.tsx
@@ -116,6 +116,11 @@ function renderView() {
             renderView();
           });
         }}
+        setSolution={(index) => {
+          sessionManager.setSolution(index).then(() => {
+            renderView();
+          });
+        }}
       />
     </React.StrictMode>,
   );
@@ -159,7 +164,7 @@ let referenceSessionDividerStatus: null | {
   initialTextWidth: number;
   initialEngineWidth: number;
 } = null;
-const MIN_PANE_PIXEL = 200;
+const MIN_PANE_PIXEL = 250;
 function sessionDividerMove(event: MouseEvent) {
   const { mouseDownX, initialTextWidth, initialEngineWidth } = referenceSessionDividerStatus!;
   const deltaX = event.clientX - mouseDownX;
@@ -179,9 +184,6 @@ function sessionDividerStop() {
   const { currentDeltaX, initialTextWidth, initialEngineWidth } = referenceSessionDividerStatus!;
   const newTextWidth = initialTextWidth + currentDeltaX;
   const newEngineWidth = initialEngineWidth - currentDeltaX;
-  console.log(newTextWidth);
-  console.log(newEngineWidth);
-  console.log(((1 + newTextWidth) / (newTextWidth + newEngineWidth)) * 2);
   setDividerProportion(newTextWidth / newEngineWidth);
   localStorage.setItem(LS_SESSION_DIVIDER_PROPORTION, `${newTextWidth / newEngineWidth}`);
 }
diff --git a/src/sessions.ts b/src/sessions.ts
index 4fa3536..a795034 100644
--- a/src/sessions.ts
+++ b/src/sessions.ts
@@ -8,7 +8,7 @@ import {
 } from './examples';
 import { Declaration, check } from './datalog/syntax';
 import { compile } from './datalog/compile';
-import { AppToWorker, WorkerStats, WorkerToApp } from './worker';
+import { AppToWorker, WorkerQuery, WorkerStats, WorkerToApp } from './worker';
 
 function decodeDusaHashURI(): null | { program: string } {
   if (!window.location.hash.startsWith('#')) return null;
@@ -39,30 +39,28 @@ type SessionData =
       worker: null;
     }
   | {
-      status: 'error';
+      status: 'load-error';
       text: string;
       textLoaded: string;
       worker: Worker;
-      facts?: string[][];
-      stats?: WorkerStats;
       issues: { msg: string; loc?: SourceLocation }[];
       errorMessage: string;
     }
   | {
-      status: 'paused';
+      status: 'paused' | 'running';
       text: string;
       textLoaded: string;
       worker: Worker;
-      facts: string[][];
-      stats: WorkerStats | null;
+      stats: WorkerStats;
+      query: null | WorkerQuery;
     }
   | {
-      status: 'running' | 'done';
+      status: 'done';
       text: string;
       textLoaded: string;
       worker: Worker;
-      facts: string[][];
       stats: WorkerStats;
+      query: null | WorkerQuery;
     };
 
 export type Session =
@@ -71,27 +69,25 @@ export type Session =
       text: string;
     }
   | {
-      status: 'error';
+      status: 'load-error';
       text: string;
       textModified: boolean;
-      facts?: string[][];
-      stats?: WorkerStats;
-      issues: { msg: string; loc?: SourceLocation }[];
       errorMessage: string;
+      issues: { msg: string; loc?: SourceLocation }[];
     }
   | {
-      status: 'paused';
+      status: 'paused' | 'running';
       text: string;
       textModified: boolean;
-      facts: string[][];
-      stats: WorkerStats | null;
+      stats: WorkerStats;
+      query: null | WorkerQuery;
     }
   | {
-      status: 'running' | 'done';
+      status: 'done';
       text: string;
       textModified: boolean;
-      facts: string[][];
       stats: WorkerStats;
+      query: null | WorkerQuery;
     };
 
 class SessionTabs {
@@ -306,24 +302,8 @@ class SessionTabs {
     }
 
     switch (msg.type) {
-      case 'error':
-        if (session.status !== 'running' && session.status !== 'paused') {
-          reportUnexpected();
-        } else {
-          this.sessionData[activeSession] = {
-            status: 'error',
-            text: session.text,
-            textLoaded: session.textLoaded,
-            worker: session.worker,
-            errorMessage: 'error during execution',
-            issues: [{ msg: msg.message }],
-            stats: msg.stats,
-          };
-        }
-        break;
-
       case 'done':
-        if (session.status !== 'running') {
+        if (session.status !== 'running' && session.status !== 'done') {
           reportUnexpected();
         } else {
           this.sessionData[activeSession] = {
@@ -331,14 +311,14 @@ class SessionTabs {
             text: session.text,
             textLoaded: session.textLoaded,
             worker: session.worker,
-            facts: session.facts,
             stats: msg.stats,
+            query: msg.query,
           };
         }
         break;
 
       case 'paused':
-        if (session.status !== 'running') {
+        if (session.status !== 'running' && session.status !== 'paused') {
           reportUnexpected();
         } else {
           this.sessionData[activeSession] = {
@@ -346,23 +326,8 @@ class SessionTabs {
             text: session.text,
             textLoaded: session.textLoaded,
             worker: session.worker,
-            facts: session.facts,
-            stats: msg.stats,
-          };
-        }
-        break;
-
-      case 'saturated':
-        if (session.status !== 'running') {
-          reportUnexpected();
-        } else {
-          this.sessionData[activeSession] = {
-            status: msg.last ? 'done' : 'paused',
-            text: session.text,
-            textLoaded: session.textLoaded,
-            worker: session.worker,
-            facts: [...session.facts, msg.facts],
             stats: msg.stats,
+            query: msg.query,
           };
         }
         break;
@@ -376,8 +341,8 @@ class SessionTabs {
             text: session.text,
             textLoaded: session.textLoaded,
             worker: session.worker,
-            facts: session.facts,
             stats: msg.stats,
+            query: msg.query,
           };
         }
     }
@@ -415,6 +380,27 @@ class SessionTabs {
     return this.lock;
   }
 
+  setSolution(index: null | number) {
+    this.lock = this.lock.then(() => {
+      const activeSession = this.activeSession;
+      const session = this.sessionData[activeSession];
+      if (
+        session.status === 'done' ||
+        session.status === 'running' ||
+        session.status === 'paused'
+      ) {
+        return this.messageWorker(session.worker, { type: 'setsolution', solution: index }).then(
+          (msg) => {
+            this.handleMessageResponse(activeSession, msg);
+          },
+        );
+      } else {
+        return Promise.resolve();
+      }
+    });
+    return this.lock;
+  }
+
   suspendProgram() {
     this.lock = this.lock.then(() => {
       const activeSession = this.activeSession;
@@ -454,12 +440,12 @@ class SessionTabs {
 
         if (issues.length > 0 || decls === null) {
           this.sessionData[activeSession] = {
-            status: 'error',
+            status: 'load-error',
             text,
             textLoaded: text,
             worker,
             issues,
-            errorMessage: `unable to load program: ${issues.length} error${
+            errorMessage: `Unable to load program: ${issues.length} error${
               issues.length === 1 ? '' : 's'
             }`,
           };
@@ -468,15 +454,26 @@ class SessionTabs {
 
         const program = compile(decls);
 
-        return this.messageWorker(worker, { type: 'load', program }).then(({ stats }) => {
-          this.sessionData[activeSession] = {
-            status: 'paused',
-            text,
-            textLoaded: text,
-            worker,
-            facts: [],
-            stats,
-          };
+        return this.messageWorker(worker, { type: 'load', program }).then((response) => {
+          if (response.type === 'done' || response.type === 'running') {
+            this.sessionData[activeSession] = {
+              status: response.type,
+              text,
+              textLoaded: text,
+              worker,
+              stats: response.stats,
+              query: response.query,
+            };
+          } else {
+            this.sessionData[activeSession] = {
+              status: 'load-error',
+              text,
+              textLoaded: text,
+              worker,
+              issues: [],
+              errorMessage: `unexpected response ${response.type} to load message`,
+            };
+          }
         });
       });
     return this.lock;
diff --git a/src/worker.ts b/src/worker.ts
index 786d09c..1ac7913 100644
--- a/src/worker.ts
+++ b/src/worker.ts
@@ -3,30 +3,36 @@ import {
   ChoiceTree,
   ChoiceTreeNode,
   CompiledProgram,
-  Fact,
+  Database,
   Program,
   factToString,
   makeInitialDb,
-  pathToString,
   stepTreeRandomDFS,
 } from './datalog/engine';
 
+export type WorkerQuery = {
+  type: 'list';
+  solution: number | null;
+  value: string[];
+};
+
 export interface WorkerStats {
   cycles: number;
   deadEnds: number;
+  solutions: number;
+  error: string | null;
 }
 
 export type WorkerToApp =
   | { stats: WorkerStats; type: 'hello' }
-  | { stats: WorkerStats; type: 'saturated'; facts: string[]; last: boolean }
-  | { stats: WorkerStats; type: 'paused' }
-  | { stats: WorkerStats; type: 'running' }
-  | { stats: WorkerStats; type: 'done' }
-  | { stats: WorkerStats; type: 'error'; message: string }
+  | { stats: WorkerStats; type: 'paused'; query: null | WorkerQuery }
+  | { stats: WorkerStats; type: 'running'; query: null | WorkerQuery }
+  | { stats: WorkerStats; type: 'done'; query: null | WorkerQuery }
   | { stats: WorkerStats; type: 'reset' };
 
 export type AppToWorker =
   | { type: 'status' }
+  | { type: 'setsolution'; solution: number | null }
   | { type: 'stop' }
   | { type: 'load'; program: CompiledProgram }
   | { type: 'start' }
@@ -35,105 +41,105 @@ export type AppToWorker =
 const CYCLE_LIMIT = 10000;
 const TIME_LIMIT = 500;
 let program: Program | null = null;
-let queuedFacts: Fact[] | null = null;
-let queuedError: string | null = null;
-
-let stats: WorkerStats = { cycles: 0, deadEnds: 0 };
+let solutions: Database[] = [];
+let setSolution: number | null = null;
+
+function newStats(): WorkerStats {
+  return {
+    cycles: 0,
+    deadEnds: 0,
+    solutions: 0,
+    error: null,
+  };
+}
+let stats: WorkerStats = newStats();
 
-function post(message: WorkerToApp) {
+function post(message: WorkerToApp): true {
   postMessage(message);
+  return true;
 }
 
 let tree: null | ChoiceTree = null;
 let path: [ChoiceTreeNode, Data | 'defer'][] = [];
 
-function cycle(): boolean {
+function cycle(): null | number {
   const limit = stats.cycles + CYCLE_LIMIT + Math.random() * CYCLE_LIMIT;
   const start = performance.now();
   try {
     while (stats.cycles < limit && start + TIME_LIMIT > performance.now()) {
-      if (tree === null) return false;
-      console.log(pathToString(tree, path));
+      if (tree === null) return null;
+      //(pathToString(tree, path));
       const result = stepTreeRandomDFS(program!, tree, path, stats);
       tree = result.tree;
       path = result.tree === null ? path : result.path;
 
       if (result.solution) {
-        queuedFacts = ([] as Fact[]).concat(
-          ...Object.entries(result.solution.facts).map(([name, argses]) =>
-            argses.map<Fact>(([args, value]) => ({
-              type: 'Fact',
-              name,
-              args,
-              value,
-            })),
-          ),
-        );
-        return false;
+        solutions.push(result.solution);
+        stats.solutions += 1;
+        return 0;
       }
     }
   } catch (e) {
-    queuedError = `${e}`;
-    return false;
+    stats.error = `${e}`;
+    return null;
   }
 
-  return true;
+  return 0;
 }
 
 let liveLoopHandle: null | ReturnType<typeof setTimeout> = null;
 function liveLoop() {
-  if (cycle()) {
-    liveLoopHandle = setTimeout(liveLoop);
+  let nextTimeout: null | number = null;
+  if ((nextTimeout = cycle()) !== null) {
+    liveLoopHandle = setTimeout(liveLoop, nextTimeout);
   } else {
     liveLoopHandle = null;
   }
 }
 
+function resolveQuery(index: number): WorkerQuery {
+  return {
+    type: 'list',
+    solution: setSolution,
+    value: ([] as string[])
+      .concat(
+        ...Object.entries(solutions[index].facts).map(([name, values]) =>
+          values.map(([args, value]) => factToString({ type: 'Fact', name, args, value })),
+        ),
+      )
+      .sort(),
+  };
+}
+
 // Picking up where you left off
-function resume(state: 'error' | 'paused' | 'done' | 'saturated' | 'running') {
-  switch (state) {
-    case 'error': {
-      return post({ type: 'error', message: queuedError!, stats });
-    }
+function resume(state: 'paused' | 'done' | 'running') {
+  const query =
+    solutions.length === 0
+      ? null
+      : setSolution === null
+      ? resolveQuery(solutions.length - 1)
+      : resolveQuery(setSolution);
 
+  switch (state) {
     case 'paused': {
-      return post({ type: 'paused', stats });
+      return post({ type: 'paused', stats, query });
     }
 
     case 'done': {
-      return post({ type: 'done', stats });
+      return post({ type: 'done', stats, query });
     }
 
     case 'running': {
       liveLoopHandle = setTimeout(liveLoop);
-      return post({ type: 'running', stats });
-    }
-
-    case 'saturated': {
-      const msg: WorkerToApp = {
-        type: 'saturated',
-        facts: queuedFacts!.map(factToString),
-        last: tree === null,
-        stats,
-      };
-      queuedFacts = null;
-      return post(msg);
+      return post({ type: 'running', stats, query });
     }
   }
 }
 
-onmessage = (event: MessageEvent<AppToWorker>) => {
+onmessage = (event: MessageEvent<AppToWorker>): true => {
   // What state are we actually in?
-  const state: 'error' | 'paused' | 'done' | 'saturated' | 'running' =
-    liveLoopHandle !== null
-      ? 'running'
-      : queuedError !== null
-      ? 'error'
-      : queuedFacts !== null
-      ? 'saturated'
-      : tree === null
-      ? 'done'
-      : 'paused';
+  const state: 'paused' | 'done' | 'running' =
+    liveLoopHandle !== null ? 'running' : tree === null || stats.error !== null ? 'done' : 'paused';
 
   // Pause
   if (liveLoopHandle !== null) {
@@ -143,17 +149,15 @@ onmessage = (event: MessageEvent<AppToWorker>) => {
 
   switch (event.data.type) {
     case 'load':
-      stats = { cycles: 0, deadEnds: 0 };
+      stats = newStats();
       path = [];
       program = event.data.program.program;
-      queuedFacts = null;
-      queuedError = null;
       try {
         tree = { type: 'leaf', db: makeInitialDb(event.data.program) };
-        return resume('paused');
+        return resume('running');
       } catch (e) {
-        queuedError = `${e}`;
-        return resume('error');
+        stats.error = `${e}`;
+        return resume('done');
       }
     case 'start':
       if (state === 'paused') {
@@ -166,15 +170,18 @@ onmessage = (event: MessageEvent<AppToWorker>) => {
       }
       return resume(state);
     case 'reset':
-      stats = { cycles: 0, deadEnds: 0 };
+      stats = newStats();
+      solutions = [];
+      setSolution = null;
       tree = null;
       path = [];
       program = null;
-      queuedFacts = null;
-      queuedError = null;
       return post({ type: 'reset', stats });
     case 'status':
       return resume(state);
+    case 'setsolution':
+      setSolution = event.data.solution;
+      return resume(state);
   }
 };