1.1 --- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Wed Dec 30 20:26:08 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Wed Dec 30 21:34:33 2009 +0100
     1.3 @@ -9,22 +9,24 @@
     1.4  package isabelle.proofdocument
     1.5  
     1.6  
     1.7 +import scala.actors.Actor._
     1.8 +
     1.9  import java.util.regex.Pattern
    1.10  
    1.11  
    1.12  object Proof_Document
    1.13  {
    1.14    // Be careful when changing this regex. Not only must it handle the
    1.15 -  // spurious end of a token but also:  
    1.16 +  // spurious end of a token but also:
    1.17    // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
    1.18    // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
    1.19 -  
    1.20 -  val token_pattern = 
    1.21 +
    1.22 +  val token_pattern =
    1.23      Pattern.compile(
    1.24        "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
    1.25        "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
    1.26 -      "(\\?'?|')[A-Za-z_0-9.]*|" + 
    1.27 -      "[A-Za-z_0-9.]+|" + 
    1.28 +      "(\\?'?|')[A-Za-z_0-9.]*|" +
    1.29 +      "[A-Za-z_0-9.]+|" +
    1.30        "[!#$%&*+-/<=>?@^_|~]+|" +
    1.31        "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
    1.32        "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
    1.33 @@ -38,18 +40,51 @@
    1.34  
    1.35  
    1.36  class Proof_Document(
    1.37 -  val id: Isar_Document.Document_ID,
    1.38 -  val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
    1.39 -  val token_start: Map[Token, Int],  // FIXME eliminate
    1.40 -  val commands: Linear_Set[Command],
    1.41 -  var states: Map[Command, Command])   // FIXME immutable, eliminate!?
    1.42 +    val id: Isar_Document.Document_ID,
    1.43 +    val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
    1.44 +    val token_start: Map[Token, Int],  // FIXME eliminate
    1.45 +    val commands: Linear_Set[Command],
    1.46 +    var states: Map[Command, Command])   // FIXME immutable, eliminate!?
    1.47 +  extends Session.Entity
    1.48  {
    1.49    import Proof_Document.StructureChange
    1.50  
    1.51    def content = Token.string_from_tokens(Nil ++ tokens, token_start)
    1.52  
    1.53  
    1.54 -  
    1.55 +  /* accumulated messages */
    1.56 +
    1.57 +  private val accumulator = actor {
    1.58 +    loop {
    1.59 +      react {
    1.60 +        case (session: Session, message: XML.Tree) =>
    1.61 +          message match {
    1.62 +            case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
    1.63 +              for {
    1.64 +                XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
    1.65 +                  <- elems
    1.66 +              } {
    1.67 +                session.lookup_entity(cmd_id) match {
    1.68 +                  case Some(cmd: Command) =>
    1.69 +                    val state = cmd.finish_static(state_id)
    1.70 +                    session.register_entity(state)
    1.71 +                    states += (cmd -> state)  // FIXME !?
    1.72 +                    session.command_change.event(cmd)   // FIXME really!?
    1.73 +                  case _ =>
    1.74 +                }
    1.75 +              }
    1.76 +            case _ =>
    1.77 +          }
    1.78 +
    1.79 +        case bad => System.err.println("document accumulator: ignoring bad message " + bad)
    1.80 +      }
    1.81 +    }
    1.82 +  }
    1.83 +
    1.84 +  def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) }
    1.85 +
    1.86 +
    1.87 +
    1.88    /** token view **/
    1.89  
    1.90    def text_changed(session: Session, change: Change): (Proof_Document, StructureChange) =
    1.91 @@ -101,7 +136,7 @@
    1.92  
    1.93      val ins = new Token(change.added, Token.Kind.OTHER)
    1.94      start += (ins -> change.start)
    1.95 -    
    1.96 +
    1.97      var invalid_tokens = split_begin ::: ins :: split_end ::: end
    1.98      var new_tokens: List[Token] = Nil
    1.99      var old_suffix: List[Token] = Nil
   1.100 @@ -140,7 +175,7 @@
   1.101        old_suffix.firstOption, new_token_list, start)
   1.102    }
   1.103  
   1.104 -  
   1.105 +
   1.106    /** command view **/
   1.107  
   1.108    private def token_changed(

     2.1 --- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 20:26:08 2009 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 21:34:33 2009 +0100
     2.3 @@ -55,10 +55,12 @@
     2.4    @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
     2.5    def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
     2.6  
     2.7 +  // FIXME eliminate
     2.8    @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]()
     2.9    def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id)
    2.10  
    2.11  
    2.12 +
    2.13    /** main actor **/
    2.14  
    2.15    private case class Register(entity: Session.Entity)
    2.16 @@ -92,6 +94,7 @@
    2.17                  Some(command.id)
    2.18              })
    2.19        }
    2.20 +      register(doc)
    2.21        documents += (doc.id -> doc)
    2.22        prover.edit_document(old.id, doc.id, id_changes)
    2.23  
    2.24 @@ -112,29 +115,9 @@
    2.25          }
    2.26        if (target.isDefined) target.get.consume(this, result.message)
    2.27        else if (result.kind == Isabelle_Process.Kind.STATUS) {
    2.28 -        //{{{ global status message
    2.29 +        // global status message
    2.30          for (elem <- result.body) {
    2.31            elem match {
    2.32 -            // document edits
    2.33 -            case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
    2.34 -              document(doc_id) match {
    2.35 -                case None =>  // FIXME clarify
    2.36 -                case Some(doc) =>
    2.37 -                  for {
    2.38 -                    XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
    2.39 -                    <- edits }
    2.40 -                  {
    2.41 -                    entities.get(cmd_id) match {
    2.42 -                      case Some(cmd: Command) =>
    2.43 -                        val state = cmd.finish_static(state_id)
    2.44 -                        register(state)
    2.45 -                        doc.states += (cmd -> state)  // FIXME !?
    2.46 -                        command_change.event(cmd)   // FIXME really!?
    2.47 -                      case _ =>
    2.48 -                    }
    2.49 -                  }
    2.50 -              }
    2.51 -
    2.52              // command and keyword declarations
    2.53              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
    2.54                outer_syntax += (name, kind)
    2.55 @@ -147,7 +130,6 @@
    2.56            case _ =>
    2.57            }
    2.58          }
    2.59 -        //}}}
    2.60        }
    2.61        else if (result.kind == Isabelle_Process.Kind.EXIT)
    2.62          prover = null
    2.63 @@ -178,6 +160,7 @@
    2.64          case Begin_Document(path: String) if prover_ready =>
    2.65            val id = create_id()
    2.66            val doc = Proof_Document.empty(id)
    2.67 +          register(doc)
    2.68            documents += (id -> doc)
    2.69            prover.begin_document(id, path)
    2.70            reply(doc)