equal
deleted
inserted
replaced
1 # -*- shell-script -*- :mode=shellscript: |
|
2 |
|
3 JEDIT_HOME="$COMPONENT" |
|
4 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit" |
|
5 |
|
6 JEDIT_OPTIONS="-reuseview -noserver -nobackground" |
|
7 JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false" |
|
8 #JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false" |
|
9 JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit" |
|
10 |
|
11 JEDIT_STYLE_SHEETS="$ISABELLE_HOME/lib/html/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css" |
|
12 |
|
13 ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets" |
|
14 |
|
15 ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools" |
|
16 |
|