Stream: Beginner Questions

Topic: Reset jedit window settings?

Naso (Jun 07 2023 at 03:48):

Hello, how can I reset the jedit window settings on Mac? Thank you

Naso (Jun 24 2023 at 12:03):

Can no one help me? I accidentally closed the "Output" tab and cannot get it to come back.

Mathias Fleury (Jun 24 2023 at 12:30):

Plugins > Isabelle >  Output panel

Mathias Fleury (Jun 24 2023 at 12:31):

I don't remember if you have to dock to the bottom afterwards.

Naso (Jun 24 2023 at 13:34):

Mathias Fleury said:

I don't remember if you have to dock to the bottom afterwards.

Thank you Mathias :) This restored the output panel but now it is floating. Do you know how I can dock it?

Mathias Fleury (Jun 24 2023 at 13:35):

somewhere right-click > dock at

Mathias Fleury (Jun 24 2023 at 13:36):

the small triangle arrow, top left

Naso (Jun 24 2023 at 13:38):

right-clicking anywhere in the floating output window doesn't appear to do anything

Naso (Jun 24 2023 at 13:38):

(on macOS)

Naso (Jun 24 2023 at 13:39):

ohh...
image.png

Naso (Jun 24 2023 at 13:40):

there is an extremely tiny black triangle in the top left, above a grey background

Naso (Jun 24 2023 at 13:40):

and clicking on it works!

Naso (Jun 24 2023 at 13:40):

thank you :)

Last updated: Dec 21 2024 at 16:20 UTC