[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

@@ -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>
   );
 }