From 2a070332f26473d8bb00290c39e56a41ff3c6ae5 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 11 Jun 2024 20:39:42 +0200
Subject: [PATCH] side-by-side goals #90

---
 client/src/components/infoview/goals.tsx | 20 ++++++++++++----
 client/src/css/infoview.css              | 29 ++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 5 deletions(-)

diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx
index d101cbe..1325bf4 100644
--- a/client/src/components/infoview/goals.tsx
+++ b/client/src/components/infoview/goals.tsx
@@ -153,8 +153,8 @@ export const Goal = React.memo((props: GoalProps) => {
             { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
             undefined,
         [locs, goal.mvarId])
-    const goalLi = <div key={'goal'}>
-        <div className="goal-title">{t("Goal")}:</div>
+    const goalLi = <div key={'goal'} className="goal">
+        {/* <div className="goal-title">{t("Goal")}:</div> */}
         <LocationsContext.Provider value={goalLocs}>
             <InteractiveCode fmt={goal.type} />
         </LocationsContext.Provider>
@@ -168,18 +168,28 @@ export const Goal = React.memo((props: GoalProps) => {
     const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
     const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
 
-    return <div>
+    return <>
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
         {filter.reverse && goalLi}
+        <div className="hypotheses">
         {! typewriter && objectHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">{t("Objects")}:</div>
             {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
         {!typewriter && assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">{t("Assumptions")}:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        {!filter.reverse && goalLi}
+        </div>
+        {!filter.reverse && <>
+            <div className='goal-sign'>
+                <svg width="100%" height="100%">
+                    <line x1="0%" y1="0%" x2="0%" y2="100%" />
+                    <line x1="0%" y1="50%" x2="100%" y2="50%" />
+                </svg>
+            </div>
+            {goalLi}
+        </>}
         {/* {showHints && hints} */}
-    </div>
+    </>
 })
 
 export const MainAssumptions = React.memo((props: GoalProps2) => {
diff --git a/client/src/css/infoview.css b/client/src/css/infoview.css
index 1d3428b..37b1801 100644
--- a/client/src/css/infoview.css
+++ b/client/src/css/infoview.css
@@ -189,3 +189,32 @@
 .tooltip-arrow {
   display: none;
 }
+
+
+.goal-tab {
+  /* border: 2px dotted darkgreen; */
+  display: flex;
+  flex-direction: row;
+}
+
+.goal-tab .goal, .goal-tab .hypotheses {
+  /* border: 1px solid lightblue; */
+  display: inline-block;
+  flex: 1;
+  display: flex;
+  flex-direction: column;
+  justify-content: center;
+}
+
+.goal-sign {
+  /* border: 1px solid lightblue; */
+  width: 1rem;
+  margin-left: .5rem;
+  margin-right: .5rem;
+  display: inline-block;
+}
+
+.goal-sign line {
+  stroke: var(--clr-dark-gray);
+  stroke-width: 2;
+}