provide server name uniformly on all platforms;
authorwenzelm
Sat, 02 Jan 2016 15:18:38 +0100
changeset 62036 773cb226738c
parent 62035 b3cda398a5b1
child 62037 9bb80149dad9
provide server name uniformly on all platforms;
Admin/Linux/Isabelle.run
Admin/lib/Tools/makedist_bundle
src/Doc/JEdit/JEdit.thy
src/Pure/Tools/main.scala
src/Tools/jEdit/etc/settings
--- a/Admin/Linux/Isabelle.run	Sat Jan 02 13:29:34 2016 +0100
+++ b/Admin/Linux/Isabelle.run	Sat Jan 02 15:18:38 2016 +0100
@@ -40,5 +40,5 @@
     "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
     -classpath "{CLASSPATH}" \
     "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
-    isabelle.Main -server="$("$ISABELLE_HOME/bin/isabelle" jedit_client -n)" "$@"
+    isabelle.Main "$@"
 fi
--- a/Admin/lib/Tools/makedist_bundle	Sat Jan 02 13:29:34 2016 +0100
+++ b/Admin/lib/Tools/makedist_bundle	Sat Jan 02 15:18:38 2016 +0100
@@ -201,6 +201,7 @@
         do
           echo "$ARG"
         done
+        echo "-Disabelle.jedit_server=${ISABELLE_NAME}"
       ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.options${PLATFORM}"
     done
 
@@ -268,6 +269,7 @@
       do
         echo -e "$ARG\r"
       done
+      echo -e "-Disabelle.jedit_server=${ISABELLE_NAME}\r"
     ) > "$ISABELLE_TARGET/${ISABELLE_NAME}.l4j.ini"
 
     (
@@ -370,6 +372,7 @@
           do
             echo "<string>$OPT</string>"
           done
+          echo "<string>-Disabelle.jedit_server={ISABELLE_NAME}</string>"
           echo "<string>-Dapple.awt.application.name={ISABELLE_NAME}</string>"
 
           cat "$APP_TEMPLATE/Info.plist-part2"
--- a/src/Doc/JEdit/JEdit.thy	Sat Jan 02 13:29:34 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sat Jan 02 15:18:38 2016 +0100
@@ -287,10 +287,9 @@
   name (e.g.\ \<^verbatim>\<open>Isabelle2016\<close>). Thus @{tool jedit_client} can connect to the
   main Isabelle application without further options.
 
-  The regular jEdit command line option \<^verbatim>\<open>-server\<close> allows to provide a
-  different name, e.g.\ \<^verbatim>\<open>isabelle jedit -j-server=\<close>\<open>name\<close>. To connect to such
-  an alternative server process with @{tool jedit_client} requires a
-  corresponding option \<^verbatim>\<open>-s\<close>~\<open>name\<close>.
+  The JVM system property \<^verbatim>\<open>isabelle.jedit_server\<close> provides a different server
+  name, e.g.\ \<^verbatim>\<open>isabelle jedit -J-Disabelle.jedit_server=\<close>\<open>name\<close> and
+  \<^verbatim>\<open>isabelle jedit_client -s\<close>~\<open>name\<close> to connect later on.
 \<close>
 
 
--- a/src/Pure/Tools/main.scala	Sat Jan 02 13:29:34 2016 +0100
+++ b/src/Pure/Tools/main.scala	Sat Jan 02 15:18:38 2016 +0100
@@ -44,12 +44,18 @@
 
         /* args */
 
+        val jedit_settings =
+          "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
+
+        val jedit_server =
+          System.getProperty("isabelle.jedit_server") match {
+            case null | "" => "-noserver"
+            case name => "-server=" + name
+          }
+
         val jedit_options =
           Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
 
-        val jedit_settings =
-          Array("-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")))
-
         val more_args =
         {
           args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
@@ -72,7 +78,8 @@
           Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
         val jedit_main = jedit.getMethod("main", classOf[Array[String]])
 
-        () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
+        () => jedit_main.invoke(
+          null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
       }
       catch {
         case exn: Throwable =>
--- a/src/Tools/jEdit/etc/settings	Sat Jan 02 13:29:34 2016 +0100
+++ b/src/Tools/jEdit/etc/settings	Sat Jan 02 15:18:38 2016 +0100
@@ -3,7 +3,7 @@
 JEDIT_HOME="$COMPONENT"
 JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
 
-JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
+JEDIT_OPTIONS="-reuseview -nobackground -log=9"
 
 JEDIT_JAVA_OPTIONS32="-Xms128m -Xmx1024m -Xss4m -XX:MetaspaceSize=128m"
 JEDIT_JAVA_OPTIONS64="-Xms512m -Xmx2560m -Xss8m -XX:MetaspaceSize=256m"