# HG changeset patch
# User wenzelm
# Date 1262097219 -3600
# Node ID d71ecec53c61b675730c818409d79f9a310d6575
# Parent  211ac6c4d4c9e2e4e45240becd6e65595a551b26
tuned;

diff -r 211ac6c4d4c9 -r d71ecec53c61 src/Tools/jEdit/src/proofdocument/proof_document.scala
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 29 15:00:11 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 29 15:33:39 2009 +0100
@@ -9,8 +9,6 @@
 package isabelle.proofdocument
 
 
-import scala.actors.Actor, Actor._
-
 import java.util.regex.Pattern
 
 
@@ -41,8 +39,8 @@
 
 class Proof_Document(
   val id: String,
-  val tokens: Linear_Set[Token],
-  val token_start: Map[Token, Int],
+  val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
+  val token_start: Map[Token, Int],  // FIXME eliminate
   val commands: Linear_Set[Command],
   var states: Map[Command, Command_State])   // FIXME immutable
 {
diff -r 211ac6c4d4c9 -r d71ecec53c61 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Tue Dec 29 15:00:11 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Tue Dec 29 15:33:39 2009 +0100
@@ -44,7 +44,7 @@
             reply(())
           }
 
-        case Stop =>
+        case Stop =>  // FIXME clarify
           if (prover != null)
             prover.kill
           prover_ready = false
@@ -102,7 +102,7 @@
     prover.begin_document(document_0.id, path)   // FIXME fresh document!?!
   }
 
-  def handle_change(change: Change)
+  private def handle_change(change: Change)
   {
     val old = document(change.parent.get.id).get
     val (doc, changes) = old.text_changed(this, change)