src/Tools/jEdit/dist-template/lib/Tools/jedit
changeset 34880 f88fc4fcab86
parent 34843 eb8806a2e348
child 34881 d5b901fc63e7
--- 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[@]}"