Support for jEdit server provided by Makarius

lib/isabelle/Tools/why3

@@ -16,10 +16,16 @@ function usage()
   echo "    -b           batch mode"
   echo "    -i NAME      interactive mode using interface NAME"
   echo
-  echo "  Process files generated by Why3"
+  echo "Process files generated by Why3."
   exit 1
 }
 
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
 
 ## utilities
 
@@ -61,22 +67,31 @@ done
 
 shift $(($OPTIND - 1))
 
-if [ "$1" = "" ]; then
-  usage
-else
-  NAME=`dirname "$1"`/`basename "$1" .xml`
-fi
+[ "$#" != 1 ] && usage
+
+NAME=`dirname "$1"`/`basename "$1" .xml`
 
 if [ "$BATCH" = true ]; then
-  $ISABELLE_PROCESS -e "use_thy \"$NAME\";" -rq Why3
+  "$ISABELLE_PROCESS" -e "use_thy \"$NAME\";" -rq Why3
 elif [ "$INTERACTIVE" = true ]; then
-  if [ "$INTERFACE" = emacs ]; then
-    LOGIC="-L"
-  else
-    LOGIC="-l"
-  fi
   make_theory "$NAME"
-  $ISABELLE_TOOL $INTERFACE $LOGIC Why3 "$NAME.thy"
+  case "$INTERFACE" in
+    emacs)
+      "$ISABELLE_TOOL" emacs -L Why3 "${NAME}.thy"
+      ;;
+    jedit)
+      if [ -f "$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER" ]; then
+        "$ISABELLE_TOOL" java -jar "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" \
+          "-settings=$(jvmpath "$JEDIT_SETTINGS")" "-server=$WHY3_JEDIT_SERVER" \
+          -reuseview -wait "$(jvmpath "${NAME}.thy")"
+      else
+        "$ISABELLE_TOOL" jedit -l Why3 "${NAME}.thy"
+      fi
+      ;;
+    *)
+      fail "Unknown Isabelle interface: \"$INTERFACE\""
+      ;;
+  esac
 else
   usage
 fi

lib/isabelle/Tools/why3_jedit

+#!/usr/bin/env bash
+#
+# DESCRIPTION: Isabelle/jEdit with Why3 session and server port
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+  echo
+  echo "Usage: isabelle $PRG [ARGS...]"
+  echo
+  echo "Start Isabelle/jEdit with Why3 session and server port, for quick invocation"
+  echo "via why3ide."
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## main
+
+[ "$1" = "-?" ] && usage
+
+SERVER_FILE="$JEDIT_SETTINGS/$WHY3_JEDIT_SERVER"
+
+if [ -f "$SERVER_FILE" ]; then
+  fail "Server already running: \"$SERVER_FILE\""
+else
+  exec "$ISABELLE_TOOL" jedit "-j-server=$WHY3_JEDIT_SERVER" -l Why3 "$@"
+fi

lib/isabelle/etc/settings

-ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/Tools"
+# -*- shell-script -*- :mode=shellscript:
+
+WHY3_ISABELLE_HOME="$COMPONENT"
+WHY3_JEDIT_SERVER="server-Why3"
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$WHY3_ISABELLE_HOME/Tools"

share/provers-detection-data.conf

@@ -448,7 +448,7 @@ version_ok = "2013-2"
 command = "%l/why3-cpulimit 0 0 -s %e why3 -b %f"
 driver = "drivers/isabelle.drv"
 in_place = true
-editor = "jedit-isabelle"
+editor = "isabelle-jedit"
 
 [editor pvs]
 name = "PVS"
@@ -462,7 +462,7 @@ command = "coqide -I %l/coq-tactic -R %l/coq Why3 %f"
 name = "Emacs/ProofGeneral/Coq"
 command = "emacs23 --eval \"(setq coq-load-path '(\\\"%l/coq-tactic\\\" (\\\"%l/coq\\\" \\\"Why3\\\")))\" %f"
 
-[editor jedit-isabelle]
+[editor isabelle-jedit]
 name = "Isabelle/jEdit"
 command = "isabelle why3 -i jedit %f"