src/Pure/System/session.scala
changeset 45709 87017fcbad83
parent 45672 a497c5d4a523
child 46120 f7ee2e5a83dd
     1.1 --- a/src/Pure/System/session.scala	Thu Dec 01 13:34:16 2011 +0100
     1.2 +++ b/src/Pure/System/session.scala	Thu Dec 01 14:29:14 2011 +0100
     1.3 @@ -211,7 +211,7 @@
     1.4        def cancel() { timer.cancel() }
     1.5      }
     1.6  
     1.7 -    var prover: Option[Isabelle_Process with Isabelle_Document] = None
     1.8 +    var prover: Option[Isabelle_Process with Protocol] = None
     1.9  
    1.10  
    1.11      /* delayed command changes */
    1.12 @@ -365,7 +365,7 @@
    1.13            }
    1.14          case Isabelle_Markup.Assign_Execs if result.is_raw =>
    1.15            XML.content(result.body).mkString match {
    1.16 -            case Isabelle_Document.Assign(id, assign) =>
    1.17 +            case Protocol.Assign(id, assign) =>
    1.18                try { handle_assign(id, assign) }
    1.19                catch { case _: Document.State.Fail => bad_result(result) }
    1.20              case _ => bad_result(result)
    1.21 @@ -378,7 +378,7 @@
    1.22            }
    1.23          case Isabelle_Markup.Removed_Versions if result.is_raw =>
    1.24            XML.content(result.body).mkString match {
    1.25 -            case Isabelle_Document.Removed(removed) =>
    1.26 +            case Protocol.Removed(removed) =>
    1.27                try { handle_removed(removed) }
    1.28                catch { case _: Document.State.Fail => bad_result(result) }
    1.29              case _ => bad_result(result)
    1.30 @@ -429,8 +429,7 @@
    1.31          case Start(timeout, args) if prover.isEmpty =>
    1.32            if (phase == Session.Inactive || phase == Session.Failed) {
    1.33              phase = Session.Startup
    1.34 -            prover =
    1.35 -              Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isabelle_Document)
    1.36 +            prover = Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Protocol)
    1.37            }
    1.38  
    1.39          case Stop =>