# HG changeset patch
# User wenzelm
# Date 1230486038 -3600
# Node ID 5c79f97ec1d1d34a3a4c52850dc5bbf8f3f5a58b
# Parent  61ffe9a35f1d4d2201712fd619eae1f09ef24a47
superficial tuning;
improved comments and sectioning;

diff -r 61ffe9a35f1d -r 5c79f97ec1d1 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Dec 28 16:40:29 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Dec 28 18:40:38 2008 +0100
@@ -7,26 +7,26 @@
 
 package isabelle.jedit
 
+
 import isabelle.utils.EventSource
-
 import isabelle.proofdocument.Text
-
-import isabelle.prover.{ Prover, Command, CommandChangeInfo }
+import isabelle.prover.{Prover, Command, CommandChangeInfo}
 import isabelle.prover.Command.Phase
 
 import javax.swing.Timer
-import javax.swing.event.{ CaretListener, CaretEvent }
+import javax.swing.event.{CaretListener, CaretEvent}
 import java.awt.Graphics2D
-import java.awt.event.{ ActionEvent, ActionListener }
-import java.awt.Color;
+import java.awt.event.{ActionEvent, ActionListener}
+import java.awt.Color
 
-import org.gjt.sp.jedit.buffer.{ BufferListener, JEditBuffer }
-import org.gjt.sp.jedit.textarea.{ JEditTextArea, TextAreaExtension, TextAreaPainter }
+import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
 import org.gjt.sp.jedit.syntax.SyntaxStyle
 
