# HG changeset patch
# User wenzelm
# Date 1445686951 -7200
# Node ID 9334634404494bec07a21f9816aa9260cdd5e667
# Parent  d40f906bb13f35d3e4746c149f48ed96bc1d2c65
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;

diff -r d40f906bb13f -r 933463440449 NEWS
--- a/NEWS	Fri Oct 23 21:03:16 2015 +0200
+++ b/NEWS	Sat Oct 24 13:42:31 2015 +0200
@@ -57,6 +57,15 @@
 * Action "isabelle-reset" now uses keyboard shortcut C+e BACK_SPACE,
 instead of former C+e LEFT.
 
+* New command-line tool "isabelle jedit_client" allows to connect to
+already running Isabelle/jEdit process. This achieves the effect of
+single-instance applications seen on common GUI desktops.
+
+* The command-line tool "isabelle jedit" and the isabelle.Main
+application wrapper threat the default $USER_HOME/Scratch.thy more
+uniformly, and allow the dummy file argument ":" to open an empty buffer
+instead.
+
 
 *** Document preparation ***
 
@@ -514,10 +523,6 @@
 
   \<star>  code: 0x0022c6  group: operator  font: Deja␣Vu␣Sans␣Mono
 
-* Command-line tool "isabelle jedit_client" allows to connect to already
-running Isabelle/jEdit process. This achieves the effect of
-single-instance applications seen on common GUI desktops.
-
 * Command-line tool "isabelle update_then" expands old Isar command
 conflations:
 
diff -r d40f906bb13f -r 933463440449 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri Oct 23 21:03:16 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Oct 24 13:42:31 2015 +0200
@@ -236,8 +236,8 @@
     -n           no build of session image on startup
     -s           system build mode for session image
 
-  Start jEdit with Isabelle plugin setup and open theory FILES
-  (default "$USER_HOME/Scratch.thy").\<close>}
+  Start jEdit with Isabelle plugin setup and open FILES
+  (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}
 
   The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic
   image to be used for proof processing.  Additional session root
diff -r d40f906bb13f -r 933463440449 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Fri Oct 23 21:03:16 2015 +0200
+++ b/src/Pure/Tools/main.scala	Sat Oct 24 13:42:31 2015 +0200
@@ -51,9 +51,14 @@
           Array("-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")))
 
         val more_args =
-          if (args.isEmpty)
-            Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
-          else args
+        {
+          args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
+            case Nil | List("--") =>
+              args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
+            case List(":") => args.slice(0, args.size - 1)
+            case _ => args
+          }
+        }
 
 
         /* main startup */
diff -r d40f906bb13f -r 933463440449 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Oct 23 21:03:16 2015 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Oct 24 13:42:31 2015 +0200
@@ -107,7 +107,7 @@
   echo "    -s           system build mode for session image"
   echo
   echo "  Start jEdit with Isabelle plugin setup and open FILES"
-  echo "  (default \"$USER_HOME/Scratch.thy\")."
+  echo "  (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)."
   echo
   exit 1
 }
@@ -196,14 +196,10 @@
 
 # args
 
-if [ "$#" -eq 0 ]; then
-  ARGS["${#ARGS[@]}"]="$(platform_path "$USER_HOME/Scratch.thy")"
-else
-  while [ "$#" -gt 0 ]; do
-    ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
-    shift
-  done
-fi
+while [ "$#" -gt 0 ]; do
+  ARGS["${#ARGS[@]}"]="$(platform_path "$1")"
+  shift
+done
 
 
 ## dependencies