Re: [isabelle] jedit



On Tue, 15 May 2012, Tobias Nipkow wrote:

For demos with a video projector, every line counts. How can I get rid of as much of the grey area around the file buffer and the output window? I mean especially the panels between the two windows and the one below the output window. (Thanks to Dimitriy I have already been able to remove the grey area to the left of the file buffer). The two windows should remain horizontal.

The Output panel is managed by the "dockable window manager" of jEdit, and follows its own rules. For example, you can probably get 1-2 more lines by removing all dockables from the bottom line, and retaining a floating version of Output (there can be more than one). You can then make the two windows slightly overlapping, to hide some of their decoration.

Moreover, it is possible to scale the font size of the Output panel down, say to 85% of the main text font.


In the course that we have had on Mon/Tue, we had the opposite sitation. The projector had a resolution of 1920x1080, and the window decorations and menus were rather tiny. The TextArea font size only applies to the main text buffer and the output panel.

The equipment in the LRI building is from last year, and all the rooms have rather high-resolution displays or projectors by default. The time of classic 1024x768 seems to be over.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.