src/Pure/System/session.scala
changeset 38150 67fc24df3721
parent 37849 4f9de312cc23
child 38221 e0f00f0945b4
     1.1 --- a/src/Pure/System/session.scala	Thu Aug 05 13:41:00 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Thu Aug 05 14:35:35 2010 +0200
     1.3 @@ -76,7 +76,6 @@
     1.4  
     1.5    private case class Start(timeout: Int, args: List[String])
     1.6    private case object Stop
     1.7 -  private case class Begin_Document(path: String)
     1.8  
     1.9    private lazy val session_actor = actor {
    1.10  
    1.11 @@ -84,8 +83,9 @@
    1.12  
    1.13      def register(entity: Session.Entity) { entities += (entity.id -> entity) }
    1.14  
    1.15 -    var documents = Map[Isar_Document.Document_ID, Document]()
    1.16 +    var documents = Map[Document.Version_ID, Document]()
    1.17      def register_document(doc: Document) { documents += (doc.id -> doc) }
    1.18 +    register_document(Document.init)
    1.19  
    1.20  
    1.21      /* document changes */
    1.22 @@ -94,22 +94,31 @@
    1.23      {
    1.24        require(change.parent.isDefined)
    1.25  
    1.26 -      val (changes, doc) = change.result.join
    1.27 -      val id_changes = changes map {
    1.28 -        case (c1, c2) =>
    1.29 -          (c1.map(_.id).getOrElse(""),
    1.30 -           c2 match {
    1.31 -              case None => None
    1.32 -              case Some(command) =>
    1.33 -                if (!lookup_command(command.id).isDefined) {
    1.34 -                  register(command)
    1.35 -                  prover.define_command(command.id, system.symbols.encode(command.source))
    1.36 -                }
    1.37 -                Some(command.id)
    1.38 -            })
    1.39 -      }
    1.40 +      val (node_edits, doc) = change.result.join
    1.41 +      val id_edits =
    1.42 +        node_edits map {
    1.43 +          case (name, None) => (name, None)
    1.44 +          case (name, Some(cmd_edits)) =>
    1.45 +            val chs =
    1.46 +              cmd_edits map {
    1.47 +                case (c1, c2) =>
    1.48 +                  val id1 = c1.map(_.id)
    1.49 +                  val id2 =
    1.50 +                    c2 match {
    1.51 +                      case None => None
    1.52 +                      case Some(command) =>
    1.53 +                        if (!lookup_command(command.id).isDefined) {
    1.54 +                          register(command)
    1.55 +                          prover.define_command(command.id, system.symbols.encode(command.source))
    1.56 +                        }
    1.57 +                        Some(command.id)
    1.58 +                    }
    1.59 +                  (id1, id2)
    1.60 +              }
    1.61 +            (name -> Some(chs))
    1.62 +        }
    1.63        register_document(doc)
    1.64 -      prover.edit_document(change.parent.get.id, doc.id, id_changes)
    1.65 +      prover.edit_document(change.parent.get.id, doc.id, id_edits)
    1.66      }
    1.67  
    1.68  
    1.69 @@ -229,13 +238,6 @@
    1.70              prover = null
    1.71            }
    1.72  
    1.73 -        case Begin_Document(path: String) if prover != null =>
    1.74 -          val id = create_id()
    1.75 -          val doc = Document.empty(id)
    1.76 -          register_document(doc)
    1.77 -          prover.begin_document(id, path)
    1.78 -          reply(doc)
    1.79 -
    1.80          case change: Change if prover != null =>
    1.81            handle_change(change)
    1.82  
    1.83 @@ -304,7 +306,4 @@
    1.84  
    1.85    def stop() { session_actor ! Stop }
    1.86    def input(change: Change) { session_actor ! change }
    1.87 -
    1.88 -  def begin_document(path: String): Document =
    1.89 -    (session_actor !? Begin_Document(path)).asInstanceOf[Document]
    1.90  }