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