# HG changeset patch
# User wenzelm
# Date 1285699779 -7200
# Node ID c7f0fa0593f0796f2d6a094df5389ef1045fa29b
# Parent  909ee37c34c1faaf71fe83cbf8b6291d9ad7ef2d
tuned default perspective;

diff -r 909ee37c34c1 -r c7f0fa0593f0 src/Tools/jEdit/dist-template/lib/Tools/jedit
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Tue Sep 28 20:35:17 2010 +0200
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Tue Sep 28 20:49:39 2010 +0200
@@ -106,7 +106,7 @@
 
 if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
   cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
-    <DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
+<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-session" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
 EOF
   cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
 <?xml version="1.0" encoding="UTF-8" ?>
diff -r 909ee37c34c1 -r c7f0fa0593f0 src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Sep 28 20:35:17 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Sep 28 20:49:39 2010 +0200
@@ -7,12 +7,9 @@
 buffer.noTabs=true
 buffer.sidekick.keystroke-parse=true
 buffer.tabSize=2
-console.dock-position=bottom
 console.encoding=UTF-8
 console.font=IsabelleText
 console.fontsize=14
-console.height=174
-console.width=412
 delete-line.shortcut=A+d
 delete.shortcut2=C+d
 encoding.opt-out.Big5-HKSCS=true
@@ -181,8 +178,9 @@
 insert-newline-indent.shortcut=
 insert-newline.shortcut=ENTER
 isabelle-output.dock-position=bottom
-isabelle-raw-output.dock-position=bottom
 isabelle-session.dock-position=bottom
+isabelle-session.height=174
+isabelle-session.width=412
 line-end.shortcut=END
 line-home.shortcut=HOME
 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel