# HG changeset patch
# User wenzelm
# Date 1260570558 -3600
# Node ID d0ff1c3a91ea3809065fa700302d67744f3935e0
# Parent  d1040b77b189f31d27078c9abed79882a83ff629
more serious command line handling;

diff -r d1040b77b189 -r d0ff1c3a91ea src/Tools/jEdit/dist-template/etc/settings
--- a/src/Tools/jEdit/dist-template/etc/settings	Fri Dec 11 22:40:55 2009 +0100
+++ b/src/Tools/jEdit/dist-template/etc/settings	Fri Dec 11 23:29:18 2009 +0100
@@ -4,4 +4,6 @@
 #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m"
 JEDIT_OPTIONS="-reuseview -noserver -nobackground"
 
+ISABELLE_JEDIT_OPTIONS="-m xsymbols -m no_brackets -m no_type_brackets"
+
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"
diff -r d1040b77b189 -r d0ff1c3a91ea src/Tools/jEdit/dist-template/lib/Tools/jedit
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit	Fri Dec 11 22:40:55 2009 +0100
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit	Fri Dec 11 23:29:18 2009 +0100
@@ -43,50 +43,56 @@
 JEDIT_LOGIC="$ISABELLE_LOGIC"
 JEDIT_PRINT_MODE=""
 
-declare -a JAVA_OPTIONS; eval "JAVA_OPTIONS=($JEDIT_JAVA_OPTIONS)"
-declare -a OPTIONS; eval "OPTIONS=($JEDIT_OPTIONS)"
+getoptions()
+{
+  OPTIND=1
+  while getopts "J:dj:l:m:" OPT
+  do
+    case "$OPT" in
+      J)
+        JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG"
+        ;;
+      d)
+        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xdebug"
+        JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n"
+        ;;
+      j)
+        ARGS["${#ARGS[@]}"]="$OPTARG"
+        ;;
+      l)
+        JEDIT_LOGIC="$OPTARG"
+        ;;
+      m)
+        if [ -z "$JEDIT_PRINT_MODE" ]; then
+          JEDIT_PRINT_MODE="$OPTARG"
+        else
+          JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
+        fi
+        ;;
+      \?)
+        usage
+        ;;
+    esac
+  done
+}
 
-while getopts "J:dj:l:m:" OPT
-do
-  case "$OPT" in
-    J)
-      JAVA_OPTIONS["${#JAVA_OPTIONS[@]}"]="$OPTARG"
-      ;;
-    d)
-      JAVA_OPTIONS["${#JAVA_OPTIONS[@]}"]="-Xdebug"
-      JAVA_OPTIONS["${#JAVA_OPTIONS[@]}"]="-Xrunjdwp:transport=dt_socket,server=y,suspend=n"
-      ;;
-    j)
-      OPTIONS["${#OPTIONS[@]}"]="$OPTARG"
-      ;;
-    l)
-      JEDIT_LOGIC="$OPTARG"
-      ;;
-    m)
-      if [ -z "$PRINT_MODE" ]; then
-        PRINT_MODE="$OPTARG"
-      else
-        PRINT_MODE="$PRINT_MODE,$OPTARG"
-      fi
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_ARGS)"
+declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
 
+declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
+getoptions "${OPTIONS[@]}"
+
+getoptions "$@"
 shift $(($OPTIND - 1))
 
 
 # args
 
-declare -a FILES=()
-
 if [ "$#" -eq 0 ]; then
-  FILES["${#FILES[@]}"]="Scratch.thy"
+  ARGS["${#ARGS[@]}"]="Scratch.thy"
 else
   while [ "$#" -gt 0 ]; do
-    FILES["${#FILES[@]}"]="$(jvmpath "$1")"
+    ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
     shift
   done
 fi
@@ -104,6 +110,6 @@
 
 export JEDIT_LOGIC JEDIT_PRINT_MODE
 
-exec "$ISABELLE_TOOL" java "${JAVA_OPTIONS[@]}" \
+exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
   -jar "$(jvmpath "$JEDIT_HOME/jedit.jar")" \
-  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${OPTIONS[@]}" "${FILES[@]}"
+  "-settings=$(jvmpath "$ISABELLE_HOME_USER/jedit")" "${ARGS[@]}"
diff -r d1040b77b189 -r d0ff1c3a91ea src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Dec 11 22:40:55 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri Dec 11 23:29:18 2009 +0100
@@ -55,11 +55,19 @@
 
   /* settings */
 
-  def get_logic(): String =
+  def cmd_args(): List[String] =
   {
-    val logic = Isabelle.Property("logic")
-    if (logic != null) logic
-    else system.getenv_strict("ISABELLE_LOGIC")
+    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+    val logic = {
+      val logic1 = Isabelle.Property("logic")
+      if (logic1 != null && logic1 != "") logic1
+      else {
+        val logic2 = system.getenv("JEDIT_LOGIC")
+        if (logic2 != "") logic2
+        else system.getenv_strict("ISABELLE_LOGIC")
+      }
+    }
+    modes ++ List(logic)
   }
 
 
@@ -86,7 +94,7 @@
     val theory_view = new Theory_View(Isabelle.session, text_area)   // FIXME multiple text areas!?
     mapping += (buffer -> theory_view)
 
-    Isabelle.session.start(Isabelle.get_logic())
+    Isabelle.session.start(Isabelle.cmd_args())
     theory_view.activate()
     Isabelle.session.begin_document(buffer.getName)
   }
diff -r d1040b77b189 -r d0ff1c3a91ea src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Fri Dec 11 22:40:55 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Fri Dec 11 23:29:18 2009 +0100
@@ -20,7 +20,7 @@
 
   /* main actor */
 
-  private case class Start(logic: String)
+  private case class Start(args: List[String])
   private case object Stop
 
   private var prover: Isabelle_Process with Isar_Document = null
@@ -29,12 +29,9 @@
   private val session_actor = actor {
     loop {
       react {
-        case Start(logic) =>
+        case Start(args) =>
           if (prover == null) {
-            prover =
-              new Isabelle_Process(system, self,   // FIXME avoid hardwired options
-                  "-m", "xsymbols", "-m", "no_brackets", "-m", "no_type_brackets", logic)
-                with Isar_Document
+            prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
             reply(())
           }
 
@@ -55,7 +52,7 @@
     }
   }
 
-  def start(logic: String) { session_actor !? Start(logic) }
+  def start(args: List[String]) { session_actor !? Start(args) }
   def stop() { session_actor ! Stop }
   def input(change: Change) { session_actor ! change }