more abstract Session.start, without prover command-line;
Isabelle_Process.apply is directly based on ML_Process;
clarified Isabelle_Process.main command-line;
tuned signature;

--- a/src/Pure/PIDE/batch_session.scala	Tue Mar 08 11:18:21 2016 +0100
+++ b/src/Pure/PIDE/batch_session.scala	Tue Mar 08 14:44:11 2016 +0100
@@ -58,7 +58,8 @@
         case _ =>
       }
 
-    prover_session.start("Isabelle", List("-q", parent_session))
+    prover_session.start(receiver =>
+      Isabelle_Process(options, heap = parent_session, receiver = receiver))
 
     batch_session
   }

--- a/src/Pure/PIDE/prover.scala	Tue Mar 08 11:18:21 2016 +0100
+++ b/src/Pure/PIDE/prover.scala	Tue Mar 08 14:44:11 2016 +0100
@@ -39,6 +39,7 @@
   /* messages */
 
   sealed abstract class Message
+  type Receiver = Message => Unit
 
   class Input(val name: String, val args: List[String]) extends Message
   {
@@ -85,7 +86,7 @@
 
 
 abstract class Prover(
-  receiver: Prover.Message => Unit,
+  receiver: Prover.Receiver,
   system_channel: System_Channel,
   system_process: Prover.System_Process) extends Protocol
 {

--- a/src/Pure/PIDE/resources.scala	Tue Mar 08 11:18:21 2016 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Mar 08 14:44:11 2016 +0100
@@ -132,11 +132,5 @@
     Thy_Syntax.parse_change(this, reparse_limit, previous, doc_blobs, edits)
 
   def commit(change: Session.Change) { }
-
-
-  /* prover process */
-
-  def start_prover(receiver: Prover.Message => Unit, name: String, args: List[String]): Prover =
-    Isabelle_Process(receiver, args)
 }
 

--- a/src/Pure/PIDE/session.scala	Tue Mar 08 11:18:21 2016 +0100
+++ b/src/Pure/PIDE/session.scala	Tue Mar 08 14:44:11 2016 +0100
@@ -212,7 +212,7 @@
 
   /* internal messages */
 
-  private case class Start(name: String, args: List[String])
+  private case class Start(start_prover: Prover.Receiver => Prover)
   private case object Stop
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Protocol_Command(name: String, args: List[String])
@@ -532,10 +532,10 @@
           case input: Prover.Input =>
             all_messages.post(input)
 
-          case Start(name, args) if !prover.defined =>
+          case Start(start_prover) if !prover.defined =>
             if (phase == Session.Inactive || phase == Session.Failed) {
               phase = Session.Startup
-              prover.set(resources.start_prover(manager.send(_), name, args))
+              prover.set(start_prover(manager.send(_)))
             }
 
           case Stop =>
@@ -601,8 +601,8 @@
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
     global_state.value.snapshot(name, pending_edits)
 
-  def start(name: String, args: List[String])
-  { manager.send(Start(name, args)) }
+  def start(start_prover: Prover.Receiver => Prover)
+  { manager.send(Start(start_prover)) }
 
   def stop()
   {

--- a/src/Pure/System/isabelle_process.scala	Tue Mar 08 11:18:21 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala	Tue Mar 08 14:44:11 2016 +0100
@@ -10,21 +10,23 @@
 object Isabelle_Process
 {
   def apply(
-    receiver: Prover.Message => Unit = Console.println(_),
-    prover_args: List[String] = Nil): Isabelle_Process =
+    options: Options,
+    heap: String = "",
+    args: List[String] = Nil,
+    modes: List[String] = Nil,
+    secure: Boolean = false,
+    receiver: Prover.Receiver = Console.println(_)): Isabelle_Process =
   {
-    val system_channel = System_Channel()
-    val system_process =
+    val channel = System_Channel()
+    val process =
       try {
-        val process =
-          Bash.process("\"$ISABELLE_PROCESS\" -P " + File.bash_string(system_channel.server_name) +
-            " " + File.bash_args(prover_args))
-        process.stdin.close
-        process
+        ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
+          process_socket = channel.server_name)
       }
-      catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }
+      catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
+    process.stdin.close
 
-    new Isabelle_Process(receiver, system_channel, system_process)
+    new Isabelle_Process(receiver, channel, process)
   }
 
 
@@ -33,7 +35,7 @@
   def main(args: Array[String])
   {
     Command_Line.tool {
-      var ml_args: List[String] = Nil
+      var eval_args: List[String] = Nil
       var modes: List[String] = Nil
       var options = Options.init()
 
@@ -50,8 +52,8 @@
   $ISABELLE_PATH; if it contains a slash, it is taken as literal file;
   if it is RAW_ML_SYSTEM, the initial ML heap is used.
 """,
-        "e:" -> (arg => ml_args = ml_args ::: List("--eval", arg)),
-        "f:" -> (arg => ml_args = ml_args ::: List("--use", arg)),
+        "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)),
+        "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)),
         "m:" -> (arg => modes = arg :: modes),
         "o:" -> (arg => options = options + arg))
 
@@ -62,17 +64,15 @@
           case _ => getopts.usage()
         }
 
-      ML_Process(options, heap = heap, args = ml_args, modes = modes).
+      ML_Process(options, heap = heap, args = eval_args ::: args.toList, modes = modes).
         result().print_stdout.rc
     }
   }
 }
 
 class Isabelle_Process private(
-    receiver: Prover.Message => Unit,
-    system_channel: System_Channel,
-    system_process: Prover.System_Process)
-  extends Prover(receiver, system_channel, system_process)
+    receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process)
+  extends Prover(receiver, channel, process)
 {
   def encode(s: String): String = Symbol.encode(s)
   def decode(s: String): String = Symbol.decode(s)

--- a/src/Pure/System/ml_process.scala	Tue Mar 08 11:18:21 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Tue Mar 08 14:44:11 2016 +0100
@@ -12,9 +12,9 @@
   def apply(options: Options,
     heap: String = "",
     args: List[String] = Nil,
-    process_socket: String = "",
+    modes: List[String] = Nil,
     secure: Boolean = false,
-    modes: List[String] = Nil): Bash.Process =
+    process_socket: String = ""): Bash.Process =
   {
     val load_heaps =
     {
@@ -55,19 +55,18 @@
       }
       else Nil
 
-    val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
-
     val eval_modes =
       if (modes.isEmpty) Nil
       else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_raw _)(modes))
 
-
     // options
     val isabelle_process_options = Isabelle_System.tmp_file("options")
     File.write(isabelle_process_options, YXML.string_of_body(options.encode))
     val env = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = if (load_heaps.isEmpty) Nil else List("Options.load_default ()")
 
+    val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
+
     val eval_process =
       if (process_socket == "") Nil
       else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket))
@@ -75,7 +74,7 @@
     // bash
     val bash_args =
       Word.explode(Isabelle_System.getenv("ML_OPTIONS")) :::
-      (eval_heaps ::: eval_exit ::: eval_secure ::: eval_modes ::: eval_options ::: eval_process).
+      (eval_heaps ::: eval_exit ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
     Bash.process(env = env, script =

--- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Mar 08 11:18:21 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Mar 08 14:44:11 2016 +0100
@@ -69,15 +69,16 @@
       dirs = session_dirs(), sessions = List(session_name()))
   }
 
-  def session_args(): List[String] =
+  def session_start()
   {
-    (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
-     space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).
-      map(m => List("-m", m)).flatten ::: List("-q", session_name())
+    val modes =
+      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
+       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
+    PIDE.session.start(receiver =>
+      Isabelle_Process(
+        PIDE.options.value, heap = session_name(), modes = modes, receiver = receiver))
   }
 
-  def session_start(): Unit = PIDE.session.start("Isabelle", session_args())
-
   def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
 
   def session_list(): List[String] =