src/Pure/System/session.scala
changeset 38370 8b15d0f98962
parent 38366 fea82d1add74
child 38373 e8197eea3cd0
     1.1 --- a/src/Pure/System/session.scala	Fri Aug 13 18:16:50 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Fri Aug 13 18:21:19 2010 +0200
     1.3 @@ -20,16 +20,6 @@
     1.4    case object Global_Settings
     1.5    case object Perspective
     1.6    case class Commands_Changed(set: Set[Command])
     1.7 -
     1.8 -
     1.9 -
    1.10 -  /* managed entities */
    1.11 -
    1.12 -  trait Entity
    1.13 -  {
    1.14 -    val id: Document.ID
    1.15 -    def consume(message: XML.Tree, forward: Command => Unit): Unit
    1.16 -  }
    1.17  }
    1.18  
    1.19  
    1.20 @@ -72,13 +62,9 @@
    1.21    @volatile private var syntax = new Outer_Syntax(system.symbols)
    1.22    def current_syntax: Outer_Syntax = syntax
    1.23  
    1.24 -  @volatile private var entities = Map[Document.ID, Session.Entity]()
    1.25 -  def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id)
    1.26 -  def lookup_command(id: Document.ID): Option[Command] =
    1.27 -    lookup_entity(id) match {
    1.28 -      case Some(cmd: Command) => Some(cmd)
    1.29 -      case _ => None
    1.30 -    }
    1.31 +  @volatile private var global_state = Document.State.init
    1.32 +  private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
    1.33 +  def current_state(): Document.State = global_state
    1.34  
    1.35    private case class Started(timeout: Int, args: List[String])
    1.36    private case object Stop
    1.37 @@ -87,12 +73,6 @@
    1.38  
    1.39      var prover: Isabelle_Process with Isar_Document = null
    1.40  
    1.41 -    def register(entity: Session.Entity) { entities += (entity.id -> entity) }
    1.42 -
    1.43 -    var documents = Map[Document.Version_ID, Document]()
    1.44 -    def register_document(doc: Document) { documents += (doc.id -> doc) }
    1.45 -    register_document(Document.init)
    1.46 -
    1.47  
    1.48      /* document changes */
    1.49  
    1.50 @@ -101,14 +81,21 @@
    1.51      {
    1.52        require(change.is_finished)
    1.53  
    1.54 -      val old_id = change.prev.join.id
    1.55 +      val old_doc = change.prev.join
    1.56        val (node_edits, doc) = change.result.join
    1.57  
    1.58 +      var former_assignment = current_state().the_assignment(old_doc).join
    1.59 +      for {
    1.60 +        (name, Some(cmd_edits)) <- node_edits
    1.61 +        (prev, None) <- cmd_edits
    1.62 +        removed <- old_doc.nodes(name).commands.get_after(prev)
    1.63 +      } former_assignment -= removed
    1.64 +
    1.65        val id_edits =
    1.66          node_edits map {
    1.67            case (name, None) => (name, None)
    1.68            case (name, Some(cmd_edits)) =>
    1.69 -            val chs =
    1.70 +            val ids =
    1.71                cmd_edits map {
    1.72                  case (c1, c2) =>
    1.73                    val id1 = c1.map(_.id)
    1.74 @@ -116,18 +103,18 @@
    1.75                      c2 match {
    1.76                        case None => None
    1.77                        case Some(command) =>
    1.78 -                        if (!lookup_command(command.id).isDefined) {
    1.79 -                          register(command)
    1.80 +                        if (current_state().lookup_command(command.id).isEmpty) {
    1.81 +                          change_state(_.define_command(command))
    1.82                            prover.define_command(command.id, system.symbols.encode(command.source))
    1.83                          }
    1.84                          Some(command.id)
    1.85                      }
    1.86                    (id1, id2)
    1.87                }
    1.88 -            (name -> Some(chs))
    1.89 +            (name -> Some(ids))
    1.90          }
    1.91 -      register_document(doc)
    1.92 -      prover.edit_document(old_id, doc.id, id_edits)
    1.93 +      change_state(_.define_document(doc, former_assignment))
    1.94 +      prover.edit_document(old_doc.id, doc.id, id_edits)
    1.95      }
    1.96      //}}}
    1.97  
    1.98 @@ -144,47 +131,38 @@
    1.99      {
   1.100        raw_results.event(result)
   1.101  
   1.102 -      val target_id: Option[Document.ID] = Position.get_id(result.properties)
   1.103 -      val target: Option[Session.Entity] =
   1.104 -        target_id match {
   1.105 -          case None => None
   1.106 -          case Some(id) => lookup_entity(id)
   1.107 +      Position.get_id(result.properties) match {
   1.108 +        case Some(target_id) =>
   1.109 +          try {
   1.110 +            val (st, state) = global_state.accumulate(target_id, result.message)
   1.111 +            global_state = state
   1.112 +            indicate_command_change(st.command)  // FIXME forward Command.State (!?)
   1.113 +          }
   1.114 +          catch {
   1.115 +            case _: Document.Failed_State =>
   1.116 +              if (result.is_status) {
   1.117 +                result.body match {
   1.118 +                  case List(Isar_Document.Assign(edits)) =>
   1.119 +                    try { change_state(_.assign(target_id, edits)) }
   1.120 +                    catch { case _: Document.Failed_State => bad_result(result) }
   1.121 +                  case _ => bad_result(result)
   1.122 +                }
   1.123 +              }
   1.124 +              else bad_result(result)
   1.125 +          }
   1.126 +        case None =>
   1.127 +          if (result.is_status) {
   1.128 +            result.body match {
   1.129 +              // keyword declarations   // FIXME always global!?
   1.130 +              case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   1.131 +              case List(Keyword.Keyword_Decl(name)) => syntax += name
   1.132 +              case _ => if (!result.is_ready) bad_result(result)
   1.133 +            }
   1.134 +          }
   1.135 +          else if (result.kind == Markup.EXIT) prover = null
   1.136 +          else if (result.is_raw) raw_output.event(result)
   1.137 +          else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
   1.138          }
   1.139 -      if (target.isDefined) target.get.consume(result.message, indicate_command_change)
   1.140 -      else if (result.is_status) {
   1.141 -        // global status message
   1.142 -        result.body match {
   1.143 -
   1.144 -          // execution assignment
   1.145 -          case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
   1.146 -            documents.get(target_id.get) match {
   1.147 -              case Some(doc) =>
   1.148 -                val execs =
   1.149 -                  for {
   1.150 -                    Isar_Document.Edit(cmd_id, exec_id) <- edits
   1.151 -                    cmd <- lookup_command(cmd_id)
   1.152 -                  } yield {
   1.153 -                    val st = cmd.assign_exec(exec_id)  // FIXME session state
   1.154 -                    register(st)
   1.155 -                    (cmd, st)
   1.156 -                  }
   1.157 -                doc.assign_execs(execs)  // FIXME session state
   1.158 -              case None => bad_result(result)
   1.159 -            }
   1.160 -
   1.161 -          // keyword declarations
   1.162 -          case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   1.163 -          case List(Keyword.Keyword_Decl(name)) => syntax += name
   1.164 -
   1.165 -          case _ => if (!result.is_ready) bad_result(result)
   1.166 -        }
   1.167 -      }
   1.168 -      else if (result.kind == Markup.EXIT)
   1.169 -        prover = null
   1.170 -      else if (result.is_raw)
   1.171 -        raw_output.event(result)
   1.172 -      else if (!result.is_system)   // FIXME syslog (!?)
   1.173 -        bad_result(result)
   1.174      }
   1.175      //}}}
   1.176  
   1.177 @@ -325,11 +303,14 @@
   1.178  
   1.179      def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   1.180      {
   1.181 +      val state_snapshot = current_state()
   1.182        val history_snapshot = history
   1.183  
   1.184 -      require(history_snapshot.exists(_.is_assigned))
   1.185 +      val found_stable = history_snapshot.find(change =>
   1.186 +        change.is_finished && state_snapshot.is_assigned(change.document.join))
   1.187 +      require(found_stable.isDefined)
   1.188 +      val stable = found_stable.get
   1.189        val latest = history_snapshot.head
   1.190 -      val stable = history_snapshot.find(_.is_assigned).get
   1.191  
   1.192        val edits =
   1.193          (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
   1.194 @@ -342,7 +323,10 @@
   1.195          val is_outdated = !(pending_edits.isEmpty && latest == stable)
   1.196          def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
   1.197          def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   1.198 -        def state(command: Command): Command.State = document.current_state(command)
   1.199 +        def lookup_command(id: Document.Command_ID): Option[Command] =
   1.200 +          state_snapshot.lookup_command(id)
   1.201 +        def state(command: Command): Command.State =
   1.202 +          state_snapshot.command_state(document, command)
   1.203        }
   1.204      }
   1.205  
   1.206 @@ -358,7 +342,7 @@
   1.207              val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
   1.208                isabelle.Future.fork {
   1.209                  val old_doc = prev.join
   1.210 -                old_doc.await_assignment
   1.211 +                val former_assignment = current_state().the_assignment(old_doc).join  // FIXME async!?
   1.212                  Document.text_edits(Session.this, old_doc, edits)
   1.213                }
   1.214              val new_change = new Document.Change(prev, edits, result)