src/Tools/jEdit/src/jedit/output_dockable.scala
author wenzelm
Mon Aug 30 13:01:32 2010 +0200 (2010-08-30)
changeset 38872 26c505765024
parent 38360 53224a4d2f0e
child 39513 fce2202892c4
permissions -rw-r--r--
Command.results: ordered by serial number;
     1 /*  Title:      Tools/jEdit/src/jedit/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.awt.BorderLayout
    18 import java.awt.event.{ComponentEvent, ComponentAdapter}
    19 
    20 import org.gjt.sp.jedit.View
    21 
    22 
    23 class Output_Dockable(view: View, position: String) extends Dockable(view, position)
    24 {
    25   Swing_Thread.require()
    26 
    27   val html_panel =
    28     new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
    29   add(html_panel, BorderLayout.CENTER)
    30 
    31 
    32   /* component state -- owned by Swing thread */
    33 
    34   private var zoom_factor = 100
    35   private var show_debug = false
    36   private var show_tracing = false
    37   private var follow_caret = true
    38   private var current_command: Option[Command] = None
    39 
    40 
    41   private def handle_resize()
    42   {
    43     Swing_Thread.now {
    44       html_panel.resize(Isabelle.font_family(),
    45         scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    46     }
    47   }
    48 
    49   private def handle_perspective(): Boolean =
    50     Swing_Thread.now {
    51       Document_View(view.getTextArea) match {
    52         case Some(doc_view) =>
    53           val cmd = doc_view.selected_command()
    54           if (current_command == cmd) false
    55           else { current_command = cmd; true }
    56         case None => false
    57       }
    58     }
    59 
    60   private def handle_update(restriction: Option[Set[Command]] = None)
    61   {
    62     Swing_Thread.now {
    63       if (follow_caret) handle_perspective()
    64       Document_View(view.getTextArea) match {
    65         case Some(doc_view) =>
    66           current_command match {
    67             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
    68               val snapshot = doc_view.model.snapshot()
    69               val filtered_results =
    70                 snapshot.state(cmd).results.iterator.map(_._2) filter {
    71                   case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
    72                   case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
    73                   case _ => true
    74                 }
    75               html_panel.render(filtered_results.toList)
    76             case _ =>
    77           }
    78         case None =>
    79       }
    80     }
    81   }
    82 
    83 
    84   /* main actor */
    85 
    86   private val main_actor = actor {
    87     loop {
    88       react {
    89         case Session.Global_Settings => handle_resize()
    90         case Session.Commands_Changed(changed) => handle_update(Some(changed))
    91         case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
    92         case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    93       }
    94     }
    95   }
    96 
    97   override def init()
    98   {
    99     Isabelle.session.global_settings += main_actor
   100     Isabelle.session.commands_changed += main_actor
   101     Isabelle.session.perspective += main_actor
   102   }
   103 
   104   override def exit()
   105   {
   106     Isabelle.session.global_settings -= main_actor
   107     Isabelle.session.commands_changed -= main_actor
   108     Isabelle.session.perspective -= main_actor
   109   }
   110 
   111 
   112   /* resize */
   113 
   114   addComponentListener(new ComponentAdapter {
   115     val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
   116     override def componentResized(e: ComponentEvent) { delay() }
   117   })
   118 
   119 
   120   /* controls */
   121 
   122   private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   123   zoom.tooltip = "Zoom factor for basic font size"
   124 
   125   private val debug = new CheckBox("Debug") {
   126     reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
   127   }
   128   debug.selected = show_debug
   129   debug.tooltip =
   130     "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
   131 
   132   private val tracing = new CheckBox("Tracing") {
   133     reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
   134   }
   135   tracing.selected = show_tracing
   136   tracing.tooltip = "Indicate output of tracing messages"
   137 
   138   private val auto_update = new CheckBox("Auto update") {
   139     reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
   140   }
   141   auto_update.selected = follow_caret
   142   auto_update.tooltip = "Indicate automatic update following cursor movement"
   143 
   144   private val update = new Button("Update") {
   145     reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
   146   }
   147   update.tooltip = "Update display according to the command at cursor position"
   148 
   149   val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
   150   add(controls.peer, BorderLayout.NORTH)
   151 
   152   handle_update()
   153 }