--- a/src/Tools/jEdit/src/proofdocument/session.scala Mon Jan 04 00:13:09 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala Mon Jan 04 19:08:10 2010 +0100
@@ -55,8 +55,12 @@
@volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
+ def lookup_command(id: Session.Entity_ID): Option[Command] =
+ lookup_entity(id) match {
+ case Some(cmd: Command) => Some(cmd)
+ case _ => None
+ }
- private case class Register(entity: Session.Entity)
private case class Start(timeout: Int, args: List[String])
private case object Stop
private case class Begin_Document(path: String)
@@ -67,6 +71,9 @@
def register(entity: Session.Entity) { entities += (entity.id -> entity) }
+ var documents = Map[Isar_Document.Document_ID, Document]()
+ def register_document(doc: Document) { documents += (doc.id -> doc) }
+
/* document changes */
@@ -80,13 +87,15 @@
(c1.map(_.id).getOrElse(""),
c2 match {
case None => None
- case Some(command) => // FIXME register/define only commands unknown to prover
- register(command)
- prover.define_command(command.id, system.symbols.encode(command.content))
+ case Some(command) =>
+ if (!lookup_command(command.id).isDefined) {
+ register(command)
+ prover.define_command(command.id, system.symbols.encode(command.content))
+ }
Some(command.id)
})
}
- register(doc)
+ register_document(doc)
prover.edit_document(change.parent.get.id, doc.id, id_changes)
}
@@ -97,16 +106,35 @@
{
raw_results.event(result)
+ val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
val target: Option[Session.Entity] =
- Position.get_id(result.props) match {
+ target_id match {
case None => None
- case Some(id) => entities.get(id)
+ case Some(id) => lookup_entity(id)
}
if (target.isDefined) target.get.consume(this, result.message)
else if (result.kind == Isabelle_Process.Kind.STATUS) {
// global status message
for (elem <- result.body) {
elem match {
+ // document state assigment
+ case XML.Elem(Markup.ASSIGN, _, edits) if target_id.isDefined =>
+ documents.get(target_id.get) match {
+ case Some(doc) =>
+ val states =
+ for {
+ XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+ <- edits
+ cmd <- lookup_command(cmd_id)
+ } yield {
+ val st = cmd.assign_state(state_id)
+ register(st)
+ (cmd, st)
+ }
+ doc.assign_states(states)
+ case None =>
+ }
+
// command and keyword declarations
case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
syntax += (name, kind)
@@ -167,10 +195,6 @@
loop {
react {
- case Register(entity: Session.Entity) =>
- register(entity)
- reply(())
-
case Start(timeout, args) =>
if (prover == null) {
prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
@@ -190,7 +214,7 @@
case Begin_Document(path: String) if prover != null =>
val id = create_id()
val doc = Document.empty(id)
- register(doc)
+ register_document(doc)
prover.begin_document(id, path)
reply(doc)
@@ -209,8 +233,6 @@
/* main methods */
- def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
-
def start(timeout: Int, args: List[String]): Option[String] =
(session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]