[isabelle] jedit



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.

Thanks
Tobias





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