src/Pure/Admin/component_jedit.scala
changeset 82182 137559b26f74
parent 82180 1fad64843239
child 82411 49ca1a40c04a
--- a/src/Pure/Admin/component_jedit.scala	Sat Feb 15 14:37:41 2025 +0100
+++ b/src/Pure/Admin/component_jedit.scala	Sat Feb 15 15:06:38 2025 +0100
@@ -486,9 +486,6 @@
 classpath "$JEDIT_JAR"
 
 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
-JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9"
-JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m"
-JEDIT_JAVA_SYSTEM_OPTIONS="-Dsun.java2d.metal=false -Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
 
 ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/doc"
 """)