# HG changeset patch
# User immler@in.tum.de
# Date 1247052583 -7200
# Node ID 70759ca6bb87c7fa61e530a56ee834199921b44e
# Parent  8213a350fd452f02b338c5d41c17d4c28a5f66c0
activation

diff -r 8213a350fd45 -r 70759ca6bb87 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Wed Jul 08 13:29:43 2009 +0200
@@ -40,13 +40,6 @@
 
     theory_view = new TheoryView(view.getTextArea, prover)
     prover.set_document(theory_view.change_receiver, buffer.getName)
-    theory_view.activate
-    val MAX = TheoryView.MAX_CHANGE_LENGTH
-    for (i <- 0 to buffer.getLength / MAX) {
-      prover ! new isabelle.proofdocument.Text.Change(
-        Isabelle.system.id(), i * MAX,
-        buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), "")
-    }
 
     // register output-view
     prover.output_info += (text =>
@@ -82,7 +75,6 @@
 
   def deactivate
   {
-    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
     theory_view.deactivate
     prover.stop
   }
diff -r 8213a350fd45 -r 70759ca6bb87 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Jul 08 13:29:43 2009 +0200
@@ -12,7 +12,7 @@
 import scala.actors.Actor._
 
 import isabelle.proofdocument.Text
-import isabelle.prover.{Prover, Command}
+import isabelle.prover.{Prover, ProverEvents, Command}
 
 import java.awt.Graphics2D
 import java.awt.event.{ActionEvent, ActionListener}
@@ -22,7 +22,7 @@
 
 import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.SyntaxStyle
+import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
 
 
 object TheoryView
@@ -51,7 +51,6 @@
   
   private val buffer = text_area.getBuffer
   private val prover = Isabelle.prover_setup(buffer).get.prover
-  buffer.addBufferListener(this)
 
 
   private var col: Text.Change = null
@@ -84,9 +83,19 @@
     text_area.addLeftOfScrollBar(phase_overview)
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
     buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
+    buffer.addBufferListener(this)
+
+    val MAX = TheoryView.MAX_CHANGE_LENGTH
+    for (i <- 0 to buffer.getLength / MAX) {
+      prover ! new isabelle.proofdocument.Text.Change(
+        Isabelle.system.id(), i * MAX,
+        buffer.getText(i * MAX, MAX min buffer.getLength - i * MAX), "")
+    }
   }
 
   def deactivate() {
+    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
+    buffer.removeBufferListener(this)
     text_area.getPainter.removeExtension(this)
     text_area.removeLeftOfScrollBar(phase_overview)
     text_area.removeCaretListener(selected_state_controller)
@@ -101,10 +110,13 @@
   val change_receiver = actor {
     loop {
       react {
-        case _ =>
+        case ProverEvents.Activate =>
+          activate()
+        case c: Command =>
           update_delay()
           repaint_delay()
           phase_overview.repaint_delay()
+        case x => System.err.println("warning: change_receiver ignored " + x)
       }
     }
   }
diff -r 8213a350fd45 -r 70759ca6bb87 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Jul 08 13:29:43 2009 +0200
@@ -40,7 +40,7 @@
 
  val empty =
   new ProofDocument(isabelle.jedit.Isabelle.system.id(),
-    LinearSet(), Map(), LinearSet(), false, _ => false)
+    LinearSet(), Map(), LinearSet(), _ => false)
 
 }
 
@@ -49,19 +49,11 @@
   val tokens: LinearSet[Token],
   val token_start: Map[Token, Int],
   val commands: LinearSet[Command],
-  val active: Boolean,
   is_command_keyword: String => Boolean)
 {
 
-  def mark_active: ProofDocument =
-    new ProofDocument(id, tokens, token_start, commands, true, is_command_keyword)
-  def activate: (ProofDocument, StructureChange) = {
-    val (doc, change) =
-      text_changed(new Text.Change(isabelle.jedit.Isabelle.system.id(), 0, content, content))
-    return (doc.mark_active, change)
-  }
   def set_command_keyword(f: String => Boolean): ProofDocument =
-    new ProofDocument(isabelle.jedit.Isabelle.system.id(), tokens, token_start, commands, active, f)
+    new ProofDocument(id, tokens, token_start, commands, f)
 
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
   /** token view **/
@@ -222,7 +214,7 @@
 
     val doc =
       new ProofDocument(new_id, new_tokenset, new_token_start,
-        new_commandset, active, is_command_keyword)
+        new_commandset, is_command_keyword)
     return (doc, change)
   }
 
diff -r 8213a350fd45 -r 70759ca6bb87 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Jul 08 13:29:42 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Jul 08 13:29:43 2009 +0200
@@ -47,7 +47,8 @@
     mutable.SynchronizedMap[IsarDocument.State_ID, Command]
   private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] with
     mutable.SynchronizedMap[IsarDocument.Command_ID, Command]
-  private var document_versions = List(ProofDocument.empty)
+  private var document_versions =
+    List(ProofDocument.empty.set_command_keyword(command_decls.contains))
   private val document_id0 = ProofDocument.empty.id
 
   def command(id: IsarDocument.Command_ID): Option[Command] = commands.get(id)
@@ -85,7 +86,6 @@
 
   /* event handling */
 
-  val activated = new EventBus[Unit]
   val output_info = new EventBus[String]
   var change_receiver: Actor = null
   
@@ -138,7 +138,7 @@
                   case XML.Elem(Markup.READY, _, _)
                   if !initialized =>
                     initialized = true
-                    Swing_Thread.now { this ! ProverEvents.Activate }
+                    change_receiver ! ProverEvents.Activate
 
                   // document edits
                   case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
@@ -230,18 +230,6 @@
     import ProverEvents._
     loop {
       react {
-        case Activate => {
-            val old = document
-            val (doc, structure_change) = old.activate
-            document_versions ::= doc
-            edit_document(old.id, doc.id, structure_change)
-        }
-        case SetIsCommandKeyword(f) => {
-            val old = document
-            val doc = old.set_command_keyword(f)
-            document_versions ::= doc
-            edit_document(old.id, doc.id, StructureChange(None, Nil, Nil))
-        }
         case change: Text.Change => {
             val old = document
             val (doc, structure_change) = old.text_changed(change)
@@ -258,7 +246,6 @@
   
   def set_document(change_receiver: Actor, path: String) {
     this.change_receiver = change_receiver
-    this ! ProverEvents.SetIsCommandKeyword(command_decls.contains)
     process.begin_document(document_id0, path)
   }