# HG changeset patch
# User wenzelm
# Date 1457465614 -3600
# Node ID 40624a9e94c45e792ab430dafdaf5d86523f2efa
# Parent  2e352f63d15fb24552ca8d4c97745c859a6dd126
tuned signature;

diff -r 2e352f63d15f -r 40624a9e94c4 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Mar 08 20:24:41 2016 +0100
+++ b/src/Pure/System/isabelle_process.ML	Tue Mar 08 20:33:34 2016 +0100
@@ -10,7 +10,7 @@
   val protocol_command: string -> (string list -> unit) -> unit
   val reset_tracing: Document_ID.exec -> unit
   val crashes: exn list Synchronized.var
-  val init: string -> unit
+  val init_protocol: string -> unit
   val init_options: unit -> unit
 end;
 
@@ -181,12 +181,12 @@
 end;
 
 
-(* init *)
+(* init protocol *)
 
 val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
 val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
 
-val init = uninterruptible (fn _ => fn socket =>
+val init_protocol = uninterruptible (fn _ => fn socket =>
   let
     val _ = SHA1_Samples.test ()
       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
diff -r 2e352f63d15f -r 40624a9e94c4 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Mar 08 20:24:41 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala	Tue Mar 08 20:33:34 2016 +0100
@@ -21,7 +21,7 @@
     val process =
       try {
         ML_Process(options, heap = heap, args = args, modes = modes, secure = secure,
-          process_socket = channel.server_name)
+          channel = Some(channel))
       }
       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
     process.stdin.close
diff -r 2e352f63d15f -r 40624a9e94c4 src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Tue Mar 08 20:24:41 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Tue Mar 08 20:33:34 2016 +0100
@@ -15,7 +15,7 @@
     modes: List[String] = Nil,
     secure: Boolean = false,
     redirect: Boolean = false,
-    process_socket: String = ""): Bash.Process =
+    channel: Option[System_Channel] = None): Bash.Process =
   {
     val load_heaps =
     {
@@ -72,8 +72,11 @@
     val eval_secure = if (secure) List("Secure.set_secure ()") else Nil
 
     val eval_process =
-      if (process_socket == "") List("Isabelle_Process.init_options ()")
-      else List("Isabelle_Process.init " + ML_Syntax.print_string_raw(process_socket))
+      channel match {
+        case None => List("Isabelle_Process.init_options ()")
+        case Some(ch) =>
+          List("Isabelle_Process.init_protocol " + ML_Syntax.print_string_raw(ch.server_name))
+      }
 
     // bash
     val bash_args =