delayed repainting new phase in buffer and overview;
authorimmler@in.tum.de
Mon Dec 15 16:23:17 2008 +0100 (2008-12-15)
changeset 3440498155c35d252
parent 34403 6c812a3cb170
child 34405 a67a4eaebcff
delayed repainting new phase in buffer and overview;
reverted johannes' handling of removed Commands
src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
src/Tools/jEdit/src/jedit/TheoryView.scala
src/Tools/jEdit/src/prover/Prover.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Dec 10 19:52:35 2008 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Dec 15 16:23:17 2008 +0100
     1.3 @@ -23,12 +23,14 @@
     1.4  package isabelle.jedit
     1.5  
     1.6  import isabelle.prover.Command
     1.7 +import isabelle.utils.Delay
     1.8  
     1.9  import javax.swing._
    1.10  import java.awt.event._
    1.11  import java.awt._
    1.12  import org.gjt.sp.jedit.gui.RolloverButton;
    1.13  import org.gjt.sp.jedit.textarea.JEditTextArea;
    1.14 +import org.gjt.sp.jedit.buffer.JEditBuffer;
    1.15  import org.gjt.sp.jedit._
    1.16  
    1.17  class PhaseOverviewPanel(textarea : JEditTextArea) extends JPanel(new BorderLayout) {
    1.18 @@ -36,7 +38,11 @@
    1.19    private val WIDTH = 10
    1.20  	private val HILITE_HEIGHT = 2
    1.21  
    1.22 -  Plugin.plugin.prover.commandInfo.add(_ => repaint())
    1.23 +  Plugin.plugin.prover.commandInfo.add(cc => {
    1.24 +      System.err.println(cc.command.idString + ": " + cc.command.phase)
    1.25 +      paintCommand(cc.command,textarea.getBuffer, getGraphics)
    1.26 +      System.err.println(cc.command.idString + ": " + cc.command.phase)
    1.27 +    })
    1.28    setRequestFocusEnabled(false);
    1.29  
    1.30    addMouseListener(new MouseAdapter {
    1.31 @@ -69,32 +75,33 @@
    1.32      } else ""
    1.33  	}
    1.34  
    1.35 +  private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
    1.36 +      val line1 = buffer.getLineOfOffset(command.start)
    1.37 +      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
    1.38 +      val y = lineToY(line1)
    1.39 +      val height = lineToY(line2) - y - 1
    1.40 +      val (light, dark) = command.phase match {
    1.41 +        case Command.Phase.UNPROCESSED => (Color.yellow, new Color(128,128,0))
    1.42 +        case Command.Phase.FINISHED => (Color.green, new Color(0, 128, 0))
    1.43 +        case Command.Phase.FAILED => (Color.red, new Color(128,0,0))
    1.44 +      }
    1.45 +
    1.46 +      gfx.setColor(light)
    1.47 +      gfx.fillRect(0, y, getWidth - 1, 1 max height)
    1.48 +      if(height > 2){
    1.49 +        gfx.setColor(dark)
    1.50 +        gfx.drawRect(0, y, getWidth - 1, height)
    1.51 +      }
    1.52 +
    1.53 +  }
    1.54 +
    1.55  	override def paintComponent(gfx : Graphics) {
    1.56  		super.paintComponent(gfx)
    1.57  
    1.58 -
    1.59  		val buffer = textarea.getBuffer
    1.60  
    1.61 -		val line_count = buffer.getLineCount
    1.62 -
    1.63 -    for(command <- Plugin.plugin.prover.document.commands) {
    1.64 -      val line1 = buffer.getLineOfOffset(command.start)
    1.65 -      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
    1.66 -      if(line1 < 0 || line2 > line_count){
    1.67 -        System.err.println("invalid line numbers: " + line1 + " - " + line2)
    1.68 -      } else {
    1.69 -        val y1 = lineToY(line1)
    1.70 -        val y2 = lineToY(line2) - 1
    1.71 -        val linelength = buffer.getLineLength(line1)
    1.72 -        val color = command.phase match {
    1.73 -          case Command.Phase.UNPROCESSED => Color.yellow
    1.74 -          case Command.Phase.FINISHED => Color.green
    1.75 -          case Command.Phase.FAILED => Color.red
    1.76 -        }
    1.77 -				gfx.setColor(color)
    1.78 -				gfx.fillRect(0, y1, getWidth, 1 max y2 - y1)
    1.79 -			}
    1.80 -		}
    1.81 +    for(c <- Plugin.plugin.prover.document.commands)
    1.82 +      paintCommand(c, buffer, gfx)
    1.83  	}
    1.84  
    1.85  	override def getPreferredSize : Dimension =
     2.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Dec 10 19:52:35 2008 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Dec 15 16:23:17 2008 +0100
     2.3 @@ -94,10 +94,10 @@
     2.4    {
     2.5      buffer.addBufferListener(this)
     2.6      buffer.setProperty(ISABELLE_THEORY_PROPERTY, this)
     2.7 +
     2.8 +    val repaint_delay = new isabelle.utils.Delay(100, () => repaintAll())
     2.9 +    prover.commandInfo.add(_ => repaint_delay.delay())
    2.10      
    2.11 -    prover.commandInfo.add(e => repaint(e.command))
    2.12 -    prover.commandInfo.add(e => repaintAll())
    2.13 -	
    2.14      Plugin.plugin.viewFontChanged.add(font => updateFont())
    2.15      
    2.16      colTimer.stop
    2.17 @@ -157,7 +157,7 @@
    2.18    
    2.19    def repaint(cmd : Command)
    2.20    {
    2.21 -    var ph = cmd.phase
    2.22 +    val ph = cmd.phase
    2.23      if (textArea != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
    2.24        var start = textArea.getLineOfOffset(toCurrent(cmd.start))
    2.25        var stop = textArea.getLineOfOffset(toCurrent(cmd.stop) - 1)
     3.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Dec 10 19:52:35 2008 +0100
     3.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Dec 15 16:23:17 2008 +0100
     3.3 @@ -61,15 +61,18 @@
     3.4          }
     3.5          else {
     3.6            val tree = parse_failsafe(converter.decode(r.result))
     3.7 +          if (st == null || (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE))
     3.8            tree match {
     3.9              //handle all kinds of status messages here
    3.10              case Elem("message", List(("class","status")), elems) =>
    3.11                elems map (elem => elem match{
    3.12 +
    3.13                    // catch command_start and keyword declarations
    3.14                    case Elem("command_decl", List(("name", name), ("kind", _)), _) =>
    3.15                      command_decls.addEntry(name)
    3.16                    case Elem("keyword_decl", List(("name", name)), _) =>
    3.17                      keyword_decls.addEntry(name)
    3.18 +
    3.19                    // expecting markups here
    3.20                    case Elem(kind, List(("offset", offset),
    3.21                                         ("end_offset", end_offset),
    3.22 @@ -83,6 +86,7 @@
    3.23                        // inner syntax: id from props
    3.24                        else st
    3.25                      command.root_node.insert(command.node_from(kind, begin, end))
    3.26 +
    3.27                    // Phase changed
    3.28                    case Elem("finished", _, _) =>
    3.29                      st.phase = Phase.FINISHED
    3.30 @@ -94,14 +98,12 @@
    3.31                      st.phase = Phase.FAILED
    3.32                      fireChange(st)
    3.33                    case Elem("removed", _, _) =>
    3.34 -                    // TODO: never lose information on command + id ??
    3.35 -                    //document.prover.commands.removeKey(st.idString)
    3.36 +                    document.prover.commands.removeKey(st.idString)
    3.37                      st.phase = Phase.REMOVED
    3.38                      fireChange(st)
    3.39                    case _ =>
    3.40                  }) 
    3.41              case _ =>
    3.42 -              //TODO
    3.43                if (st != null)
    3.44                handleResult(st, r, tree)
    3.45            }