# HG changeset patch # User wenzelm # Date 1288270574 -7200 # Node ID 0b57e3d9bc62b248a1b22b4fa0724127b8bbdd0e # Parent e11da4ec9d7451ae6dc6a3f3b061e2940428975d dock isabelle-session at bottom (again, cf. 37bdc2220cf8) to ensure that controls are fully visible; diff -r e11da4ec9d74 -r 0b57e3d9bc62 src/Tools/jEdit/dist-template/lib/Tools/jedit --- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Tue Oct 26 16:56:07 2010 +0200 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Thu Oct 28 14:56:14 2010 +0200 @@ -106,7 +106,7 @@ if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" < + EOF cat > "$JEDIT_SETTINGS/perspective.xml" < diff -r e11da4ec9d74 -r 0b57e3d9bc62 src/Tools/jEdit/dist-template/properties/jedit.props --- a/src/Tools/jEdit/dist-template/properties/jedit.props Tue Oct 26 16:56:07 2010 +0200 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Thu Oct 28 14:56:14 2010 +0200 @@ -178,9 +178,9 @@ insert-newline-indent.shortcut= insert-newline.shortcut=ENTER isabelle-output.dock-position=bottom +isabelle-session.dock-position=bottom isabelle-output.height=174 isabelle-output.width=412 -isabelle-session.dock-position=right line-end.shortcut=END line-home.shortcut=HOME lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel