src/Tools/jEdit/src/proofdocument/theory_view.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34772 1a79c9b9af82
permissions -rw-r--r--
misc modernization of names;
     1 /*
     2  * jEdit text area as document text source
     3  *
     4  * @author Fabian Immler, TU Munich
     5  * @author Johannes Hölzl, TU Munich
     6  * @author Makarius
     7  */
     8 
     9 package isabelle.proofdocument
    10 
    11 
    12 import scala.actors.Actor, Actor._
    13 import scala.collection.mutable
    14 
    15 import java.awt.{Color, Graphics2D}
    16 import javax.swing.event.{CaretListener, CaretEvent}
    17 
    18 import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
    19 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    20 import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
    21 
    22 import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker, Raw_Output_Dockable}
    23 
    24 
    25 object Theory_View
    26 {
    27   def choose_color(command: Command, doc: Proof_Document): Color =
    28   {
    29     command.status(doc) match {
    30       case Command.Status.UNPROCESSED => new Color(255, 228, 225)
    31       case Command.Status.FINISHED => new Color(234, 248, 255)
    32       case Command.Status.FAILED => new Color(255, 106, 106)
    33       case _ => Color.red
    34     }
    35   }
    36 }
    37 
    38 
    39 class Theory_View(text_area: JEditTextArea)
    40 {
    41   private val buffer = text_area.getBuffer
    42 
    43 
    44   /* prover setup */
    45 
    46   val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
    47 
    48   prover.command_change += ((command: Command) =>
    49     if (current_document().commands.contains(command))
    50       Swing_Thread.later {
    51         // FIXME proper handling of buffer vs. text areas
    52         // repaint if buffer is active
    53         if (text_area.getBuffer == buffer) {
    54           update_syntax(command)
    55           invalidate_line(command)
    56           overview.repaint()
    57         }
    58       })
    59 
    60 
    61   /* changes vs. edits */
    62 
    63   private val change_0 = new Change(prover.document_0.id, None, Nil)
    64   private var _changes = List(change_0)   // owned by Swing/AWT thread
    65   def changes = _changes
    66   private var current_change = change_0
    67 
    68   private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread
    69 
    70   private val edits_delay = Swing_Thread.delay_last(300) {
    71     if (!edits.isEmpty) {
    72       val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
    73       _changes ::= change
    74       prover.input(change)
    75       current_change = change
    76       edits.clear
    77     }
    78   }
    79 
    80 
    81   /* buffer_listener */
    82 
    83   private val buffer_listener = new BufferListener {
    84     override def preContentInserted(buffer: JEditBuffer,
    85       start_line: Int, offset: Int, num_lines: Int, length: Int)
    86     {
    87       edits += Insert(offset, buffer.getText(offset, length))
    88       edits_delay()
    89     }
    90 
    91     override def preContentRemoved(buffer: JEditBuffer,
    92       start_line: Int, start: Int, num_lines: Int, removed_length: Int)
    93     {
    94       edits += Remove(start, buffer.getText(start, removed_length))
    95       edits_delay()
    96     }
    97 
    98     override def contentInserted(buffer: JEditBuffer,
    99       start_line: Int, offset: Int, num_lines: Int, length: Int) { }
   100 
   101     override def contentRemoved(buffer: JEditBuffer,
   102       start_line: Int, offset: Int, num_lines: Int, length: Int) { }
   103 
   104     override def bufferLoaded(buffer: JEditBuffer) { }
   105     override def foldHandlerChanged(buffer: JEditBuffer) { }
   106     override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
   107     override def transactionComplete(buffer: JEditBuffer) { }
   108   }
   109 
   110 
   111   /* text_area_extension */
   112 
   113   private val text_area_extension = new TextAreaExtension {
   114     override def paintValidLine(gfx: Graphics2D,
   115       screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   116     {
   117       val document = current_document()
   118       def from_current(pos: Int) = Theory_View.this.from_current(document, pos)
   119       def to_current(pos: Int) = Theory_View.this.to_current(document, pos)
   120       val saved_color = gfx.getColor
   121 
   122       val metrics = text_area.getPainter.getFontMetrics
   123 
   124       // encolor phase
   125       var cmd = document.command_at(from_current(start))
   126       while (cmd.isDefined && cmd.get.start(document) < end) {
   127         val e = cmd.get
   128         val begin = start max to_current(e.start(document))
   129         val finish = (end - 1) min to_current(e.stop(document))
   130         encolor(gfx, y, metrics.getHeight, begin, finish,
   131           Theory_View.choose_color(e, document), true)
   132         cmd = document.commands.next(e)
   133       }
   134 
   135       gfx.setColor(saved_color)
   136     }
   137 
   138     override def getToolTipText(x: Int, y: Int): String =
   139     {
   140       val document = current_document()
   141       val offset = from_current(document, text_area.xyToOffset(x, y))
   142       document.command_at(offset) match {
   143         case Some(cmd) =>
   144           document.token_start(cmd.tokens.first)
   145           cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
   146         case None => null
   147       }
   148     }
   149   }
   150 
   151 
   152   /* activation */
   153 
   154   private val overview = new Document_Overview(prover, text_area, to_current)
   155 
   156   private val selected_state_controller = new CaretListener {
   157     override def caretUpdate(e: CaretEvent) {
   158       val doc = current_document()
   159       doc.command_at(e.getDot) match {
   160         case Some(cmd)
   161           if (doc.token_start(cmd.tokens.first) <= e.getDot &&
   162             Isabelle.plugin.selected_state != cmd) =>
   163           Isabelle.plugin.selected_state = cmd
   164         case _ =>
   165       }
   166     }
   167   }
   168 
   169   def activate()
   170   {
   171     text_area.addCaretListener(selected_state_controller)
   172     text_area.addLeftOfScrollBar(overview)
   173     text_area.getPainter.
   174       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
   175     buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover))
   176     buffer.addBufferListener(buffer_listener)
   177 
   178     val dockable =
   179       text_area.getView.getDockableWindowManager.getDockable("isabelle-raw-output")
   180     if (dockable != null) {
   181       val output_dockable = dockable.asInstanceOf[Raw_Output_Dockable]
   182       val output_text_view = prover.output_text_view
   183       output_dockable.set_text(output_text_view)
   184     }
   185 
   186     buffer.propertiesChanged()
   187   }
   188 
   189   def deactivate() {
   190     buffer.setTokenMarker(buffer.getMode.getTokenMarker)
   191     buffer.removeBufferListener(buffer_listener)
   192     text_area.getPainter.removeExtension(text_area_extension)
   193     text_area.removeLeftOfScrollBar(overview)
   194     text_area.removeCaretListener(selected_state_controller)
   195   }
   196 
   197 
   198   /* history of changes */
   199 
   200   private def doc_or_pred(c: Change): Proof_Document =
   201     prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
   202 
   203   def current_document() = doc_or_pred(current_change)
   204 
   205 
   206   /* update to desired version */
   207 
   208   def set_version(goal: Change) {
   209     // changes in buffer must be ignored
   210     buffer.removeBufferListener(buffer_listener)
   211 
   212     def apply(change: Change): Unit = change.edits.foreach {
   213       case Insert(start, text) => buffer.insert(start, text)
   214       case Remove(start, text) => buffer.remove(start, text.length)
   215     }
   216 
   217     def unapply(change: Change): Unit = change.edits.reverse.foreach {
   218       case Insert(start, text) => buffer.remove(start, text.length)
   219       case Remove(start, text) => buffer.insert(start, text)
   220     }
   221 
   222     // undo/redo changes
   223     val ancs_current = current_change.ancestors
   224     val ancs_goal = goal.ancestors
   225     val paired = ancs_current.reverse zip ancs_goal.reverse
   226     def last_common[A](xs: List[(A, A)]): Option[A] = {
   227       xs match {
   228         case (x, y) :: xs =>
   229           if (x == y)
   230             xs match {
   231               case (a, b) :: ys =>
   232                 if (a == b) last_common(xs)
   233                 else Some(x)
   234               case _ => Some(x)
   235             }
   236           else None
   237         case _ => None
   238       }
   239     }
   240     val common_anc = last_common(paired).get
   241 
   242     ancs_current.takeWhile(_ != common_anc) map unapply
   243     ancs_goal.takeWhile(_ != common_anc).reverse map apply
   244 
   245     current_change = goal
   246     // invoke repaint
   247     buffer.propertiesChanged()
   248     invalidate_all()
   249     overview.repaint()
   250 
   251     // track changes in buffer
   252     buffer.addBufferListener(buffer_listener)
   253   }
   254 
   255 
   256   /* transforming offsets */
   257 
   258   private def changes_from(doc: Proof_Document): List[Edit] =
   259     List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
   260       edits.toList
   261 
   262   def from_current(doc: Proof_Document, offset: Int): Int =
   263     (offset /: changes_from(doc).reverse) ((i, change) => change before i)
   264 
   265   def to_current(doc: Proof_Document, offset: Int): Int =
   266     (offset /: changes_from(doc)) ((i, change) => change after i)
   267 
   268 
   269   private def lines_of_command(cmd: Command) =
   270   {
   271     val document = current_document()
   272     (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
   273      buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
   274   }
   275 
   276 
   277   /* (re)painting */
   278 
   279   private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() }
   280 
   281   private def update_syntax(cmd: Command) {
   282     val (line1, line2) = lines_of_command(cmd)
   283     if (line2 >= text_area.getFirstLine &&
   284       line1 <= text_area.getFirstLine + text_area.getVisibleLines)
   285         update_delay()
   286   }
   287 
   288   private def invalidate_line(cmd: Command) =
   289   {
   290     val (start, stop) = lines_of_command(cmd)
   291     text_area.invalidateLineRange(start, stop)
   292 
   293     if (Isabelle.plugin.selected_state == cmd)
   294       Isabelle.plugin.selected_state = cmd  // update State view
   295   }
   296 
   297   private def invalidate_all() =
   298     text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
   299       text_area.getLastPhysicalLine)
   300 
   301   private def encolor(gfx: Graphics2D,
   302     y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
   303   {
   304     val start = text_area.offsetToXY(begin)
   305     val stop =
   306       if (finish < buffer.getLength) text_area.offsetToXY(finish)
   307       else {
   308         val p = text_area.offsetToXY(finish - 1)
   309         val metrics = text_area.getPainter.getFontMetrics
   310         p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
   311         p
   312       }
   313 
   314     if (start != null && stop != null) {
   315       gfx.setColor(color)
   316       if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
   317       else gfx.drawRect(start.x, y, stop.x - start.x, height)
   318     }
   319   }
   320 
   321 
   322   /* init */
   323 
   324   prover.start()
   325 
   326   edits += Insert(0, buffer.getText(0, buffer.getLength))
   327   edits_delay()
   328 }