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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and