# HG changeset patch
# User immler@in.tum.de
# Date 1227890979 -3600
# Node ID 7b5f44553aaf2abc61ca76fee0b57b160bf07c5b
# Parent  fe1afce19eb1d74f5e0efd3b5830cca1aa49f8c5
ugly fine-grained buffer markup

diff -r fe1afce19eb1 -r 7b5f44553aaf src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri Nov 28 15:51:40 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Fri Nov 28 17:49:39 2008 +0100
@@ -31,7 +31,23 @@
         case _ => Color.red
       }
   }
-  
+
+  def chooseColor(status : String) : Color = {
+    //TODO: as properties!
+    status match {
+      case "ident" => new Color(192, 192, 255)
+      case "literal" => new Color(192, 255, 255)
+      case "fixed_decl" => new Color(192, 192, 192)
+      case "prop" => new Color(255, 192 ,255)
+      case "typ" => new Color(192, 192, 128)
+      case "term" => new Color(192, 128, 192)
+      case "method" => new Color(128, 192, 192)
+      case "doc_source" => new Color(128, 128, 192)
+      case "ML_source" => new Color(128, 192, 128)
+      case "local_fact_decl" => new Color(192, 128, 128)
+      case _ => Color.red
+    }
+  }
   def withView(view : TextArea, f : (TheoryView) => Unit) {
     if (view != null && view.getBuffer() != null)
       view.getBuffer().getProperty(ISABELLE_THEORY_PROPERTY) match {
@@ -147,32 +163,44 @@
       textArea.invalidateLineRange(textArea.getFirstPhysicalLine, 
                                    textArea.getLastPhysicalLine)
   }
-  
+
+  def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color){
+      val fm = textArea.getPainter.getFontMetrics
+      val startP = textArea.offsetToXY(begin)
+      val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish)
+                  else { var p = textArea.offsetToXY(finish - 1)
+                         p.x = p.x + fm.charWidth(' ')
+                         p }
+			
+      if (startP != null && stopP != null) {
+        gfx.setColor(color)
+        gfx.fillRect(startP.x, y, stopP.x - startP.x, height)
+      }
+  }
+
   override def paintValidLine(gfx : Graphics2D, screenLine : Int,
                               pl : Int, start : Int, end : Int, y : Int)
   {	
-    var fm = textArea.getPainter().getFontMetrics()
-    var savedColor = gfx.getColor()
+    val fm = textArea.getPainter.getFontMetrics
+    var savedColor = gfx.getColor
     var e = prover.document.getNextCommandContaining(fromCurrent(start))
-    
+
+    //Encolor Phase
     while (e != null && toCurrent(e.start) < end) {
       val begin = Math.max(start, toCurrent(e.start))
-      val startP = textArea.offsetToXY(begin)
-
       val finish = Math.min(end - 1, toCurrent(e.stop))
-      val stopP = if (finish < buffer.getLength()) textArea.offsetToXY(finish) 
-                  else { var p = textArea.offsetToXY(finish - 1) 
-                         p.x = p.x + fm.charWidth(' ') 
-                         p }
-			
-      if (startP != null && stopP != null) {
-        gfx.setColor(chooseColor(e))
-        gfx.fillRect(startP.x, y, stopP.x - startP.x, fm.getHeight())
+      encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e))
+      // paint details of command
+      var dy = 0
+      for(status <- e.statuses){
+        dy += 1
+        val begin = Math.max(start, toCurrent(status.start + e.start))
+        val finish = Math.min(end - 1, toCurrent(status.stop + e.start))
+        encolor(gfx, y + dy, fm.getHeight - dy, begin, finish, chooseColor(status.kind))
       }
-      
       e = e.next
     }
-    
+
     gfx.setColor(savedColor)
   }
 	
diff -r fe1afce19eb1 -r 7b5f44553aaf src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Fri Nov 28 15:51:40 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Fri Nov 28 17:49:39 2008 +0100
@@ -36,12 +36,17 @@
   var phase = Phase.UNPROCESSED
 	
   var results = Nil : List[XML.Tree]
-  
+
+  //offsets relative to first.start!
+  class Status(val kind : String,val start : Int, val stop : Int ) { }
+  var statuses = Nil : List[Status]
+  def statusesxml = XML.Elem("statuses", List(), statuses.map (s => XML.Text(s.kind + ": " + s.start + "-" + s.stop + "\n")))
+
   def idString = java.lang.Long.toString(id, 36)
   def document = XML.document(results match {
                                 case Nil => XML.Elem("message", List(), List())
                                 case List(elem) => elem
-                                case _ => 
+                                case _ =>
                                   XML.Elem("messages", List(), List(results.first,
                                                                     results.last))
                               }, "style")
@@ -49,6 +54,22 @@
     results = results ::: List(tree)
   }
 
+  def addStatus(tree : XML.Tree) {
+    val (markup_info, attr) = tree match { case XML.Elem("message", _, XML.Elem(kind, attr, _) :: _) => (kind, attr)
+                                   case _ => null}
+
+    //process attributes:
+    var markup_begin = -1
+    var markup_end = -1
+    for((n, a) <- attr) {
+      if(n.equals("offset")) markup_begin = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
+      if(n.equals("end_offset")) markup_end = Int.unbox(java.lang.Integer.valueOf(a)) - first.start
+    }
+    if(markup_begin > -1 && markup_end > -1){
+          statuses = new Status(markup_info, markup_begin, markup_end) :: statuses
+    }
+  }
+
   def next = if (last.next != null) last.next.command else null
   def previous = if (first.previous != null) first.previous.command else null
 
diff -r fe1afce19eb1 -r 7b5f44553aaf src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Fri Nov 28 15:51:40 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri Nov 28 17:49:39 2008 +0100
@@ -105,11 +105,11 @@
         fireChange()
               
       case IsabelleProcess.Kind.STATUS =>
-        System.err.println("ST: " + tree)
+        st.addStatus(tree)
         val state = tree match { case Elem("message", _,
                                            Elem (name, _, _) :: _) => name
                                  case _ => null }
-
+        
         if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE) {
           state match {
             case "finished" =>