1.1 --- a/src/Pure/System/session.scala	Sun Jul 03 19:42:32 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sun Jul 03 19:53:35 2011 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
     1.5    {
     1.6      val this_actor = self
     1.7 -    var prover: Isabelle_Process with Isar_Document = null
     1.8 +    var prover: Option[Isabelle_Process with Isar_Document] = None
     1.9  
    1.10  
    1.11      /* document changes */
    1.12 @@ -188,7 +188,8 @@
    1.13                        case Some(command) =>
    1.14                          if (global_state.peek().lookup_command(command.id).isEmpty) {
    1.15                            global_state.change(_.define_command(command))
    1.16 -                          prover.define_command(command.id, system.symbols.encode(command.source))
    1.17 +                          prover.get.
    1.18 +                            define_command(command.id, system.symbols.encode(command.source))
    1.19                          }
    1.20                          Some(command.id)
    1.21                      }
    1.22 @@ -197,7 +198,7 @@
    1.23              (name -> Some(ids))
    1.24          }
    1.25        global_state.change(_.define_version(version, former_assignment))
    1.26 -      prover.edit_version(previous.id, version.id, id_edits)
    1.27 +      prover.get.edit_version(previous.id, version.id, id_edits)
    1.28      }
    1.29      //}}}
    1.30  
    1.31 @@ -276,41 +277,42 @@
    1.32      while (!finished) {
    1.33        receive {
    1.34          case Interrupt_Prover =>
    1.35 -          if (prover != null) prover.interrupt
    1.36 +          prover.map(_.interrupt)
    1.37  
    1.38 -        case Edit_Node(thy_name, header, text_edits) if prover != null =>
    1.39 +        case Edit_Node(thy_name, header, text_edits) if prover.isDefined =>
    1.40            edit_version(List((thy_name, Some(text_edits))))
    1.41            reply(())
    1.42  
    1.43 -        case Init_Node(thy_name, header, text) if prover != null =>
    1.44 +        case Init_Node(thy_name, header, text) if prover.isDefined =>
    1.45            // FIXME compare with existing node
    1.46            edit_version(List(
    1.47              (thy_name, None),
    1.48              (thy_name, Some(List(Text.Edit.insert(0, text))))))
    1.49            reply(())
    1.50  
    1.51 -        case change: Document.Change if prover != null =>
    1.52 +        case change: Document.Change if prover.isDefined =>
    1.53            handle_change(change)
    1.54  
    1.55          case result: Isabelle_Process.Result => handle_result(result)
    1.56  
    1.57 -        case Start(timeout, args) if prover == null =>
    1.58 +        case Start(timeout, args) if prover.isEmpty =>
    1.59            if (phase == Session.Inactive || phase == Session.Failed) {
    1.60              phase = Session.Startup
    1.61 -            prover = new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document
    1.62 +            prover =
    1.63 +              Some(new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document)
    1.64            }
    1.65  
    1.66          case Stop =>
    1.67            if (phase == Session.Ready) {
    1.68              global_state.change(_ => Document.State.init)  // FIXME event bus!?
    1.69              phase = Session.Shutdown
    1.70 -            prover.terminate
    1.71 +            prover.get.terminate
    1.72              phase = Session.Inactive
    1.73            }
    1.74            finished = true
    1.75            reply(())
    1.76  
    1.77 -        case bad if prover != null =>
    1.78 +        case bad if prover.isDefined =>
    1.79            System.err.println("session_actor: ignoring bad message " + bad)
    1.80        }
    1.81      }