vscode goal window

Stream: general

[Johan Commelin]

Is it possible to have a goal window that shows only the tactic state, and no messages etc...

I'm giving a talk later today, and I think that for a complete newbie there's quite a lot of disctraction in the goal window.
(Of course all that feedback is super useful to us power users, but I would like to have an extremely clean goal window for the talk.)

[Gabriel Ebner]

You can click on the triangles to collapse all parts of the infoview.

[Johan Commelin]

Yes, but if I move my cursor back and forth they auto-open again.

[Johan Commelin]

goal_window.gif

[Johan Commelin]

It would be really great if there was a way to only display the contents of Tactic state and just hide all the other bells and whistles (pin/reload buttons, widget/plain text option, messages).

[Gabriel Ebner]

I've just pushed a change that remembers the collapsed-state of the error messages. Properly adding support for a "distraction-free" infoview takes a bit more time. Making a custom build where the unwanted elements are just deleted is more feasible.

[Johan Commelin]

Great! Thank you so much!
If such a custom build is not too much trouble, that would be wonderful.

[Patrick Massot]

@Gabriel Ebner are you doing it or do you expect that Johan will do it?

[Patrick Massot]

I don't mind doing it but I need to know soon because I should be elsewhere already

[Gabriel Ebner]

If you could do it that would be awesome.

[Patrick Massot]

@Johan Commelin could you try installing lean-0.17.0.vsix?

[Patrick Massot]

You need to go to the extension panel and click on the menu in the upper right corner and choose Install from VSIX

[Johan Commelin]

Yes, let me try.

[Johan Commelin]

Works like a charm!

[Johan Commelin]

@Patrick Massot awesome, thank you so much!

[Patrick Massot]

For the record, here the diff with the official extension:

--- a/infoview/index.css
+++ b/infoview/index.css
@@ -90,4 +90,17 @@ select {
     background-color: var(--vscode-dropdown-background);
     color: var(--vscode-dropdown-foreground);
     border-color: var(--vscode-dropdown-border);
-}
\ No newline at end of file
+}
+
+/* Johan's hacks */
+div.mv2 {
+    display: none;
+}
+
+div.mv1 select {
+    display: none;
+}
+
+div.fr label, select {
+    display: none;
+}

[Patrick Massot]

I only used the VSCode web dev tools to inspect the infoview HTML+CSS and brutally switched off display in CSS.

[Patrick Massot]

Now I really need to run

[Kevin Buzzard]

Thank you Patrick! I will keep a copy of this one myself: I am speaking on Friday to a generalist (non-mathematician) audience about numbers and this version might be better for me too.

[Kevin Buzzard]

I'm assuming I can switch backwards and forwards between the two versions relatively easily? I quite like being able to see error messages :-)

[Patrick Massot]

How was your talk Johan?

[Johan Commelin]

I think it went really well. People liked the Lean demo, and I'm sure the uncluttered goal window contributed to that.

[Johan Commelin]

After the talk several people hang around and had some more questions. I've pointed several of them to NNG and/or zulip.

[Patrick Massot]

What did you show in the Lean demo (apart from the uncluttered goal window)?