# HG changeset patch
# User immler@in.tum.de
# Date 1229354597 -3600
# Node ID 98155c35d252a24d4cb080b6f441e43f581cdbef
# Parent  6c812a3cb170e99855790cb61df7ac012959793d
delayed repainting new phase in buffer and overview;
reverted johannes' handling of removed Commands

diff -r 6c812a3cb170 -r 98155c35d252 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Dec 10 19:52:35 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Dec 15 16:23:17 2008 +0100
@@ -23,12 +23,14 @@
 package isabelle.jedit
 
 import isabelle.prover.Command
+import isabelle.utils.Delay
 
 import javax.swing._
 import java.awt.event._
 import java.awt._
 import org.gjt.sp.jedit.gui.RolloverButton;
 import org.gjt.sp.jedit.textarea.JEditTextArea;
+import org.gjt.sp.jedit.buffer.JEditBuffer;
 import org.gjt.sp.jedit._
 
 class PhaseOverviewPanel(textarea : JEditTextArea) extends JPanel(new BorderLayout) {
@@ -36,7 +38,11 @@
   private val WIDTH = 10
 	private val HILITE_HEIGHT = 2
 
-  Plugin.plugin.prover.commandInfo.add(_ => repaint())
+  Plugin.plugin.prover.commandInfo.add(cc => {
+      System.err.println(cc.command.idString + ": " + cc.command.phase)
+      paintCommand(cc.command,textarea.getBuffer, getGraphics)
+      System.err.println(cc.command.idString + ": " + cc.command.phase)
+    })
   setRequestFocusEnabled(false);
 
   addMouseListener(new MouseAdapter {
@@ -69,32 +75,33 @@
     } else ""
 	}
 
+  private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
+      val line1 = buffer.getLineOfOffset(command.start)
+      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
+      val y = lineToY(line1)
+      val height = lineToY(line2) - y - 1
+      val (light, dark) = command.phase match {
+        case Command.Phase.UNPROCESSED => (Color.yellow, new Color(128,128,0))
+        case Command.Phase.FINISHED => (Color.green, new Color(0, 128, 0))
+        case Command.Phase.FAILED => (Color.red, new Color(128,0,0))
+      }
+
+      gfx.setColor(light)
+      gfx.fillRect(0, y, getWidth - 1, 1 max height)
+      if(height > 2){
+        gfx.setColor(dark)
+        gfx.drawRect(0, y, getWidth - 1, height)
+      }
+
+  }
+
 	override def paintComponent(gfx : Graphics) {
 		super.paintComponent(gfx)
 
-
 		val buffer = textarea.getBuffer
 
-		val line_count = buffer.getLineCount
-
-    for(command <- Plugin.plugin.prover.document.commands) {
-      val line1 = buffer.getLineOfOffset(command.start)
-      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
-      if(line1 < 0 || line2 > line_count){
-        System.err.println("invalid line numbers: " + line1 + " - " + line2)
-      } else {
-        val y1 = lineToY(line1)
-        val y2 = lineToY(line2) - 1
-        val linelength = buffer.getLineLength(line1)
-        val color = command.phase match {
-          case Command.Phase.UNPROCESSED => Color.yellow
-          case Command.Phase.FINISHED => Color.green
-          case Command.Phase.FAILED => Color.red
-        }
-				gfx.setColor(color)
-				gfx.fillRect(0, y1, getWidth, 1 max y2 - y1)
-			}
-		}
+    for(c <- Plugin.plugin.prover.document.commands)
+      paintCommand(c, buffer, gfx)
 	}
 
 	override def getPreferredSize : Dimension =
diff -r 6c812a3cb170 -r 98155c35d252 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Dec 10 19:52:35 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Dec 15 16:23:17 2008 +0100
@@ -94,10 +94,10 @@
   {
     buffer.addBufferListener(this)
     buffer.setProperty(ISABELLE_THEORY_PROPERTY, this)
+
+    val repaint_delay = new isabelle.utils.Delay(100, () => repaintAll())
+    prover.commandInfo.add(_ => repaint_delay.delay())
     
-    prover.commandInfo.add(e => repaint(e.command))
-    prover.commandInfo.add(e => repaintAll())
-	
     Plugin.plugin.viewFontChanged.add(font => updateFont())
     
     colTimer.stop
@@ -157,7 +157,7 @@
   
   def repaint(cmd : Command)
   {
-    var ph = cmd.phase
+    val ph = cmd.phase
     if (textArea != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
       var start = textArea.getLineOfOffset(toCurrent(cmd.start))
       var stop = textArea.getLineOfOffset(toCurrent(cmd.stop) - 1)
diff -r 6c812a3cb170 -r 98155c35d252 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Dec 10 19:52:35 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Dec 15 16:23:17 2008 +0100
@@ -61,15 +61,18 @@
         }
         else {
           val tree = parse_failsafe(converter.decode(r.result))
+          if (st == null || (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE))
           tree match {
             //handle all kinds of status messages here
             case Elem("message", List(("class","status")), elems) =>
               elems map (elem => elem match{
+
                   // catch command_start and keyword declarations
                   case Elem("command_decl", List(("name", name), ("kind", _)), _) =>
                     command_decls.addEntry(name)
                   case Elem("keyword_decl", List(("name", name)), _) =>
                     keyword_decls.addEntry(name)
+
                   // expecting markups here
                   case Elem(kind, List(("offset", offset),
                                        ("end_offset", end_offset),
@@ -83,6 +86,7 @@
                       // inner syntax: id from props
                       else st
                     command.root_node.insert(command.node_from(kind, begin, end))
+
                   // Phase changed
                   case Elem("finished", _, _) =>
                     st.phase = Phase.FINISHED
@@ -94,14 +98,12 @@
                     st.phase = Phase.FAILED
                     fireChange(st)
                   case Elem("removed", _, _) =>
-                    // TODO: never lose information on command + id ??
-                    //document.prover.commands.removeKey(st.idString)
+                    document.prover.commands.removeKey(st.idString)
                     st.phase = Phase.REMOVED
                     fireChange(st)
                   case _ =>
                 }) 
             case _ =>
-              //TODO
               if (st != null)
               handleResult(st, r, tree)
           }