equal
deleted
inserted
replaced
98 shift |
98 shift |
99 done |
99 done |
100 fi |
100 fi |
101 |
101 |
102 |
102 |
|
103 ## default perspective |
|
104 |
|
105 mkdir -p "$JEDIT_SETTINGS/DockableWindowManager" |
|
106 |
|
107 if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then |
|
108 cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF |
|
109 <DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="172" BOTTOM_POS="183" /> |
|
110 EOF |
|
111 cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF |
|
112 <?xml version="1.0" encoding="UTF-8" ?> |
|
113 <!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> |
|
114 <PERSPECTIVE> |
|
115 <VIEW PLAIN="FALSE"> |
|
116 <GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" /> |
|
117 </VIEW> |
|
118 </PERSPECTIVE> |
|
119 EOF |
|
120 fi |
|
121 |
|
122 |
103 ## main |
123 ## main |
104 |
124 |
105 case "$JEDIT_LOGIC" in |
125 case "$JEDIT_LOGIC" in |
106 /*) |
126 /*) |
107 ;; |
127 ;; |
112 |
132 |
113 export JEDIT_LOGIC JEDIT_PRINT_MODE |
133 export JEDIT_LOGIC JEDIT_PRINT_MODE |
114 |
134 |
115 exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \ |
135 exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \ |
116 -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \ |
136 -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \ |
117 "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${ARGS[@]}" |
137 "-settings=$(jvmpath "$JEDIT_SETTINGS")" "${ARGS[@]}" |