diff -r 5fab62ae3532 -r ac6648c0c0fb src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Aug 09 10:41:17 2013 +0200 +++ b/src/Pure/System/session.scala Fri Aug 09 11:18:36 2013 +0200 @@ -238,6 +238,7 @@ /* actor messages */ private case class Start(args: List[String]) + private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Change( doc_edits: List[Document.Edit_Command], previous: Document.Version, @@ -506,6 +507,9 @@ global_options.event(Session.Global_Options(options)) reply(()) + case Cancel_Exec(exec_id) if prover.isDefined => + prover.get.cancel_exec(exec_id) + case Session.Raw_Edits(edits) if prover.isDefined => handle_raw_edits(edits) reply(()) @@ -552,6 +556,8 @@ session_actor !? Stop } + def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) } + def update(edits: List[Document.Edit_Text]) { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }