more explicit treatment of Swing thread context;
authorwenzelm
Sat Aug 07 16:15:52 2010 +0200 (2010-08-07)
changeset 382232a368e8e0a80
parent 38222 dac5fa0ac971
child 38224 809578d7f6af
more explicit treatment of Swing thread context;
Document_Model.snapshot: require Swing thread;
src/Pure/System/swing_thread.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
     1.1 --- a/src/Pure/System/swing_thread.scala	Sat Aug 07 14:45:26 2010 +0200
     1.2 +++ b/src/Pure/System/swing_thread.scala	Sat Aug 07 16:15:52 2010 +0200
     1.3 @@ -46,8 +46,9 @@
     1.4  
     1.5    private def delayed_action(first: Boolean)(time_span: Int)(action: => Unit): () => Unit =
     1.6    {
     1.7 -    val listener =
     1.8 -      new ActionListener { override def actionPerformed(e: ActionEvent) { action } }
     1.9 +    val listener = new ActionListener {
    1.10 +      override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
    1.11 +    }
    1.12      val timer = new Timer(time_span, listener)
    1.13      timer.setRepeats(false)
    1.14  
     2.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 14:45:26 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sat Aug 07 16:15:52 2010 +0200
     2.3 @@ -151,7 +151,7 @@
     2.4  
     2.5    def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
     2.6    {
     2.7 -    Swing_Thread.assert()
     2.8 +    Swing_Thread.require()
     2.9      val model = new Document_Model(session, buffer, thy_name)
    2.10      buffer.setProperty(key, model)
    2.11      model.activate()
    2.12 @@ -160,7 +160,7 @@
    2.13  
    2.14    def apply(buffer: Buffer): Option[Document_Model] =
    2.15    {
    2.16 -    Swing_Thread.assert()
    2.17 +    Swing_Thread.require()
    2.18      buffer.getProperty(key) match {
    2.19        case model: Document_Model => Some(model)
    2.20        case _ => None
    2.21 @@ -169,7 +169,7 @@
    2.22  
    2.23    def exit(buffer: Buffer)
    2.24    {
    2.25 -    Swing_Thread.assert()
    2.26 +    Swing_Thread.require()
    2.27      apply(buffer) match {
    2.28        case None => error("No document model for buffer: " + buffer)
    2.29        case Some(model) =>
    2.30 @@ -209,8 +209,10 @@
    2.31  
    2.32    /* snapshot */
    2.33  
    2.34 -  def snapshot(): Change.Snapshot =
    2.35 -    Swing_Thread.now { session.current_change().snapshot(thy_name, edits_buffer.toList) }
    2.36 +  def snapshot(): Change.Snapshot = {
    2.37 +    Swing_Thread.require()
    2.38 +    session.current_change().snapshot(thy_name, edits_buffer.toList)
    2.39 +  }
    2.40  
    2.41  
    2.42    /* buffer listener */
    2.43 @@ -246,7 +248,7 @@
    2.44        val start = buffer.getLineStartOffset(line)
    2.45        val stop = start + line_segment.count
    2.46  
    2.47 -      val snapshot = Document_Model.this.snapshot()
    2.48 +      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
    2.49  
    2.50        /* FIXME
    2.51        for (text_area <- Isabelle.jedit_text_areas(buffer)
     3.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat Aug 07 14:45:26 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Aug 07 16:15:52 2010 +0200
     3.3 @@ -46,7 +46,7 @@
     3.4  
     3.5    def init(model: Document_Model, text_area: TextArea): Document_View =
     3.6    {
     3.7 -    Swing_Thread.assert()
     3.8 +    Swing_Thread.require()
     3.9      val doc_view = new Document_View(model, text_area)
    3.10      text_area.putClientProperty(key, doc_view)
    3.11      doc_view.activate()
    3.12 @@ -55,7 +55,7 @@
    3.13  
    3.14    def apply(text_area: TextArea): Option[Document_View] =
    3.15    {
    3.16 -    Swing_Thread.assert()
    3.17 +    Swing_Thread.require()
    3.18      text_area.getClientProperty(key) match {
    3.19        case doc_view: Document_View => Some(doc_view)
    3.20        case _ => None
    3.21 @@ -64,7 +64,7 @@
    3.22  
    3.23    def exit(text_area: TextArea)
    3.24    {
    3.25 -    Swing_Thread.assert()
    3.26 +    Swing_Thread.require()
    3.27      apply(text_area) match {
    3.28        case None => error("No document view for text area: " + text_area)
    3.29        case Some(doc_view) =>
    3.30 @@ -86,14 +86,14 @@
    3.31  
    3.32    def extend_styles()
    3.33    {
    3.34 -    Swing_Thread.assert()
    3.35 +    Swing_Thread.require()
    3.36      styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
    3.37    }
    3.38    extend_styles()
    3.39  
    3.40    def set_styles()
    3.41    {
    3.42 -    Swing_Thread.assert()
    3.43 +    Swing_Thread.require()
    3.44      text_area.getPainter.setStyles(styles)
    3.45    }
    3.46  
    3.47 @@ -118,7 +118,7 @@
    3.48  
    3.49    def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
    3.50    {
    3.51 -    Swing_Thread.assert()
    3.52 +    Swing_Thread.require()
    3.53  
    3.54      val buffer = model.buffer
    3.55      var visible_change = false
    3.56 @@ -148,54 +148,56 @@
    3.57        first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.58        start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
    3.59      {
    3.60 -      Swing_Thread.now {
    3.61 -        val snapshot = model.snapshot()
    3.62 +      Swing_Thread.assert()
    3.63 +
    3.64 +      val snapshot = model.snapshot()
    3.65 +
    3.66 +      val command_range: Iterable[(Command, Int)] =
    3.67 +      {
    3.68 +        val range = snapshot.node.command_range(snapshot.revert(start(0)))
    3.69 +        if (range.hasNext) {
    3.70 +          val (cmd0, start0) = range.next
    3.71 +          new Iterable[(Command, Int)] {
    3.72 +            def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
    3.73 +          }
    3.74 +        }
    3.75 +        else Iterable.empty
    3.76 +      }
    3.77  
    3.78 -        val command_range: Iterable[(Command, Int)] =
    3.79 -        {
    3.80 -          val range = snapshot.node.command_range(snapshot.revert(start(0)))
    3.81 -          if (range.hasNext) {
    3.82 -            val (cmd0, start0) = range.next
    3.83 -            new Iterable[(Command, Int)] {
    3.84 -              def iterator = Document.command_starts(snapshot.node.commands.iterator(cmd0), start0)
    3.85 +      val saved_color = gfx.getColor
    3.86 +      try {
    3.87 +        var y = y0
    3.88 +        for (i <- 0 until physical_lines.length) {
    3.89 +          if (physical_lines(i) != -1) {
    3.90 +            val line_start = start(i)
    3.91 +            val line_end = model.visible_line_end(line_start, end(i))
    3.92 +
    3.93 +            val a = snapshot.revert(line_start)
    3.94 +            val b = snapshot.revert(line_end)
    3.95 +            val cmds = command_range.iterator.
    3.96 +              dropWhile { case (cmd, c) => c + cmd.length <= a } .
    3.97 +              takeWhile { case (_, c) => c < b }
    3.98 +
    3.99 +            for ((command, command_start) <- cmds if !command.is_ignored) {
   3.100 +              val p =
   3.101 +                text_area.offsetToXY(line_start max snapshot.convert(command_start))
   3.102 +              val q =
   3.103 +                text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
   3.104 +              assert(p.y == q.y)
   3.105 +              gfx.setColor(Document_View.choose_color(snapshot, command))
   3.106 +              gfx.fillRect(p.x, y, q.x - p.x, line_height)
   3.107              }
   3.108            }
   3.109 -          else Iterable.empty
   3.110 +          y += line_height
   3.111          }
   3.112 -
   3.113 -        val saved_color = gfx.getColor
   3.114 -        try {
   3.115 -          var y = y0
   3.116 -          for (i <- 0 until physical_lines.length) {
   3.117 -            if (physical_lines(i) != -1) {
   3.118 -              val line_start = start(i)
   3.119 -              val line_end = model.visible_line_end(line_start, end(i))
   3.120 -
   3.121 -              val a = snapshot.revert(line_start)
   3.122 -              val b = snapshot.revert(line_end)
   3.123 -              val cmds = command_range.iterator.
   3.124 -                dropWhile { case (cmd, c) => c + cmd.length <= a } .
   3.125 -                takeWhile { case (_, c) => c < b }
   3.126 -
   3.127 -              for ((command, command_start) <- cmds if !command.is_ignored) {
   3.128 -                val p =
   3.129 -                  text_area.offsetToXY(line_start max snapshot.convert(command_start))
   3.130 -                val q =
   3.131 -                  text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
   3.132 -                assert(p.y == q.y)
   3.133 -                gfx.setColor(Document_View.choose_color(snapshot, command))
   3.134 -                gfx.fillRect(p.x, y, q.x - p.x, line_height)
   3.135 -              }
   3.136 -            }
   3.137 -            y += line_height
   3.138 -          }
   3.139 -        }
   3.140 -        finally { gfx.setColor(saved_color) }
   3.141        }
   3.142 +      finally { gfx.setColor(saved_color) }
   3.143      }
   3.144  
   3.145      override def getToolTipText(x: Int, y: Int): String =
   3.146      {
   3.147 +      Swing_Thread.assert()
   3.148 +
   3.149        val snapshot = model.snapshot()
   3.150        val offset = snapshot.revert(text_area.xyToOffset(x, y))
   3.151        snapshot.node.command_at(offset) match {
   3.152 @@ -213,7 +215,10 @@
   3.153    /* caret handling */
   3.154  
   3.155    def selected_command(): Option[Command] =
   3.156 +  {
   3.157 +    Swing_Thread.require()
   3.158      model.snapshot().node.proper_command_at(text_area.getCaretPosition)
   3.159 +  }
   3.160  
   3.161    private val caret_listener = new CaretListener {
   3.162      private val delay = Swing_Thread.delay_last(session.input_delay) {
     4.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sat Aug 07 14:45:26 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sat Aug 07 16:15:52 2010 +0200
     4.3 @@ -40,6 +40,7 @@
     4.4  {
     4.5    def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
     4.6    {
     4.7 +    Swing_Thread.assert()
     4.8      Document_Model(buffer) match {
     4.9        case Some(model) =>
    4.10          val snapshot = model.snapshot()
     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat Aug 07 14:45:26 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sat Aug 07 16:15:52 2010 +0200
     5.3 @@ -95,7 +95,7 @@
     5.4      import Isabelle_Sidekick.int_to_pos
     5.5  
     5.6      val root = data.root
     5.7 -    val doc = model.snapshot().node  // FIXME cover all nodes (!??)
     5.8 +    val doc = Swing_Thread.now { model.snapshot().node }  // FIXME cover all nodes (!??)
     5.9      for {
    5.10        (command, command_start) <- doc.command_range(0)
    5.11        if command.is_command && !stopped
    5.12 @@ -128,7 +128,7 @@
    5.13      import Isabelle_Sidekick.int_to_pos
    5.14  
    5.15      val root = data.root
    5.16 -    val snapshot = model.snapshot()  // FIXME cover all nodes (!??)
    5.17 +    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
    5.18      for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
    5.19        root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
    5.20            {
     6.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat Aug 07 14:45:26 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat Aug 07 16:15:52 2010 +0200
     6.3 @@ -22,7 +22,7 @@
     6.4  
     6.5  class Output_Dockable(view: View, position: String) extends Dockable(view, position)
     6.6  {
     6.7 -  Swing_Thread.assert()
     6.8 +  Swing_Thread.require()
     6.9  
    6.10    val html_panel =
    6.11      new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))