provide JEDIT_SETTINGS via settings;
authorwenzelm
Tue, 12 Jan 2010 16:51:51 +0100
changeset 34881f88fc4fcab86
parent 34880 032e14798e16
child 34882 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
     1.1 --- a/src/Tools/jEdit/dist-template/etc/settings	Tue Jan 12 14:57:29 2010 +0100
     1.2 +++ b/src/Tools/jEdit/dist-template/etc/settings	Tue Jan 12 16:51:51 2010 +0100
     1.3 @@ -1,4 +1,5 @@
     1.4  JEDIT_HOME="$COMPONENT"
     1.5 +JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
     1.6  
     1.7  JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m"
     1.8  #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m"
     2.1 --- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Tue Jan 12 14:57:29 2010 +0100
     2.2 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Tue Jan 12 16:51:51 2010 +0100
     2.3 @@ -100,6 +100,26 @@
     2.4  fi
     2.5  
     2.6  
     2.7 +## default perspective
     2.8 +
     2.9 +mkdir -p "$JEDIT_SETTINGS/DockableWindowManager"
    2.10 +
    2.11 +if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
    2.12 +  cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
    2.13 +    <DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="172" BOTTOM_POS="183" />
    2.14 +EOF
    2.15 +  cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
    2.16 +<?xml version="1.0" encoding="UTF-8" ?>
    2.17 +<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
    2.18 +<PERSPECTIVE>
    2.19 +<VIEW PLAIN="FALSE">
    2.20 +<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
    2.21 +</VIEW>
    2.22 +</PERSPECTIVE>
    2.23 +EOF
    2.24 +fi
    2.25 +
    2.26 +
    2.27  ## main
    2.28  
    2.29  case "$JEDIT_LOGIC" in
    2.30 @@ -114,4 +134,4 @@
    2.31  
    2.32  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
    2.33    -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
    2.34 -  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${ARGS[@]}"
    2.35 +  "-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}"
     3.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Jan 12 14:57:29 2010 +0100
     3.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Jan 12 16:51:51 2010 +0100
     3.3 @@ -7,6 +7,12 @@
     3.4  buffer.noTabs=true
     3.5  buffer.sidekick.keystroke-parse=true
     3.6  buffer.tabSize=2
     3.7 +console.dock-position=bottom
     3.8 +console.encoding=UTF-8
     3.9 +console.font=IsabelleText
    3.10 +console.fontsize=14
    3.11 +console.height=174
    3.12 +console.width=412
    3.13  delete-line.shortcut=A+d
    3.14  delete.shortcut2=C+d
    3.15  encoding.opt-out.Big5-HKSCS=true
    3.16 @@ -170,6 +176,9 @@
    3.17  encodingDetectors=BOM XML-PI buffer-local-property
    3.18  fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
    3.19  firstTime=false
    3.20 +isabelle-output.dock-position=bottom
    3.21 +isabelle-output.height=296
    3.22 +isabelle-output.width=512
    3.23  isabelle-protocol.dock-position=bottom
    3.24  isabelle-results.dock-position=bottom
    3.25  isabelle.activate.shortcut=CS+ENTER
    3.26 @@ -177,6 +186,7 @@
    3.27  sidekick-tree.dock-position=right
    3.28  sidekick.buffer-save-parse=true
    3.29  sidekick.complete-delay=300
    3.30 +sidekick.splitter.location=721
    3.31  tip.show=false
    3.32  view.antiAlias=standard
    3.33  view.blockCaret=true
    3.34 @@ -187,5 +197,7 @@
    3.35  view.fontsize=18
    3.36  view.fracFontMetrics=false
    3.37  view.gutter.fontsize=12
    3.38 +view.height=787
    3.39  view.middleMousePaste=true
    3.40  view.showToolbar=false
    3.41 +view.width=1072