src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 46740 852baa599351
child 47027 fc3bb6c02a3c
permissions -rw-r--r--
more explicit indication of swing thread context;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/output_dockable.scala
wenzelm@36760
     2
    Author:     Makarius
wenzelm@36760
     3
wenzelm@36760
     4
Dockable window with result message output.
wenzelm@36760
     5
*/
wenzelm@34408
     6
wenzelm@34318
     7
package isabelle.jedit
wenzelm@34318
     8
wenzelm@34760
     9
wenzelm@36015
    10
import isabelle._
wenzelm@36015
    11
wenzelm@34768
    12
import scala.actors.Actor._
wenzelm@34760
    13
wenzelm@37017
    14
import scala.swing.{FlowPanel, Button, CheckBox}
wenzelm@36988
    15
import scala.swing.event.ButtonClicked
wenzelm@36988
    16
wenzelm@43520
    17
import java.lang.System
wenzelm@37067
    18
import java.awt.BorderLayout
wenzelm@37014
    19
import java.awt.event.{ComponentEvent, ComponentAdapter}
wenzelm@34748
    20
wenzelm@34318
    21
import org.gjt.sp.jedit.View
wenzelm@34318
    22
wenzelm@34765
    23
wenzelm@37067
    24
class Output_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@34760
    25
{
wenzelm@38223
    26
  Swing_Thread.require()
wenzelm@37130
    27
wenzelm@39592
    28
  private val html_panel =
wenzelm@43661
    29
    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
krauss@42978
    30
  {
krauss@42978
    31
    override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
krauss@42978
    32
      case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
krauss@42978
    33
        val text = elem.getFirstChild().getNodeValue()
krauss@42978
    34
krauss@42978
    35
        Document_View(view.getTextArea) match {
krauss@42978
    36
          case Some(doc_view) =>
krauss@42978
    37
            val cmd = current_command.get
wenzelm@43419
    38
            val start_ofs = doc_view.update_snapshot().node.command_start(cmd).get
krauss@42978
    39
            val buffer = view.getBuffer
krauss@42978
    40
            buffer.beginCompoundEdit()
krauss@42978
    41
            buffer.remove(start_ofs, cmd.length)
krauss@42978
    42
            buffer.insert(start_ofs, text)
krauss@42978
    43
            buffer.endCompoundEdit()
krauss@42978
    44
          case None =>
krauss@42978
    45
        }
krauss@42978
    46
    }       
krauss@42978
    47
  }
krauss@42978
    48
wenzelm@39518
    49
  set_content(html_panel)
wenzelm@34768
    50
wenzelm@34768
    51
wenzelm@37130
    52
  /* component state -- owned by Swing thread */
wenzelm@36988
    53
wenzelm@37019
    54
  private var zoom_factor = 100
wenzelm@37131
    55
  private var show_tracing = false
wenzelm@37131
    56
  private var follow_caret = true
wenzelm@37131
    57
  private var current_command: Option[Command] = None
wenzelm@37019
    58
wenzelm@37131
    59
wenzelm@37131
    60
  private def handle_resize()
wenzelm@37131
    61
  {
wenzelm@37019
    62
    Swing_Thread.now {
wenzelm@37164
    63
      html_panel.resize(Isabelle.font_family(),
wenzelm@37164
    64
        scala.math.round(Isabelle.font_size() * zoom_factor / 100))
wenzelm@37019
    65
    }
wenzelm@37131
    66
  }
wenzelm@36988
    67
wenzelm@37849
    68
  private def handle_perspective(): Boolean =
wenzelm@37131
    69
    Swing_Thread.now {
wenzelm@37131
    70
      Document_View(view.getTextArea) match {
wenzelm@37849
    71
        case Some(doc_view) =>
wenzelm@37849
    72
          val cmd = doc_view.selected_command()
wenzelm@37849
    73
          if (current_command == cmd) false
wenzelm@37849
    74
          else { current_command = cmd; true }
wenzelm@37849
    75
        case None => false
wenzelm@37131
    76
      }
wenzelm@37131
    77
    }
wenzelm@37130
    78
wenzelm@37130
    79
  private def handle_update(restriction: Option[Set[Command]] = None)
