explicit Document.State value, instead of individual state variables in Session, Command, Document;
authorwenzelm
Fri Aug 13 18:21:19 2010 +0200 (2010-08-13)
changeset 383708b15d0f98962
parent 38369 5584ab3d5b13
child 38371 5b615a4a3a68
explicit Document.State value, instead of individual state variables in Session, Command, Document;
Session.snapshot: pure value based on Document.State;
Document.edit_texts: no treatment of state assignment here;
src/Pure/Isar/isar_document.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
     1.1 --- a/src/Pure/Isar/isar_document.scala	Fri Aug 13 18:16:50 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_document.scala	Fri Aug 13 18:21:19 2010 +0200
     1.3 @@ -12,9 +12,12 @@
     1.4    /* protocol messages */
     1.5  
     1.6    object Assign {
     1.7 -    def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
     1.8 +    def unapply(msg: XML.Tree): Option[List[(Document.Command_ID, Document.Exec_ID)]] =
     1.9        msg match {
    1.10 -        case XML.Elem(Markup.Assign, edits) => Some(edits)
    1.11 +        case XML.Elem(Markup.Assign, edits) =>
    1.12 +          val id_edits = edits.map(Edit.unapply)
    1.13 +          if (id_edits.forall(_.isDefined)) Some(id_edits.map(_.get))
    1.14 +          else None
    1.15          case _ => None
    1.16        }
    1.17    }
     2.1 --- a/src/Pure/PIDE/command.scala	Fri Aug 13 18:16:50 2010 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Fri Aug 13 18:21:19 2010 +0200
     2.3 @@ -40,10 +40,6 @@
     2.4      val reverse_results: List[XML.Tree],
     2.5      val markup: Markup_Text)
     2.6    {
     2.7 -    def this(command: Command) =
     2.8 -      this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup)
     2.9 -
    2.10 -
    2.11      /* content */
    2.12  
    2.13      lazy val results = reverse_results.reverse
    2.14 @@ -154,7 +150,6 @@
    2.15      val id: Document.Command_ID,
    2.16      val span: Thy_Syntax.Span,
    2.17      val static_parent: Option[Command] = None)  // FIXME !?
    2.18 -  extends Session.Entity
    2.19  {
    2.20    /* classification */
    2.21  
    2.22 @@ -178,54 +173,18 @@
    2.23    lazy val symbol_index = new Symbol.Index(source)
    2.24  
    2.25  
    2.26 -  /* accumulated messages */
    2.27 -
    2.28 -  @volatile protected var state = new Command.State(this)
    2.29 -  def current_state: Command.State = state
    2.30 -
    2.31 -  private case class Consume(message: XML.Tree, forward: Command => Unit)
    2.32 -  private case object Assign
    2.33 -
    2.34 -  private val accumulator = actor {
    2.35 -    var assigned = false
    2.36 -    loop {
    2.37 -      react {
    2.38 -        case Consume(message, forward) if !assigned =>
    2.39 -          val old_state = state
    2.40 -          state = old_state.accumulate(message)
    2.41 -          if (!(state eq old_state)) forward(static_parent getOrElse this)
    2.42 -
    2.43 -        case Assign =>
    2.44 -          assigned = true  // single assignment
    2.45 -          reply(())
    2.46 -
    2.47 -        case bad => System.err.println("Command accumulator: ignoring bad message " + bad)
    2.48 -      }
    2.49 -    }
    2.50 -  }
    2.51 -
    2.52 -  def consume(message: XML.Tree, forward: Command => Unit)
    2.53 -  {
    2.54 -    accumulator ! Consume(message, forward)
    2.55 -  }
    2.56 -
    2.57 -  def assign_exec(exec_id: Document.Exec_ID): Command =
    2.58 -  {
    2.59 -    val cmd = new Command(exec_id, span, Some(this))
    2.60 -    accumulator !? Assign
    2.61 -    cmd.state = current_state
    2.62 -    cmd
    2.63 -  }
    2.64 -
    2.65 -
    2.66    /* markup */
    2.67  
    2.68 -  lazy val empty_markup = new Markup_Text(Nil, source)
    2.69 -
    2.70    def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
    2.71    {
    2.72      val start = symbol_index.decode(begin)
    2.73      val stop = symbol_index.decode(end)
    2.74      new Markup_Tree(new Markup_Node(start, stop, info), Nil)
    2.75    }
    2.76 +
    2.77 +
    2.78 +  /* accumulated results */
    2.79 +
    2.80 +  def empty_state: Command.State =
    2.81 +    Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source))
    2.82  }
     3.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 13 18:16:50 2010 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 13 18:21:19 2010 +0200
     3.3 @@ -78,12 +78,7 @@
     3.4  
     3.5    /* initial document */
     3.6  
     3.7 -  val init: Document =
     3.8 -  {
     3.9 -    val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
    3.10 -    doc.assign_execs(Nil)
    3.11 -    doc
    3.12 -  }
    3.13 +  val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty))
    3.14  
    3.15  
    3.16  
    3.17 @@ -102,6 +97,7 @@
    3.18      val is_outdated: Boolean
    3.19      def convert(offset: Int): Int
    3.20      def revert(offset: Int): Int
    3.21 +    def lookup_command(id: Command_ID): Option[Command]
    3.22      def state(command: Command): Command.State
    3.23    }
    3.24  
    3.25 @@ -117,7 +113,6 @@
    3.26    {
    3.27      val document: Future[Document] = result.map(_._2)
    3.28      def is_finished: Boolean = prev.is_finished && document.is_finished
    3.29 -    def is_assigned: Boolean = is_finished && document.join.assignment.is_finished
    3.30    }
    3.31  
    3.32  
    3.33 @@ -127,9 +122,6 @@
    3.34    def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit])
    3.35        : (List[Edit[Command]], Document) =
    3.36    {
    3.37 -    require(old_doc.assignment.is_finished)
    3.38 -
    3.39 -
    3.40      /* phase 1: edit individual command source */
    3.41  
    3.42      @tailrec def edit_text(eds: List[Text_Edit],
    3.43 @@ -200,7 +192,6 @@
    3.44      {
    3.45        val doc_edits = new mutable.ListBuffer[Edit[Command]]
    3.46        var nodes = old_doc.nodes
    3.47 -      var former_assignment = old_doc.assignment.join
    3.48  
    3.49        for ((name, text_edits) <- edits) {
    3.50          val commands0 = nodes(name).commands
    3.51 @@ -216,9 +207,107 @@
    3.52  
    3.53          doc_edits += (name -> Some(cmd_edits))
    3.54          nodes += (name -> new Node(commands2))
    3.55 -        former_assignment --= removed_commands
    3.56 +      }
    3.57 +      (doc_edits.toList, new Document(session.create_id(), nodes))
    3.58 +    }
    3.59 +  }
    3.60 +
    3.61 +
    3.62 +
    3.63 +  /** global state -- accumulated prover results **/
    3.64 +
    3.65 +  class Failed_State(state: State) extends Exception
    3.66 +
    3.67 +  object State
    3.68 +  {
    3.69 +    val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
    3.70 +
    3.71 +    class Assignment(former_assignment: Map[Command, Exec_ID])
    3.72 +    {
    3.73 +      @volatile private var tmp_assignment = former_assignment
    3.74 +      private val promise = Future.promise[Map[Command, Exec_ID]]
    3.75 +      def is_finished: Boolean = promise.is_finished
    3.76 +      def join: Map[Command, Exec_ID] = promise.join
    3.77 +      def assign(command_execs: List[(Command, Exec_ID)])
    3.78 +      {
    3.79 +        promise.fulfill(tmp_assignment ++ command_execs)
    3.80 +        tmp_assignment = Map()
    3.81        }
    3.82 -      (doc_edits.toList, new Document(session.create_id(), nodes, former_assignment))
    3.83 +    }
    3.84 +  }
    3.85 +
    3.86 +  case class State(
    3.87 +    val commands: Map[Command_ID, Command.State] = Map(),
    3.88 +    val documents: Map[Version_ID, Document] = Map(),
    3.89 +    val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
    3.90 +    val assignments: Map[Document, State.Assignment] = Map(),
    3.91 +    val disposed: Set[ID] = Set())  // FIXME unused!?
    3.92 +  {
    3.93 +    private def fail[A]: A = throw new Failed_State(this)
    3.94 +
    3.95 +    def define_command(command: Command): State =
    3.96 +    {
    3.97 +      val id = command.id
    3.98 +      if (commands.isDefinedAt(id) || disposed(id)) fail
    3.99 +      copy(commands = commands + (id -> command.empty_state))
   3.100 +    }
   3.101 +
   3.102 +    def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
   3.103 +    {
   3.104 +      val id = document.id
   3.105 +      if (documents.isDefinedAt(id) || disposed(id)) fail
   3.106 +      copy(documents = documents + (id -> document),
   3.107 +        assignments = assignments + (document -> new State.Assignment(former_assignment)))
   3.108 +    }
   3.109 +
   3.110 +    def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
   3.111 +    def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
   3.112 +    def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
   3.113 +    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
   3.114 +    def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
   3.115 +
   3.116 +    def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
   3.117 +      execs.get(id) match {
   3.118 +        case Some((st, docs)) =>
   3.119 +          val new_st = st.accumulate(message)
   3.120 +          (new_st, copy(execs = execs + (id -> (new_st, docs))))
   3.121 +        case None =>
   3.122 +          commands.get(id) match {
   3.123 +            case Some(st) =>
   3.124 +              val new_st = st.accumulate(message)
   3.125 +              (new_st, copy(commands = commands + (id -> new_st)))
   3.126 +            case None => fail
   3.127 +          }
   3.128 +      }
   3.129 +
   3.130 +    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
   3.131 +    {
   3.132 +      val doc = the_document(id)
   3.133 +      val docs = Set(doc)  // FIXME unused (!?)
   3.134 +
   3.135 +      var new_execs = execs
   3.136 +      val assigned_execs =
   3.137 +        for ((cmd_id, exec_id) <- edits) yield {
   3.138 +          val st = the_command(cmd_id)
   3.139 +          if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
   3.140 +          new_execs += (exec_id -> (st, docs))
   3.141 +          (st.command, exec_id)
   3.142 +        }
   3.143 +      the_assignment(doc).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
   3.144 +      copy(execs = new_execs)
   3.145 +    }
   3.146 +
   3.147 +    def is_assigned(document: Document): Boolean =
   3.148 +      assignments.get(document) match {
   3.149 +        case Some(assgn) => assgn.is_finished
   3.150 +        case None => false
   3.151 +      }
   3.152 +
   3.153 +    def command_state(document: Document, command: Command): Command.State =
   3.154 +    {
   3.155 +      val assgn = the_assignment(document)
   3.156 +      require(assgn.is_finished)
   3.157 +      the_exec_state(assgn.join.getOrElse(command, fail))
   3.158      }
   3.159    }
   3.160  }
   3.161 @@ -226,28 +315,5 @@
   3.162  
   3.163  class Document(
   3.164      val id: Document.Version_ID,
   3.165 -    val nodes: Map[String, Document.Node],
   3.166 -    former_assignment: Map[Command, Command])  // FIXME !?
   3.167 -{
   3.168 -  /* command state assignment */
   3.169 -
   3.170 -  val assignment = Future.promise[Map[Command, Command]]
   3.171 -  def await_assignment { assignment.join }
   3.172 -
   3.173 -  @volatile private var tmp_assignment = former_assignment
   3.174 +    val nodes: Map[String, Document.Node])
   3.175  
   3.176 -  def assign_execs(execs: List[(Command, Command)])
   3.177 -  {
   3.178 -    assignment.fulfill(tmp_assignment ++ execs)
   3.179 -    tmp_assignment = Map()
   3.180 -  }
   3.181 -
   3.182 -  def current_state(cmd: Command): Command.State =
   3.183 -  {
   3.184 -    require(assignment.is_finished)
   3.185 -    (assignment.join).get(cmd) match {
   3.186 -      case Some(cmd_state) => cmd_state.current_state
   3.187 -      case None => new Command.State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
   3.188 -    }
   3.189 -  }
   3.190 -}
     4.1 --- a/src/Pure/System/session.scala	Fri Aug 13 18:16:50 2010 +0200
     4.2 +++ b/src/Pure/System/session.scala	Fri Aug 13 18:21:19 2010 +0200
     4.3 @@ -20,16 +20,6 @@
     4.4    case object Global_Settings
     4.5    case object Perspective
     4.6    case class Commands_Changed(set: Set[Command])
     4.7 -
     4.8 -
     4.9 -
    4.10 -  /* managed entities */
    4.11 -
    4.12 -  trait Entity
    4.13 -  {
    4.14 -    val id: Document.ID
    4.15 -    def consume(message: XML.Tree, forward: Command => Unit): Unit
    4.16 -  }
    4.17  }
    4.18  
    4.19  
    4.20 @@ -72,13 +62,9 @@
    4.21    @volatile private var syntax = new Outer_Syntax(system.symbols)
    4.22    def current_syntax: Outer_Syntax = syntax
    4.23  
    4.24 -  @volatile private var entities = Map[Document.ID, Session.Entity]()
    4.25 -  def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id)
    4.26 -  def lookup_command(id: Document.ID): Option[Command] =
    4.27 -    lookup_entity(id) match {
    4.28 -      case Some(cmd: Command) => Some(cmd)
    4.29 -      case _ => None
    4.30 -    }
    4.31 +  @volatile private var global_state = Document.State.init
    4.32 +  private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
    4.33 +  def current_state(): Document.State = global_state
    4.34  
    4.35    private case class Started(timeout: Int, args: List[String])
    4.36    private case object Stop
    4.37 @@ -87,12 +73,6 @@
    4.38  
    4.39      var prover: Isabelle_Process with Isar_Document = null
    4.40  
    4.41 -    def register(entity: Session.Entity) { entities += (entity.id -> entity) }
    4.42 -
    4.43 -    var documents = Map[Document.Version_ID, Document]()
    4.44 -    def register_document(doc: Document) { documents += (doc.id -> doc) }
    4.45 -    register_document(Document.init)
    4.46 -
    4.47  
    4.48      /* document changes */
    4.49  
    4.50 @@ -101,14 +81,21 @@
    4.51      {
    4.52        require(change.is_finished)
    4.53  
    4.54 -      val old_id = change.prev.join.id
    4.55 +      val old_doc = change.prev.join
    4.56        val (node_edits, doc) = change.result.join
    4.57  
    4.58 +      var former_assignment = current_state().the_assignment(old_doc).join
    4.59 +      for {
    4.60 +        (name, Some(cmd_edits)) <- node_edits
    4.61 +        (prev, None) <- cmd_edits
    4.62 +        removed <- old_doc.nodes(name).commands.get_after(prev)
    4.63 +      } former_assignment -= removed
    4.64 +
    4.65        val id_edits =
    4.66          node_edits map {
    4.67            case (name, None) => (name, None)
    4.68            case (name, Some(cmd_edits)) =>
    4.69 -            val chs =
    4.70 +            val ids =
    4.71                cmd_edits map {
    4.72                  case (c1, c2) =>
    4.73                    val id1 = c1.map(_.id)
    4.74 @@ -116,18 +103,18 @@
    4.75                      c2 match {
    4.76                        case None => None
    4.77                        case Some(command) =>
    4.78 -                        if (!lookup_command(command.id).isDefined) {
    4.79 -                          register(command)
    4.80 +                        if (current_state().lookup_command(command.id).isEmpty) {
    4.81 +                          change_state(_.define_command(command))
    4.82                            prover.define_command(command.id, system.symbols.encode(command.source))
    4.83                          }
    4.84                          Some(command.id)
    4.85                      }
    4.86                    (id1, id2)
    4.87                }
    4.88 -            (name -> Some(chs))
    4.89 +            (name -> Some(ids))
    4.90          }
    4.91 -      register_document(doc)
    4.92 -      prover.edit_document(old_id, doc.id, id_edits)
    4.93 +      change_state(_.define_document(doc, former_assignment))
    4.94 +      prover.edit_document(old_doc.id, doc.id, id_edits)
    4.95      }
    4.96      //}}}
    4.97  
    4.98 @@ -144,47 +131,38 @@
    4.99      {
   4.100        raw_results.event(result)
   4.101  
   4.102 -      val target_id: Option[Document.ID] = Position.get_id(result.properties)
   4.103 -      val target: Option[Session.Entity] =
   4.104 -        target_id match {
   4.105 -          case None => None
   4.106 -          case Some(id) => lookup_entity(id)
   4.107 +      Position.get_id(result.properties) match {
   4.108 +        case Some(target_id) =>
   4.109 +          try {
   4.110 +            val (st, state) = global_state.accumulate(target_id, result.message)
   4.111 +            global_state = state
   4.112 +            indicate_command_change(st.command)  // FIXME forward Command.State (!?)
   4.113 +          }
   4.114 +          catch {
   4.115 +            case _: Document.Failed_State =>
   4.116 +              if (result.is_status) {
   4.117 +                result.body match {
   4.118 +                  case List(Isar_Document.Assign(edits)) =>
   4.119 +                    try { change_state(_.assign(target_id, edits)) }
   4.120 +                    catch { case _: Document.Failed_State => bad_result(result) }
   4.121 +                  case _ => bad_result(result)
   4.122 +                }
   4.123 +              }
   4.124 +              else bad_result(result)
   4.125 +          }
   4.126 +        case None =>
   4.127 +          if (result.is_status) {
   4.128 +            result.body match {
   4.129 +              // keyword declarations   // FIXME always global!?
   4.130 +              case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   4.131 +              case List(Keyword.Keyword_Decl(name)) => syntax += name
   4.132 +              case _ => if (!result.is_ready) bad_result(result)
   4.133 +            }
   4.134 +          }
   4.135 +          else if (result.kind == Markup.EXIT) prover = null
   4.136 +          else if (result.is_raw) raw_output.event(result)
   4.137 +          else if (!result.is_system) bad_result(result)  // FIXME syslog for system messages (!?)
   4.138          }
   4.139 -      if (target.isDefined) target.get.consume(result.message, indicate_command_change)
   4.140 -      else if (result.is_status) {
   4.141 -        // global status message
   4.142 -        result.body match {
   4.143 -
   4.144 -          // execution assignment
   4.145 -          case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
   4.146 -            documents.get(target_id.get) match {
   4.147 -              case Some(doc) =>
   4.148 -                val execs =
   4.149 -                  for {
   4.150 -                    Isar_Document.Edit(cmd_id, exec_id) <- edits
   4.151 -                    cmd <- lookup_command(cmd_id)
   4.152 -                  } yield {
   4.153 -                    val st = cmd.assign_exec(exec_id)  // FIXME session state
   4.154 -                    register(st)
   4.155 -                    (cmd, st)
   4.156 -                  }
   4.157 -                doc.assign_execs(execs)  // FIXME session state
   4.158 -              case None => bad_result(result)
   4.159 -            }
   4.160 -
   4.161 -          // keyword declarations
   4.162 -          case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   4.163 -          case List(Keyword.Keyword_Decl(name)) => syntax += name
   4.164 -
   4.165 -          case _ => if (!result.is_ready) bad_result(result)
   4.166 -        }
   4.167 -      }
   4.168 -      else if (result.kind == Markup.EXIT)
   4.169 -        prover = null
   4.170 -      else if (result.is_raw)
   4.171 -        raw_output.event(result)
   4.172 -      else if (!result.is_system)   // FIXME syslog (!?)
   4.173 -        bad_result(result)
   4.174      }
   4.175      //}}}
   4.176  
   4.177 @@ -325,11 +303,14 @@
   4.178  
   4.179      def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
   4.180      {
   4.181 +      val state_snapshot = current_state()
   4.182        val history_snapshot = history
   4.183  
   4.184 -      require(history_snapshot.exists(_.is_assigned))
   4.185 +      val found_stable = history_snapshot.find(change =>
   4.186 +        change.is_finished && state_snapshot.is_assigned(change.document.join))
   4.187 +      require(found_stable.isDefined)
   4.188 +      val stable = found_stable.get
   4.189        val latest = history_snapshot.head
   4.190 -      val stable = history_snapshot.find(_.is_assigned).get
   4.191  
   4.192        val edits =
   4.193          (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
   4.194 @@ -342,7 +323,10 @@
   4.195          val is_outdated = !(pending_edits.isEmpty && latest == stable)
   4.196          def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
   4.197          def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
   4.198 -        def state(command: Command): Command.State = document.current_state(command)
   4.199 +        def lookup_command(id: Document.Command_ID): Option[Command] =
   4.200 +          state_snapshot.lookup_command(id)
   4.201 +        def state(command: Command): Command.State =
   4.202 +          state_snapshot.command_state(document, command)
   4.203        }
   4.204      }
   4.205  
   4.206 @@ -358,7 +342,7 @@
   4.207              val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
   4.208                isabelle.Future.fork {
   4.209                  val old_doc = prev.join
   4.210 -                old_doc.await_assignment
   4.211 +                val former_assignment = current_state().the_assignment(old_doc).join  // FIXME async!?
   4.212                  Document.text_edits(Session.this, old_doc, edits)
   4.213                }
   4.214              val new_change = new Document.Change(prev, edits, result)
     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Fri Aug 13 18:16:50 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Fri Aug 13 18:21:19 2010 +0200
     5.3 @@ -56,8 +56,8 @@
     5.4                    case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
     5.5                      new External_Hyperlink(begin, end, line, ref_file, ref_line)
     5.6                    case Command.RefInfo(_, _, Some(id), Some(offset)) =>
     5.7 -                    Isabelle.session.lookup_entity(id) match {
     5.8 -                      case Some(ref_cmd: Command) =>
     5.9 +                    snapshot.lookup_command(id) match {  // FIXME Command_ID vs. Exec_ID (!??)
    5.10 +                      case Some(ref_cmd) =>
    5.11                          snapshot.node.command_start(ref_cmd) match {
    5.12                            case Some(ref_cmd_start) =>
    5.13                              new Internal_Hyperlink(begin, end, line,