# HG changeset patch # User wenzelm # Date 1263311511 -3600 # Node ID f88fc4fcab86c893bcbcca1f98625ab52467e11f # Parent 032e14798e16196ec39433b30128b2bdc424426f provide JEDIT_SETTINGS via settings; provide default perspective; tuned default properties; diff -r 032e14798e16 -r f88fc4fcab86 src/Tools/jEdit/dist-template/etc/settings --- 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" diff -r 032e14798e16 -r f88fc4fcab86 src/Tools/jEdit/dist-template/lib/Tools/jedit --- 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 + cat > "$JEDIT_SETTINGS/perspective.xml" < + + + + + + +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[@]}" diff -r 032e14798e16 -r f88fc4fcab86 src/Tools/jEdit/dist-template/properties/jedit.props --- 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