src/Pure/System/session.scala
changeset 40478 4bae781b8f7c
parent 39701 7c351c1c0624
child 40479 cc06f5528bb1
     1.1 --- a/src/Pure/System/session.scala	Thu Nov 11 13:23:39 2010 +0100
     1.2 +++ b/src/Pure/System/session.scala	Thu Nov 11 16:48:46 2010 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4    def current_state(): Document.State = global_state.peek()
     1.5  
     1.6    private case object Interrupt_Prover
     1.7 -  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
     1.8 +  private case class Edit_Version(edits: List[Document.Text_Edit])
     1.9    private case class Start(timeout: Int, args: List[String])
    1.10  
    1.11    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    1.12 @@ -289,7 +289,7 @@
    1.13  
    1.14    def interrupt() { session_actor ! Interrupt_Prover }
    1.15  
    1.16 -  def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
    1.17 +  def edit_version(edits: List[Document.Text_Edit]) { session_actor !? Edit_Version(edits) }
    1.18  
    1.19    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
    1.20      global_state.peek().snapshot(name, pending_edits)