# HG changeset patch
# User wenzelm
# Date 1451750207 -3600
# Node ID a77f4a9037d4dc25ee8c9ecedee82bbf67f22437
# Parent  5651de00bca9504758adb8d3441948868638b974
clarified isabelle jedit command-line;

diff -r 5651de00bca9 -r a77f4a9037d4 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Jan 02 16:32:36 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sat Jan 02 16:56:47 2016 +0100
@@ -226,6 +226,7 @@
 \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
 
   Options are:
+    -D NAME=X    set JVM system property
     -J OPTION    add JVM runtime option
     -b           build only
     -d DIR       include session directory
@@ -260,6 +261,9 @@
   work for the command-line tool described here, and not the regular
   application.
 
+  The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
+  directly to the underlying \<^verbatim>\<open>java\<close> process.
+
   The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
   Isabelle/jEdit. This is only relevant for building from sources, which also
   requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from @{url
@@ -288,7 +292,7 @@
   main Isabelle application without further options.
 
   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
+  name, e.g.\ \<^verbatim>\<open>isabelle jedit -Disabelle.jedit_server=\<close>\<open>name\<close> and
   \<^verbatim>\<open>isabelle jedit_client -s\<close>~\<open>name\<close> to connect later on.
 \<close>
 
diff -r 5651de00bca9 -r a77f4a9037d4 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Sat Jan 02 16:32:36 2016 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Jan 02 16:56:47 2016 +0100
@@ -95,6 +95,7 @@
   echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]"
   echo
   echo "  Options are:"
+  echo "    -D NAME=X    set JVM system property"
   echo "    -J OPTION    add JVM runtime option (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)"
   echo "    -b           build only"
   echo "    -d DIR       include session directory"
@@ -138,9 +139,12 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "J:bd:fj:l:m:ns" OPT
+  while getopts "D:J:bd:fj:l:m:ns" OPT
   do
     case "$OPT" in
+      D)
+        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG"
+        ;;
       J)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
         ;;