# HG changeset patch
# User immler@in.tum.de
# Date 1228935075 -3600
# Node ID bd8d70cd9baff77b4fd4d6c620aad70012a4e7a5
# Parent  44241a37b74a3450c8e5bfc5261762851826b29e
information on command-phase left of scrollbar

diff -r 44241a37b74a -r bd8d70cd9baf src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Dec 10 14:45:04 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Dec 10 19:51:15 2008 +0100
@@ -14,7 +14,7 @@
 import java.awt.Color;
 
 import org.gjt.sp.jedit.buffer.{ BufferListener, JEditBuffer }
-import org.gjt.sp.jedit.textarea.{ TextArea, TextAreaExtension, TextAreaPainter }
+import org.gjt.sp.jedit.textarea.{ JEditTextArea, TextAreaExtension, TextAreaPainter }
 import org.gjt.sp.jedit.syntax.SyntaxStyle
 
 object TheoryView {
@@ -58,7 +58,8 @@
       case _ => Color.white
     }
   }
-  def withView(view : TextArea, f : (TheoryView) => Unit) {
+  
+  def withView(view : JEditTextArea, f : (TheoryView) => Unit) {
     if (view != null && view.getBuffer() != null)
       view.getBuffer().getProperty(ISABELLE_THEORY_PROPERTY) match {
         case null => null
@@ -67,11 +68,11 @@
       }
   }
 	
-  def activateTextArea(textArea : TextArea) {
+  def activateTextArea(textArea : JEditTextArea) {
     withView(textArea, _.activate(textArea))
   }	
 	
-  def deactivateTextArea(textArea : TextArea) {
+  def deactivateTextArea(textArea : JEditTextArea) {
     withView(textArea, _.deactivate(textArea))
   }
 }
@@ -81,7 +82,7 @@
   import TheoryView._
   import Text.Changed
   
-  var textArea : TextArea = null;
+  var textArea : JEditTextArea = null;
   var col : Changed = null;
   
   val colTimer = new Timer(300, new ActionListener() {
@@ -103,10 +104,10 @@
     colTimer.setRepeats(true)
   }
 
-  def activate(area : TextArea) {
+  def activate(area : JEditTextArea) {
     textArea = area
     textArea.addCaretListener(selectedStateController)
-    
+    textArea.addLeftOfScrollBar(new PhaseOverviewPanel(textArea))
     val painter = textArea.getPainter()
     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
     updateFont()
@@ -127,7 +128,7 @@
     }
   }
   
-  def deactivate(area : TextArea) {
+  def deactivate(area : JEditTextArea) {
     textArea.getPainter().removeExtension(this)
     textArea.removeCaretListener(selectedStateController)
     textArea = null
diff -r 44241a37b74a -r bd8d70cd9baf src/Tools/jEdit/src/prover/MarkupNode.scala
--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed Dec 10 14:45:04 2008 +0100
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed Dec 10 19:51:15 2008 +0100
@@ -66,7 +66,12 @@
   private def remove(nodes : List[MarkupNode]) {
     children_cell = children diff nodes
 
-    for(node <- nodes) swing_node remove node.swing_node
+      for(node <- nodes) try {
+        swing_node remove node.swing_node
+      } catch { case e : IllegalArgumentException =>
+        System.err.println(e.toString)
+        case e => throw e
+      }
   }
 
   def dfs : List[MarkupNode] = {