simplified init message -- removed redundant session property;
authorwenzelm
Wed Dec 30 22:56:46 2009 +0100 (2009-12-30 ago)
changeset 3421499eefb83a35d
parent 34213 9e86c1ca6e51
child 34215 f0322b595146
simplified init message -- removed redundant session property;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/General/markup.ML	Wed Dec 30 22:29:37 2009 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Wed Dec 30 22:56:46 2009 +0100
     1.3 @@ -107,7 +107,6 @@
     1.4    val disposedN: string val disposed: T
     1.5    val editN: string val edit: string -> string -> T
     1.6    val pidN: string
     1.7 -  val sessionN: string
     1.8    val promptN: string val prompt: T
     1.9    val readyN: string val ready: T
    1.10    val no_output: output * output
    1.11 @@ -313,7 +312,6 @@
    1.12  (* messages *)
    1.13  
    1.14  val pidN = "pid";
    1.15 -val sessionN = "session";
    1.16  
    1.17  val (promptN, prompt) = markup_elem "prompt";
    1.18  val (readyN, ready) = markup_elem "ready";
     2.1 --- a/src/Pure/General/markup.scala	Wed Dec 30 22:29:37 2009 +0100
     2.2 +++ b/src/Pure/General/markup.scala	Wed Dec 30 22:56:46 2009 +0100
     2.3 @@ -159,7 +159,6 @@
     2.4    /* messages */
     2.5  
     2.6    val PID = "pid"
     2.7 -  val SESSION = "session"
     2.8  
     2.9    val MESSAGE = "message"
    2.10    val CLASS = "class"
     3.1 --- a/src/Pure/System/isabelle_process.ML	Wed Dec 30 22:29:37 2009 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Dec 30 22:56:46 2009 +0100
     3.3 @@ -44,11 +44,7 @@
     3.4    message out_stream ch (Position.properties_of (Position.thread_data ())) body;
     3.5  
     3.6  fun init_message out_stream =
     3.7 -  let
     3.8 -    val pid = (Markup.pidN, process_id ());
     3.9 -    val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
    3.10 -    val text = Session.welcome ();
    3.11 -  in message out_stream "A" [pid, session] text end;
    3.12 +  message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
    3.13  
    3.14  end;
    3.15  
     4.1 --- a/src/Pure/System/isabelle_process.scala	Wed Dec 30 22:29:37 2009 +0100
     4.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Dec 30 22:56:46 2009 +0100
     4.3 @@ -124,8 +124,6 @@
     4.4    @volatile private var proc: Process = null
     4.5    @volatile private var closing = false
     4.6    @volatile private var pid: String = null
     4.7 -  @volatile private var the_session: String = null
     4.8 -  def session = the_session
     4.9  
    4.10  
    4.11    /* results */
    4.12 @@ -133,9 +131,7 @@
    4.13    private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree])
    4.14    {
    4.15      if (kind == Kind.INIT) {
    4.16 -      val map = Map(props: _*)
    4.17 -      if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
    4.18 -      if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
    4.19 +      for ((Markup.PID, p) <- props) pid = p
    4.20      }
    4.21      receiver ! new Result(kind, props, body)
    4.22    }