wenzelm@37130
    80
  {
wenzelm@37130
    81
    Swing_Thread.now {
wenzelm@37849
    82
      if (follow_caret) handle_perspective()
wenzelm@37130
    83
      Document_View(view.getTextArea) match {
wenzelm@37130
    84
        case Some(doc_view) =>
wenzelm@37130
    85
          current_command match {
wenzelm@37130
    86
            case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
wenzelm@43419
    87
              val snapshot = doc_view.update_snapshot()
wenzelm@37130
    88
              val filtered_results =
wenzelm@46208
    89
                snapshot.state.command_state(snapshot.version, cmd).results.iterator
wenzelm@46208
    90
                  .map(_._2).filter(
wenzelm@46208
    91
                  { // FIXME not scalable
wenzelm@46208
    92
                    case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
wenzelm@46208
    93
                    case _ => true
wenzelm@46208
    94
                  }).toList
wenzelm@46208
    95
              html_panel.render(filtered_results)
wenzelm@37130
    96
            case _ =>
wenzelm@37130
    97
          }
wenzelm@37130
    98
        case None =>
wenzelm@37130
    99
      }
wenzelm@37130
   100
    }
wenzelm@37130
   101
  }
wenzelm@37130
   102
wenzelm@37130
   103
wenzelm@37067
   104
  /* main actor */
wenzelm@34768
   105
wenzelm@37067
   106
  private val main_actor = actor {
wenzelm@34768
   107
    loop {
wenzelm@34768
   108
      react {
wenzelm@37019
   109
        case Session.Global_Settings => handle_resize()
wenzelm@44608
   110
        case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
wenzelm@44805
   111
        case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update()
wenzelm@37067
   112
        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
wenzelm@34768
   113
      }
wenzelm@34768
   114
    }
wenzelm@34768
   115
  }
wenzelm@34428
   116
wenzelm@37067
   117
  override def init()
wenzelm@34777
   118
  {
wenzelm@37849
   119
    Isabelle.session.global_settings += main_actor
wenzelm@37129
   120
    Isabelle.session.commands_changed += main_actor
wenzelm@44805
   121
    Isabelle.session.caret_focus += main_actor
wenzelm@34768
   122
  }
wenzelm@34768
   123
wenzelm@37067
   124
  override def exit()
wenzelm@34777
   125
  {
wenzelm@37849
   126
    Isabelle.session.global_settings -= main_actor
wenzelm@37129
   127
    Isabelle.session.commands_changed -= main_actor
wenzelm@44805
   128
    Isabelle.session.caret_focus -= main_actor
wenzelm@46740
   129
    delay_resize(false)
wenzelm@34768
   130
  }
wenzelm@36988
   131
wenzelm@36988
   132
wenzelm@37014
   133
  /* resize */
wenzelm@37014
   134
wenzelm@46740
   135
  private val delay_resize =
wenzelm@46740
   136
    Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
wenzelm@46740
   137
wenzelm@37014
   138
  addComponentListener(new ComponentAdapter {
wenzelm@46740
   139
    override def componentResized(e: ComponentEvent) { delay_resize(true) }
wenzelm@37014
   140
  })
wenzelm@37014
   141
wenzelm@37014
   142
wenzelm@37130
   143
  /* controls */
wenzelm@37130
   144
wenzelm@37130
   145
  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
wenzelm@37130
   146
  zoom.tooltip = "Zoom factor for basic font size"
wenzelm@37130
   147
wenzelm@37130
   148
  private val tracing = new CheckBox("Tracing") {
wenzelm@37130
   149
    reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
wenzelm@37130
   150
  }
wenzelm@37130
   151
  tracing.selected = show_tracing
wenzelm@37372
   152
  tracing.tooltip = "Indicate output of tracing messages"
wenzelm@37130
   153
wenzelm@37131
   154
  private val auto_update = new CheckBox("Auto update") {
wenzelm@37130
   155
    reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
wenzelm@37130
   156
  }
wenzelm@37131
   157
  auto_update.selected = follow_caret
wenzelm@37372
   158
  auto_update.tooltip = "Indicate automatic update following cursor movement"
wenzelm@36988
   159
wenzelm@37131
   160
  private val update = new Button("Update") {
wenzelm@37849
   161
    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
wenzelm@37131
   162
  }
wenzelm@37372
   163
  update.tooltip = "Update display according to the command at cursor position"
wenzelm@37131
   164
wenzelm@39592
   165
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
wenzelm@37039
   166
  add(controls.peer, BorderLayout.NORTH)
wenzelm@37039
   167
wenzelm@36988
   168
  handle_update()
wenzelm@34318
   169
}