more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
--- 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:
--- 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
--- 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 */
--- 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