merged

--- a/Admin/MacOS/App1/README	Sun Sep 11 10:30:50 2011 -0700
+++ b/Admin/MacOS/App1/README	Sun Sep 11 21:35:35 2011 +0200
@@ -3,7 +3,7 @@
 
 Requirements:
 
-* CocoaDialog 2.2.1 http://cocoadialog.sourceforge.net/
+* CocoaDialog 2.1.1 http://cocoadialog.sourceforge.net/
 
 * Platypus 4.0 http://www.sveinbjorn.org/platypus
 

--- a/Admin/MacOS/App1/script	Sun Sep 11 10:30:50 2011 -0700
+++ b/Admin/MacOS/App1/script	Sun Sep 11 21:35:35 2011 +0200
@@ -71,11 +71,42 @@
 
 # run interface with error feedback
 
+ISABELLE_INTERFACE_CHOICE="$("$ISABELLE_TOOL" getenv -b ISABELLE_INTERFACE_CHOICE)"
+if [ "$ISABELLE_INTERFACE_CHOICE" != emacs -a "$ISABELLE_INTERFACE_CHOICE" != jedit ]
+then
+  declare -a CHOICE
+  CHOICE=($("$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" dropdown \
+    --title Isabelle \
+    --text "Which Isabelle interface?" \
+    --items "Emacs / Proof General" "Isabelle/jEdit PIDE" \
+    --button2 "OK, do not ask again" --button1 "OK"))
+  if [ "${CHOICE[1]}" = 0 ]; then
+    ISABELLE_INTERFACE_CHOICE=emacs
+  else
+    ISABELLE_INTERFACE_CHOICE=jedit
+  fi
+  if [ "${CHOICE[0]}" = 2 ]; then
+    ISABELLE_HOME_USER="$("$ISABELLE_TOOL" getenv -b ISABELLE_HOME_USER)"
+    mkdir -p "$ISABELLE_HOME_USER/etc"
+    ( echo; echo "ISABELLE_INTERFACE_CHOICE=$ISABELLE_INTERFACE_CHOICE"; ) \
+      >> "$ISABELLE_HOME_USER/etc/settings"
+    "$THIS/CocoaDialog.app/Contents/MacOS/CocoaDialog" ok-msgbox \
+      --title Isabelle \
+      --text Note \
+      --informative-text "ISABELLE_INTERFACE_CHOICE stored in $ISABELLE_HOME_USER/etc/settings" \
+      --no-cancel
+  fi
+fi
+
 OUTPUT="/tmp/isabelle$$.out"
 
-# ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
-( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
-RC=$?
+if [ "$ISABELLE_INTERFACE_CHOICE" = emacs ]; then
+  ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
+  RC=$?
+else
+  ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
+  RC=$?
+fi
 
 if [ "$RC" != 0 ]; then
   echo >> "$OUTPUT"

--- a/CONTRIBUTORS	Sun Sep 11 10:30:50 2011 -0700
+++ b/CONTRIBUTORS	Sun Sep 11 21:35:35 2011 +0200
@@ -12,6 +12,10 @@
 * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM
   Refined theory on complete lattices.
 
+* 2011: Makarius Wenzel, Université Paris-Sud / LRI
+  Various building blocks for Isabelle/Scala layer and Isabelle/jEdit
+  Prover IDE.
+
 
 Contributions to Isabelle2011
 -----------------------------