src/Tools/jEdit/src/proofdocument/theory_view.scala
changeset 34759 bfea7839d9e1
parent 34742 7b8847852aae
child 34760 dc7f5e0d9d27
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala	Tue Dec 08 14:49:01 2009 +0100
     1.3 @@ -0,0 +1,327 @@
     1.4 +/*
     1.5 + * jEdit text area as document text source
     1.6 + *
     1.7 + * @author Fabian Immler, TU Munich
     1.8 + * @author Johannes Hölzl, TU Munich
     1.9 + * @author Makarius
    1.10 + */
    1.11 +
    1.12 +package isabelle.jedit
    1.13 +
    1.14 +import scala.actors.Actor, Actor._
    1.15 +import scala.collection.mutable
    1.16 +
    1.17 +import isabelle.proofdocument.{ProofDocument, Change, Edit, Insert, Remove}
    1.18 +import isabelle.prover.{Prover, Command}
    1.19 +
    1.20 +import java.awt.{Color, Graphics2D}
    1.21 +import javax.swing.event.{CaretListener, CaretEvent}
    1.22 +
    1.23 +import org.gjt.sp.jedit.buffer.{BufferListener, JEditBuffer}
    1.24 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    1.25 +import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
    1.26 +
    1.27 +
    1.28 +object TheoryView
    1.29 +{
    1.30 +  def choose_color(command: Command, doc: ProofDocument): Color =
    1.31 +  {
    1.32 +    command.status(doc) match {
    1.33 +      case Command.Status.UNPROCESSED => new Color(255, 228, 225)
    1.34 +      case Command.Status.FINISHED => new Color(234, 248, 255)
    1.35 +      case Command.Status.FAILED => new Color(255, 106, 106)
    1.36 +      case _ => Color.red
    1.37 +    }
    1.38 +  }
    1.39 +}
    1.40 +
    1.41 +
    1.42 +class TheoryView(text_area: JEditTextArea)
    1.43 +{
    1.44 +  private val buffer = text_area.getBuffer
    1.45 +
    1.46 +
    1.47 +  /* prover setup */
    1.48 +
    1.49 +  val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
    1.50 +
    1.51 +  prover.command_change += ((command: Command) =>
    1.52 +    if (current_document().commands.contains(command))
    1.53 +      Swing_Thread.later {
    1.54 +        // FIXME proper handling of buffer vs. text areas
    1.55 +        // repaint if buffer is active
    1.56 +        if (text_area.getBuffer == buffer) {
    1.57 +          update_syntax(command)
    1.58 +          invalidate_line(command)
    1.59 +          overview.repaint()
    1.60 +        }
    1.61 +      })
    1.62 +
    1.63 +
    1.64 +  /* changes vs. edits */
    1.65 +
    1.66 +  private val change_0 = new Change(prover.document_0.id, None, Nil)
    1.67 +  private var _changes = List(change_0)   // owned by Swing/AWT thread
    1.68 +  def changes = _changes
    1.69 +  private var current_change = change_0
    1.70 +
    1.71 +  private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread
    1.72 +
    1.73 +  private val edits_delay = Swing_Thread.delay_last(300) {
    1.74 +    if (!edits.isEmpty) {
    1.75 +      val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
    1.76 +      _changes ::= change
    1.77 +      prover.input(change)
    1.78 +      current_change = change
    1.79 +      edits.clear
    1.80 +    }
    1.81 +  }
    1.82 +
    1.83 +
    1.84 +  /* buffer_listener */
    1.85 +
    1.86 +  private val buffer_listener = new BufferListener {
    1.87 +    override def preContentInserted(buffer: JEditBuffer,
    1.88 +      start_line: Int, offset: Int, num_lines: Int, length: Int)
    1.89 +    {
    1.90 +      edits += Insert(offset, buffer.getText(offset, length))
    1.91 +      edits_delay()
    1.92 +    }
    1.93 +
    1.94 +    override def preContentRemoved(buffer: JEditBuffer,
    1.95 +      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
    1.96 +    {
    1.97 +      edits += Remove(start, buffer.getText(start, removed_length))
    1.98 +      edits_delay()
    1.99 +    }
   1.100 +
   1.101 +    override def contentInserted(buffer: JEditBuffer,
   1.102 +      start_line: Int, offset: Int, num_lines: Int, length: Int) { }
   1.103 +
   1.104 +    override def contentRemoved(buffer: JEditBuffer,
   1.105 +      start_line: Int, offset: Int, num_lines: Int, length: Int) { }
   1.106 +
   1.107 +    override def bufferLoaded(buffer: JEditBuffer) { }
   1.108 +    override def foldHandlerChanged(buffer: JEditBuffer) { }
   1.109 +    override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
   1.110 +    override def transactionComplete(buffer: JEditBuffer) { }
   1.111 +  }
   1.112 +
   1.113 +
   1.114 +  /* text_area_extension */
   1.115 +
   1.116 +  private val text_area_extension = new TextAreaExtension {
   1.117 +    override def paintValidLine(gfx: Graphics2D,
   1.118 +      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
   1.119 +    {
   1.120 +      val document = current_document()
   1.121 +      def from_current(pos: Int) = TheoryView.this.from_current(document, pos)
   1.122 +      def to_current(pos: Int) = TheoryView.this.to_current(document, pos)
   1.123 +      val saved_color = gfx.getColor
   1.124 +
   1.125 +      val metrics = text_area.getPainter.getFontMetrics
   1.126 +
   1.127 +      // encolor phase
   1.128 +      var cmd = document.command_at(from_current(start))
   1.129 +      while (cmd.isDefined && cmd.get.start(document) < end) {
   1.130 +        val e = cmd.get
   1.131 +        val begin = start max to_current(e.start(document))
   1.132 +        val finish = (end - 1) min to_current(e.stop(document))
   1.133 +        encolor(gfx, y, metrics.getHeight, begin, finish,
   1.134 +          TheoryView.choose_color(e, document), true)
   1.135 +        cmd = document.commands.next(e)
   1.136 +      }
   1.137 +
   1.138 +      gfx.setColor(saved_color)
   1.139 +    }
   1.140 +
   1.141 +    override def getToolTipText(x: Int, y: Int): String =
   1.142 +    {
   1.143 +      val document = current_document()
   1.144 +      val offset = from_current(document, text_area.xyToOffset(x, y))
   1.145 +      document.command_at(offset) match {
   1.146 +        case Some(cmd) =>
   1.147 +          document.token_start(cmd.tokens.first)
   1.148 +          cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
   1.149 +        case None => null
   1.150 +      }
   1.151 +    }
   1.152 +  }
   1.153 +
   1.154 +
   1.155 +  /* activation */
   1.156 +
   1.157 +  private val overview = new Document_Overview(prover, text_area, to_current)
   1.158 +
   1.159 +  private val selected_state_controller = new CaretListener {
   1.160 +    override def caretUpdate(e: CaretEvent) {
   1.161 +      val doc = current_document()
   1.162 +      doc.command_at(e.getDot) match {
   1.163 +        case Some(cmd)
   1.164 +          if (doc.token_start(cmd.tokens.first) <= e.getDot &&
   1.165 +            Isabelle.plugin.selected_state != cmd) =>
   1.166 +          Isabelle.plugin.selected_state = cmd
   1.167 +        case _ =>
   1.168 +      }
   1.169 +    }
   1.170 +  }
   1.171 +
   1.172 +  def activate() {
   1.173 +    text_area.addCaretListener(selected_state_controller)
   1.174 +    text_area.addLeftOfScrollBar(overview)
   1.175 +    text_area.getPainter.
   1.176 +      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
   1.177 +    buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
   1.178 +    buffer.addBufferListener(buffer_listener)
   1.179 +
   1.180 +    val dockable =
   1.181 +      text_area.getView.getDockableWindowManager.getDockable("isabelle-output")
   1.182 +    if (dockable != null) {
   1.183 +      val output_dockable = dockable.asInstanceOf[OutputDockable]
   1.184 +      val output_text_view = prover.output_text_view
   1.185 +      output_dockable.set_text(output_text_view)
   1.186 +    }
   1.187 +
   1.188 +    buffer.propertiesChanged()
   1.189 +  }
   1.190 +
   1.191 +  def deactivate() {
   1.192 +    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
   1.193 +    buffer.removeBufferListener(buffer_listener)
   1.194 +    text_area.getPainter.removeExtension(text_area_extension)
   1.195 +    text_area.removeLeftOfScrollBar(overview)
   1.196 +    text_area.removeCaretListener(selected_state_controller)
   1.197 +  }
   1.198 +
   1.199 +
   1.200 +  /* history of changes */
   1.201 +
   1.202 +  private def doc_or_pred(c: Change): ProofDocument =
   1.203 +    prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
   1.204 +
   1.205 +  def current_document() = doc_or_pred(current_change)
   1.206 +
   1.207 +
   1.208 +  /* update to desired version */
   1.209 +
   1.210 +  def set_version(goal: Change) {
   1.211 +    // changes in buffer must be ignored
   1.212 +    buffer.removeBufferListener(buffer_listener)
   1.213 +
   1.214 +    def apply(change: Change): Unit = change.edits.foreach {
   1.215 +      case Insert(start, text) => buffer.insert(start, text)
   1.216 +      case Remove(start, text) => buffer.remove(start, text.length)
   1.217 +    }
   1.218 +
   1.219 +    def unapply(change: Change): Unit = change.edits.reverse.foreach {
   1.220 +      case Insert(start, text) => buffer.remove(start, text.length)
   1.221 +      case Remove(start, text) => buffer.insert(start, text)
   1.222 +    }
   1.223 +
   1.224 +    // undo/redo changes
   1.225 +    val ancs_current = current_change.ancestors
   1.226 +    val ancs_goal = goal.ancestors
   1.227 +    val paired = ancs_current.reverse zip ancs_goal.reverse
   1.228 +    def last_common[A](xs: List[(A, A)]): Option[A] = {
   1.229 +      xs match {
   1.230 +        case (x, y) :: xs =>
   1.231 +          if (x == y)
   1.232 +            xs match {
   1.233 +              case (a, b) :: ys =>
   1.234 +                if (a == b) last_common(xs)
   1.235 +                else Some(x)
   1.236 +              case _ => Some(x)
   1.237 +            }
   1.238 +          else None
   1.239 +        case _ => None
   1.240 +      }
   1.241 +    }
   1.242 +    val common_anc = last_common(paired).get
   1.243 +
   1.244 +    ancs_current.takeWhile(_ != common_anc) map unapply
   1.245 +    ancs_goal.takeWhile(_ != common_anc).reverse map apply
   1.246 +
   1.247 +    current_change = goal
   1.248 +    // invoke repaint
   1.249 +    buffer.propertiesChanged()
   1.250 +    invalidate_all()
   1.251 +    overview.repaint()
   1.252 +
   1.253 +    // track changes in buffer
   1.254 +    buffer.addBufferListener(buffer_listener)
   1.255 +  }
   1.256 +
   1.257 +
   1.258 +  /* transforming offsets */
   1.259 +
   1.260 +  private def changes_from(doc: ProofDocument): List[Edit] =
   1.261 +    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
   1.262 +      edits.toList
   1.263 +
   1.264 +  def from_current(doc: ProofDocument, offset: Int): Int =
   1.265 +    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
   1.266 +
   1.267 +  def to_current(doc: ProofDocument, offset: Int): Int =
   1.268 +    (offset /: changes_from(doc)) ((i, change) => change after i)
   1.269 +
   1.270 +
   1.271 +  private def lines_of_command(cmd: Command) =
   1.272 +  {
   1.273 +    val document = current_document()
   1.274 +    (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
   1.275 +     buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
   1.276 +  }
   1.277 +
   1.278 +
   1.279 +  /* (re)painting */
   1.280 +
   1.281 +  private val update_delay = Swing_Thread.delay_first(500) { buffer.propertiesChanged() }
   1.282 +
   1.283 +  private def update_syntax(cmd: Command) {
   1.284 +    val (line1, line2) = lines_of_command(cmd)
   1.285 +    if (line2 >= text_area.getFirstLine &&
   1.286 +      line1 <= text_area.getFirstLine + text_area.getVisibleLines)
   1.287 +        update_delay()
   1.288 +  }
   1.289 +
   1.290 +  private def invalidate_line(cmd: Command) =
   1.291 +  {
   1.292 +    val (start, stop) = lines_of_command(cmd)
   1.293 +    text_area.invalidateLineRange(start, stop)
   1.294 +
   1.295 +    if (Isabelle.plugin.selected_state == cmd)
   1.296 +      Isabelle.plugin.selected_state = cmd  // update State view
   1.297 +  }
   1.298 +
   1.299 +  private def invalidate_all() =
   1.300 +    text_area.invalidateLineRange(text_area.getFirstPhysicalLine,
   1.301 +      text_area.getLastPhysicalLine)
   1.302 +
   1.303 +  private def encolor(gfx: Graphics2D,
   1.304 +    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)
   1.305 +  {
   1.306 +    val start = text_area.offsetToXY(begin)
   1.307 +    val stop =
   1.308 +      if (finish < buffer.getLength) text_area.offsetToXY(finish)
   1.309 +      else {
   1.310 +        val p = text_area.offsetToXY(finish - 1)
   1.311 +        val metrics = text_area.getPainter.getFontMetrics
   1.312 +        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)
   1.313 +        p
   1.314 +      }
   1.315 +
   1.316 +    if (start != null && stop != null) {
   1.317 +      gfx.setColor(color)
   1.318 +      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)
   1.319 +      else gfx.drawRect(start.x, y, stop.x - start.x, height)
   1.320 +    }
   1.321 +  }
   1.322 +
   1.323 +
   1.324 +  /* init */
   1.325 +
   1.326 +  prover.start()
   1.327 +
   1.328 +  edits += Insert(0, buffer.getText(0, buffer.getLength))
   1.329 +  edits_delay()
   1.330 +}