src/Tools/jEdit/src/document_view.scala
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56770 e160ae47db94
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Apr 25 12:27:18 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Apr 25 12:51:08 2014 +0200
     1.3 @@ -10,8 +10,6 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import scala.actors.Actor._
     1.8 -
     1.9  import java.awt.Graphics2D
    1.10  import java.awt.event.KeyEvent
    1.11  import javax.swing.event.{CaretListener, CaretEvent}
    1.12 @@ -176,7 +174,7 @@
    1.13  
    1.14    private val delay_caret_update =
    1.15      Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    1.16 -      session.caret_focus.event(Session.Caret_Focus)
    1.17 +      session.caret_focus.post(Session.Caret_Focus)
    1.18      }
    1.19  
    1.20    private val caret_listener = new CaretListener {
    1.21 @@ -193,60 +191,54 @@
    1.22    }
    1.23  
    1.24  
    1.25 -  /* main actor */
    1.26 +  /* main */
    1.27  
    1.28 -  private val main_actor = actor {
    1.29 -    loop {
    1.30 -      react {
    1.31 -        case _: Session.Raw_Edits =>
    1.32 -          Swing_Thread.later {
    1.33 -            overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
    1.34 -          }
    1.35 +  private val main =
    1.36 +    Session.Consumer[Any](getClass.getName) {
    1.37 +      case _: Session.Raw_Edits =>
    1.38 +        Swing_Thread.later {
    1.39 +          overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
    1.40 +        }
    1.41  
    1.42 -        case changed: Session.Commands_Changed =>
    1.43 -          val buffer = model.buffer
    1.44 -          Swing_Thread.later {
    1.45 -            JEdit_Lib.buffer_lock(buffer) {
    1.46 -              if (model.buffer == text_area.getBuffer) {
    1.47 -                val snapshot = model.snapshot()
    1.48 +      case changed: Session.Commands_Changed =>
    1.49 +        val buffer = model.buffer
    1.50 +        Swing_Thread.later {
    1.51 +          JEdit_Lib.buffer_lock(buffer) {
    1.52 +            if (model.buffer == text_area.getBuffer) {
    1.53 +              val snapshot = model.snapshot()
    1.54  
    1.55 -                val load_changed =
    1.56 -                  snapshot.load_commands.exists(changed.commands.contains)
    1.57 +              val load_changed =
    1.58 +                snapshot.load_commands.exists(changed.commands.contains)
    1.59  
    1.60 -                if (changed.assignment || load_changed ||
    1.61 -                    (changed.nodes.contains(model.node_name) &&
    1.62 -                     changed.commands.exists(snapshot.node.commands.contains)))
    1.63 -                  Swing_Thread.later { overview.delay_repaint.invoke() }
    1.64 +              if (changed.assignment || load_changed ||
    1.65 +                  (changed.nodes.contains(model.node_name) &&
    1.66 +                   changed.commands.exists(snapshot.node.commands.contains)))
    1.67 +                Swing_Thread.later { overview.delay_repaint.invoke() }
    1.68  
    1.69 -                val visible_lines = text_area.getVisibleLines
    1.70 -                if (visible_lines > 0) {
    1.71 -                  if (changed.assignment || load_changed)
    1.72 -                    text_area.invalidateScreenLineRange(0, visible_lines)
    1.73 -                  else {
    1.74 -                    val visible_range = JEdit_Lib.visible_range(text_area).get
    1.75 -                    val visible_iterator =
    1.76 -                      snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
    1.77 -                    if (visible_iterator.exists(changed.commands)) {
    1.78 -                      for {
    1.79 -                        line <- (0 until visible_lines).iterator
    1.80 -                        start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.81 -                        end = text_area.getScreenLineEndOffset(line) if end >= 0
    1.82 -                        range = Text.Range(start, end)
    1.83 -                        line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
    1.84 -                        if line_cmds.exists(changed.commands)
    1.85 -                      } text_area.invalidateScreenLineRange(line, line)
    1.86 -                    }
    1.87 +              val visible_lines = text_area.getVisibleLines
    1.88 +              if (visible_lines > 0) {
    1.89 +                if (changed.assignment || load_changed)
    1.90 +                  text_area.invalidateScreenLineRange(0, visible_lines)
    1.91 +                else {
    1.92 +                  val visible_range = JEdit_Lib.visible_range(text_area).get
    1.93 +                  val visible_iterator =
    1.94 +                    snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
    1.95 +                  if (visible_iterator.exists(changed.commands)) {
    1.96 +                    for {
    1.97 +                      line <- (0 until visible_lines).iterator
    1.98 +                      start = text_area.getScreenLineStartOffset(line) if start >= 0
    1.99 +                      end = text_area.getScreenLineEndOffset(line) if end >= 0
   1.100 +                      range = Text.Range(start, end)
   1.101 +                      line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
   1.102 +                      if line_cmds.exists(changed.commands)
   1.103 +                    } text_area.invalidateScreenLineRange(line, line)
   1.104                    }
   1.105                  }
   1.106                }
   1.107              }
   1.108            }
   1.109 -
   1.110 -        case bad =>
   1.111 -          System.err.println("command_change_actor: ignoring bad message " + bad)
   1.112 -      }
   1.113 +        }
   1.114      }
   1.115 -  }
   1.116  
   1.117  
   1.118    /* activation */
   1.119 @@ -261,16 +253,16 @@
   1.120      text_area.addKeyListener(key_listener)
   1.121      text_area.addCaretListener(caret_listener)
   1.122      text_area.addLeftOfScrollBar(overview)
   1.123 -    session.raw_edits += main_actor
   1.124 -    session.commands_changed += main_actor
   1.125 +    session.raw_edits += main
   1.126 +    session.commands_changed += main
   1.127    }
   1.128  
   1.129    private def deactivate()
   1.130    {
   1.131      val painter = text_area.getPainter
   1.132  
   1.133 -    session.raw_edits -= main_actor
   1.134 -    session.commands_changed -= main_actor
   1.135 +    session.raw_edits -= main
   1.136 +    session.commands_changed -= main
   1.137      text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
   1.138      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
   1.139      text_area.removeKeyListener(key_listener)