--- 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)
}