From 7a78aa7bf0aeffc41c9ecf020e8ed59500a49e1b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Tue, 28 May 2024 14:22:44 +0200
Subject: [PATCH] [code] Don't show goals type when details are closed.

This is a workaround for #525 #652

For now, I disable this setting, so types are not displayed.

The right fix would be to add a checkbox in the view, so this can be
toggled dynamically, but I don't have the cycles for that right now,
and not worth delaying the release which is long overdue.
---
 editor/code/views/info/Goals.tsx | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/editor/code/views/info/Goals.tsx b/editor/code/views/info/Goals.tsx
index 531b77da..4cfc33b9 100644
--- a/editor/code/views/info/Goals.tsx
+++ b/editor/code/views/info/Goals.tsx
@@ -61,16 +61,24 @@ function Goal({ goal, idx, open }: GoalP) {
     }
   });
 
+  // XXX: We want to add an option for this that can be set interactively
+  let show_goal_on_header = false;
+
+  let gtyp = (
+    <div style={{ marginLeft: "1ex" }} className={className} ref={tyRef}>
+      <CoqPp content={goal.ty} inline={false} />
+    </div>
+  );
+
   return (
     <div className="coq-goal-env" ref={ref}>
       <Details summary={`Goal (${idx})`} open={open}>
         <div style={{ paddingTop: "1ex" }} />
         <Hyps hyps={goal.hyps} />
         <hr />
+        {show_goal_on_header ? "" : gtyp}
       </Details>
-      <div style={{ marginLeft: "1ex" }} className={className} ref={tyRef}>
-        <CoqPp content={goal.ty} inline={false} />
-      </div>
+      {show_goal_on_header ? gtyp : ""}
     </div>
   );
 }