+
 object TheoryView {
 
-  def chooseColor(state : Command) : Color = {
+  def choose_color(state: Command): Color = {
     if (state == null)
       Color.red
     else
@@ -38,9 +38,9 @@
       }
   }
 
-  def chooseColor(status : String): Color = {
-    //TODO: as properties!
-    status match {
+  def choose_color(markup: String): Color = {
+    // TODO: as properties
+    markup match {
       // logical entities
       case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
         | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
@@ -51,7 +51,7 @@
       case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
         | Markup.INNER_COMMENT => new Color(255, 128, 128)
       case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
-        | Markup.ATTRIBUTE | Markup.METHOD  => Color.yellow
+        | Markup.ATTRIBUTE | Markup.METHOD => Color.yellow
       // embedded source text
       case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
         | Markup.DOC_ANTIQ => new Color(0, 192, 0)
@@ -68,204 +68,227 @@
   }
 }
 
-class TheoryView (text_area : JEditTextArea)
+
+class TheoryView (text_area: JEditTextArea)
     extends TextAreaExtension with Text with BufferListener {
-  import TheoryView._
-  import Text.Changed
 
-  var col : Changed = null
-
-  val buffer = text_area.getBuffer
+  private val buffer = text_area.getBuffer
   buffer.addBufferListener(this)
-  
-  val colTimer = new Timer(300, new ActionListener() {
-    override def actionPerformed(e : ActionEvent) { commit() }
+
+
+  private var col: Text.Changed = null
+
+  private val col_timer = new Timer(300, new ActionListener() {
+    override def actionPerformed(e: ActionEvent) = commit()
   })
-  
-  val changesSource = new EventSource[Changed]
-  val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
-
-    val repaint_delay = new isabelle.utils.Delay(100, () => repaintAll())
-    Isabelle.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
-    Isabelle.plugin.font_changed.add(font => updateFont())
 
-    colTimer.stop
-    colTimer.setRepeats(true)
+  col_timer.stop
+  col_timer.setRepeats(true)
+
+
+  private val changes_source = new EventSource[Text.Changed]
+  private val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
+
 
-  def activate() {
-    text_area.addCaretListener(selectedStateController)
-    phase_overview.textarea = text_area
-    text_area.addLeftOfScrollBar(phase_overview)
-    val painter = text_area.getPainter()
-    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
-    updateFont()
-  }
-  
-  private def updateFont() {
+  /* activation */
+
+  Isabelle.plugin.font_changed.add(font => update_font())
+
+  private def update_font() = {
     if (text_area != null) {
-      val painter = text_area.getPainter()
       if (Isabelle.plugin.font != null) {
+        val painter = text_area.getPainter
         painter.setStyles(painter.getStyles.map(style =>
-          new SyntaxStyle(style.getForegroundColor, 
-                          style.getBackgroundColor, 
-                          Isabelle.plugin.font)
+          new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, Isabelle.plugin.font)
         ))
         painter.setFont(Isabelle.plugin.font)
-        repaintAll()
+        repaint_all()
       }
     }
   }
-  
-  def deactivate() {
-    text_area.getPainter().removeExtension(this)
-    text_area.removeCaretListener(selectedStateController)
-    text_area.removeLeftOfScrollBar(phase_overview)
-  }
-  
-  val selectedStateController = new CaretListener() {
-    override def caretUpdate(e : CaretEvent) {
-      val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot())
-      if (cmd != null && cmd.start <= e.getDot() && 
-            Isabelle.prover_setup(buffer).selectedState != cmd)
+
+  private val selected_state_controller = new CaretListener {
+    override def caretUpdate(e: CaretEvent) = {
+      val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot)
+      if (cmd != null && cmd.start <= e.getDot &&
+          Isabelle.prover_setup(buffer).selectedState != cmd)
         Isabelle.prover_setup(buffer).selectedState = cmd
     }
   }
 
-  private def fromCurrent(pos : Int) =
+  def activate() = {
+    text_area.addCaretListener(selected_state_controller)
+    phase_overview.textarea = text_area
+    text_area.addLeftOfScrollBar(phase_overview)
+    text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
+    update_font()
+  }
+
+  def deactivate() = {
+    text_area.getPainter.removeExtension(this)
+    text_area.removeLeftOfScrollBar(phase_overview)
+    text_area.removeCaretListener(selected_state_controller)
+  }
+
+
+  /* painting */
+
+  val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
+  Isabelle.prover(buffer).commandInfo.add(_ => repaint_delay.delay_or_ignore())
+
+  private def from_current(pos: Int) =
     if (col != null && col.start <= pos)
       if (pos < col.start + col.added) col.start
       else pos - col.added + col.removed
     else pos
-  
-  private def toCurrent(pos : Int) = 
+
+  private def to_current(pos : Int) =
     if (col != null && col.start <= pos)
       if (pos < col.start + col.removed) col.start
       else pos + col.added - col.removed
     else pos
-  
-  def repaint(cmd : Command)
+
+  def repaint(cmd: Command) =
   {
-    val ph = cmd.phase
-    if (text_area != null && ph != Phase.REMOVE && ph != Phase.REMOVED) {
-      var start = text_area.getLineOfOffset(toCurrent(cmd.start))
-      var stop = text_area.getLineOfOffset(toCurrent(cmd.stop) - 1)
+    val phase = cmd.phase
+    if (text_area != null && phase != Phase.REMOVE && phase != Phase.REMOVED) {
+      val start = text_area.getLineOfOffset(to_current(cmd.start))
+      val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
       text_area.invalidateLineRange(start, stop)
-      
+
       if (Isabelle.prover_setup(buffer).selectedState == cmd)
-        Isabelle.prover_setup(buffer).selectedState = cmd // update State view
+        Isabelle.prover_setup(buffer).selectedState = cmd  // update State view
     }
   }
-  
-  def repaintAll()
+
+  def repaint_all() =
   {
     if (text_area != null)
-      text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
-                                   text_area.getLastPhysicalLine)
+      text_area.invalidateLineRange(text_area.getFirstPhysicalLine, text_area.getLastPhysicalLine)
   }
 
-  def encolor(gfx : Graphics2D, y : Int, height : Int, begin : Int, finish : Int, color : Color, fill : Boolean){
-      val fm = text_area.getPainter.getFontMetrics
-      val startP = text_area.offsetToXY(begin)
-      val stopP = if (finish < buffer.getLength()) text_area.offsetToXY(finish)
-                  else { var p = text_area.offsetToXY(finish - 1)
-                         p.x = p.x + fm.charWidth(' ')
-                         p }
-			
-      if (startP != null && stopP != null) {
-        gfx.setColor(color)
-        if(fill){gfx.fillRect(startP.x, y, stopP.x - startP.x, height)}
-        else {gfx.drawRect(startP.x, y, stopP.x - startP.x, height)}
+  def encolor(gfx: Graphics2D,
+    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean) =
+  {
+    val start = text_area.offsetToXY(begin)
+    val stop =
+      if (finish < buffer.getLength) text_area.offsetToXY(finish)
+      else {
+        val p = text_area.offsetToXY(finish - 1)
+        p.x = p.x + text_area.getPainter.getFontMetrics.charWidth(' ')
+        p
       }
+
+    if (start != null && stop != null) {
+      gfx.setColor(color)
+      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
+      else gfx.drawRect(start.x, y, stop.x - start.x, height)
+    }
   }
 
-  override def paintValidLine(gfx : Graphics2D, screenLine : Int,
-                              pl : Int, start : Int, end : Int, y : Int)
-  {	
-    val fm = text_area.getPainter.getFontMetrics
-    var savedColor = gfx.getColor
-    var e = Isabelle.prover(buffer).document.getNextCommandContaining(fromCurrent(start))
+
+  /* TextAreaExtension methods */
+
+  override def paintValidLine(gfx: Graphics2D,
+    screen_line: Int, pl: Int, start: Int, end: Int, y: Int) =
+  {
+    val saved_color = gfx.getColor
+
+    val metrics = text_area.getPainter.getFontMetrics
+    var e = Isabelle.prover(buffer).document.getNextCommandContaining(from_current(start))
 
-    //Encolor Phase
-    while (e != null && toCurrent(e.start) < end) {
-      val begin =  start max toCurrent(e.start)
-      val finish = end - 1 min  toCurrent(e.stop)
-      encolor(gfx, y, fm.getHeight, begin, finish, chooseColor(e), true)
+    // encolor phase
+    while (e != null && to_current(e.start) < end) {
+      val begin = start max to_current(e.start)
+      val finish = end - 1 min to_current(e.stop)
+      encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
+
       // paint details of command
-      for(node <- e.root_node.dfs){
-        val begin = toCurrent(node.start + e.start)
-        val finish = toCurrent(node.end + e.start)
-        if(finish > start && begin < end)
-        encolor(gfx, y + fm.getHeight - 4, 2, begin max start, finish min end, chooseColor(node.short), true)
+      for (node <- e.root_node.dfs) {
+        val begin = to_current(node.start + e.start)
+        val finish = to_current(node.end + e.start)
+        if (finish > start && begin < end) {
+          encolor(gfx, y + metrics.getHeight - 4, 2, begin max start, finish min end,
+            TheoryView.choose_color(node.short), true)
+        }
       }
       e = e.next
     }
 
-    gfx.setColor(savedColor)
+    gfx.setColor(saved_color)
   }
-	
-  def content(start : Int, stop : Int) = buffer.getText(start, stop - start)
-  override def length = buffer.getLength
+
+
+  /* Text methods */
 
-  def changes = changesSource
+  def content(start: Int, stop: Int) = buffer.getText(start, stop - start)
+  def length = buffer.getLength
+  def changes = changes_source
+
+
+
+  /* BufferListener methods */
 
   private def commit() {
     if (col != null)
       changes.fire(col)
     col = null
-    if (colTimer.isRunning())
-      colTimer.stop()
-  }	
-	
-  private def delayCommit() {
-    if (colTimer.isRunning())
-      colTimer.restart()
+    if (col_timer.isRunning())
+      col_timer.stop()
+  }
+
+  private def delay_commit() {
+    if (col_timer.isRunning())
+      col_timer.restart()
     else
-      colTimer.start()
+      col_timer.start()
   }
-	
-  override def contentInserted(buffer : JEditBuffer, startLine : Int, 
-                               offset : Int, numLines : Int, length : Int) { }
-  override def contentRemoved(buffer : JEditBuffer, startLine : Int, 
-                              offset : Int, numLines : Int, length : Int) { }
+
+
+  override def contentInserted(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+  override def contentRemoved(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
 
-  override def preContentInserted(buffer : JEditBuffer, startLine : Int,
-			offset : Int, numLines : Int, length : Int) {
+  override def preContentInserted(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) =
+  {
     if (col == null)
-      col = new Changed(offset, length, 0)
-    else if (col.start <= offset && offset <= col.start + col.added) 
-      col = new Changed(col.start, col.added + length, col.removed)
-    else { 
+      col = new Text.Changed(offset, length, 0)
+    else if (col.start <= offset && offset <= col.start + col.added)
+      col = new Text.Changed(col.start, col.added + length, col.removed)
+    else {
       commit()
-      col = new Changed(offset, length, 0) 
+      col = new Text.Changed(offset, length, 0)
     }
-    delayCommit()
-  }	
-  
-  override def preContentRemoved(buffer : JEditBuffer, startLine : Int,
-			start : Int, numLines : Int, removed : Int) {
+    delay_commit()
+  }
+
+  override def preContentRemoved(buffer: JEditBuffer,
+    start_line: Int, start: Int, num_lines: Int, removed: Int) =
+  {
     if (col == null)
-      col = new Changed(start, 0, removed)
-    else if (col.start > start + removed || start > col.start + col.added) { 
+      col = new Text.Changed(start, 0, removed)
+    else if (col.start > start + removed || start > col.start + col.added) {
       commit()
-      col = new Changed(start, 0, removed) 
+      col = new Text.Changed(start, 0, removed)
     }
     else {
       val offset = start - col.start
       val diff = col.added - removed
-      val (added, addRemoved) = 
-        if (diff < offset) 
+      val (added, add_removed) =
+        if (diff < offset)
           (offset max 0, diff - (offset max 0))
-        else 
+        else
           (diff - (offset min 0), offset min 0)
-      
-      col = new Changed(start min col.start, added, col.removed - addRemoved) 
+      col = new Text.Changed(start min col.start, added, col.removed - add_removed)
     }
-    delayCommit()
+    delay_commit()
   }
 
-  override def bufferLoaded(buffer : JEditBuffer) { }
-  override def foldHandlerChanged(buffer : JEditBuffer) { }
-  override def foldLevelChanged(buffer : JEditBuffer, startLine : Int, 
-                                endLine : Int) = { }
-  override def transactionComplete(buffer : JEditBuffer) = { } 
+  override def bufferLoaded(buffer: JEditBuffer) { }
+  override def foldHandlerChanged(buffer: JEditBuffer) { }
+  override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
+  override def transactionComplete(buffer: JEditBuffer) { }
 }
\ No newline at end of file