src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 43661 39fdbd814c7f
child 44582 479c07072992
permissions -rw-r--r--
propagate editor perspective through document model;
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@38872
    89
                snapshot.state(cmd).results.iterator.map(_._2) filter {
wenzelm@39513
    90
                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
wenzelm@37130
    91
                  case _ => true
wenzelm@37130
    92
                }
wenzelm@38872
    93
              html_panel.render(filtered_results.toList)
wenzelm@37130
    94
            case _ =>
wenzelm@37130
    95
          }
wenzelm@37130
    96
        case None =>
wenzelm@37130
    97
      }
wenzelm@37130
    98
    }
wenzelm@37130
    99
  }
wenzelm@37130
   100
wenzelm@37130
   101
wenzelm@37067
   102
  /* main actor */
wenzelm@34768
   103
wenzelm@37067
   104
  private val main_actor = actor {
wenzelm@34768
   105
    loop {
wenzelm@34768
   106
      react {
wenzelm@37019
   107
        case Session.Global_Settings => handle_resize()
wenzelm@38360
   108
        case Session.Commands_Changed(changed) => handle_update(Some(changed))
wenzelm@37850
   109
        case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
wenzelm@37067
   110
        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
wenzelm@34768
   111
      }
wenzelm@34768
   112
    }
wenzelm@34768
   113
  }
wenzelm@34428
   114
wenzelm@37067
   115
  override def init()
wenzelm@34777
   116
  {
wenzelm@37849
   117
    Isabelle.session.global_settings += main_actor
wenzelm@37129
   118
    Isabelle.session.commands_changed += main_actor
wenzelm@37849
   119
    Isabelle.session.perspective += main_actor
wenzelm@34768
   120
  }
wenzelm@34768
   121
wenzelm@37067
   122
  override def exit()
wenzelm@34777
   123
  {
wenzelm@37849
   124
    Isabelle.session.global_settings -= main_actor
wenzelm@37129
   125
    Isabelle.session.commands_changed -= main_actor
wenzelm@37849
   126
    Isabelle.session.perspective -= main_actor
wenzelm@34768
   127
  }
wenzelm@36988
   128
wenzelm@36988
   129
wenzelm@37014
   130
  /* resize */
wenzelm@37014
   131
wenzelm@37014
   132
  addComponentListener(new ComponentAdapter {
wenzelm@37849
   133
    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
wenzelm@37014
   134
    override def componentResized(e: ComponentEvent) { delay() }
wenzelm@37014
   135
  })
wenzelm@37014
   136
wenzelm@37014
   137
wenzelm@37130
   138
  /* controls */
wenzelm@37130
   139
wenzelm@37130
   140
  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
wenzelm@37130
   141
  zoom.tooltip = "Zoom factor for basic font size"
wenzelm@37130
   142
wenzelm@37130
   143
  private val tracing = new CheckBox("Tracing") {
wenzelm@37130
   144
    reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
wenzelm@37130
   145
  }
wenzelm@37130
   146
  tracing.selected = show_tracing
wenzelm@37372
   147
  tracing.tooltip = "Indicate output of tracing messages"
wenzelm@37130
   148
wenzelm@37131
   149
  private val auto_update = new CheckBox("Auto update") {
wenzelm@37130
   150
    reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
wenzelm@37130
   151
  }
wenzelm@37131
   152
  auto_update.selected = follow_caret
wenzelm@37372
   153
  auto_update.tooltip = "Indicate automatic update following cursor movement"
wenzelm@36988
   154
wenzelm@37131
   155
  private val update = new Button("Update") {
wenzelm@37849
   156
    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
wenzelm@37131
   157
  }
wenzelm@37372
   158
  update.tooltip = "Update display according to the command at cursor position"
wenzelm@37131
   159
wenzelm@39592
   160
  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
wenzelm@37039
   161
  add(controls.peer, BorderLayout.NORTH)
wenzelm@37039
   162
wenzelm@36988
   163
  handle_update()
wenzelm@34318
   164
}