simplified init message -- removed redundant session property;

--- a/src/Pure/General/markup.ML	Wed Dec 30 22:29:37 2009 +0100
+++ b/src/Pure/General/markup.ML	Wed Dec 30 22:56:46 2009 +0100
@@ -107,7 +107,6 @@
   val disposedN: string val disposed: T
   val editN: string val edit: string -> string -> T
   val pidN: string
-  val sessionN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val no_output: output * output
@@ -313,7 +312,6 @@
 (* messages *)
 
 val pidN = "pid";
-val sessionN = "session";
 
 val (promptN, prompt) = markup_elem "prompt";
 val (readyN, ready) = markup_elem "ready";

--- a/src/Pure/General/markup.scala	Wed Dec 30 22:29:37 2009 +0100
+++ b/src/Pure/General/markup.scala	Wed Dec 30 22:56:46 2009 +0100
@@ -159,7 +159,6 @@
   /* messages */
 
   val PID = "pid"
-  val SESSION = "session"
 
   val MESSAGE = "message"
   val CLASS = "class"

--- a/src/Pure/System/isabelle_process.ML	Wed Dec 30 22:29:37 2009 +0100
+++ b/src/Pure/System/isabelle_process.ML	Wed Dec 30 22:56:46 2009 +0100
@@ -44,11 +44,7 @@
   message out_stream ch (Position.properties_of (Position.thread_data ())) body;
 
 fun init_message out_stream =
-  let
-    val pid = (Markup.pidN, process_id ());
-    val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
-    val text = Session.welcome ();
-  in message out_stream "A" [pid, session] text end;
+  message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
 
 end;
 

--- a/src/Pure/System/isabelle_process.scala	Wed Dec 30 22:29:37 2009 +0100
+++ b/src/Pure/System/isabelle_process.scala	Wed Dec 30 22:56:46 2009 +0100
@@ -124,8 +124,6 @@
   @volatile private var proc: Process = null
   @volatile private var closing = false
   @volatile private var pid: String = null
-  @volatile private var the_session: String = null
-  def session = the_session
 
 
   /* results */
@@ -133,9 +131,7 @@
   private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree])
   {
     if (kind == Kind.INIT) {
-      val map = Map(props: _*)
-      if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
-      if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
+      for ((Markup.PID, p) <- props) pid = p
     }
     receiver ! new Result(kind, props, body)
   }