provide JEDIT_SETTINGS via settings;
authorwenzelm
Tue, 12 Jan 2010 16:51:51 +0100
changeset 34880 f88fc4fcab86
parent 34879 032e14798e16
child 34881 d5b901fc63e7
provide JEDIT_SETTINGS via settings; provide default perspective; tuned default properties;
src/Tools/jEdit/dist-template/etc/settings
src/Tools/jEdit/dist-template/lib/Tools/jedit
src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/etc/settings	Tue Jan 12 14:57:29 2010 +0100
+++ b/src/Tools/jEdit/dist-template/etc/settings	Tue Jan 12 16:51:51 2010 +0100
@@ -1,4 +1,5 @@
 JEDIT_HOME="$COMPONENT"
+JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
 
 JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m"
 #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m"
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Tue Jan 12 14:57:29 2010 +0100
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Tue Jan 12 16:51:51 2010 +0100
@@ -100,6 +100,26 @@
 fi
 
 
+## default perspective
+
+mkdir -p "$JEDIT_SETTINGS/DockableWindowManager"
+
+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="172" BOTTOM_POS="183" />
+EOF
+  cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
+<?xml version="1.0" encoding="UTF-8" ?>
+<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
+<PERSPECTIVE>
+<VIEW PLAIN="FALSE">
+<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
+</VIEW>
+</PERSPECTIVE>
+EOF
+fi
+
+
 ## main
 
 case "$JEDIT_LOGIC" in
@@ -114,4 +134,4 @@
 
 exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
   -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
-  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${ARGS[@]}"
+  "-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}"
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Jan 12 14:57:29 2010 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Jan 12 16:51:51 2010 +0100
@@ -7,6 +7,12 @@
 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
@@ -170,6 +176,9 @@
 encodingDetectors=BOM XML-PI buffer-local-property
 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
 firstTime=false
+isabelle-output.dock-position=bottom
+isabelle-output.height=296
+isabelle-output.width=512
 isabelle-protocol.dock-position=bottom
 isabelle-results.dock-position=bottom
 isabelle.activate.shortcut=CS+ENTER
@@ -177,6 +186,7 @@
 sidekick-tree.dock-position=right
 sidekick.buffer-save-parse=true
 sidekick.complete-delay=300
+sidekick.splitter.location=721
 tip.show=false
 view.antiAlias=standard
 view.blockCaret=true
@@ -187,5 +197,7 @@
 view.fontsize=18
 view.fracFontMetrics=false
 view.gutter.fontsize=12
+view.height=787
 view.middleMousePaste=true
 view.showToolbar=false
+view.width=1072