src/Tools/jEdit/src/jedit/output_dockable.scala
author wenzelm
Fri May 28 17:48:18 2010 +0200 (2010-05-28 ago)
changeset 37164 8b4617ad1593
parent 37132 10ef4da1c314
child 37372 babe498016e8
permissions -rw-r--r--
reuse main view.font from jEdit;
     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.assert()
    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_caret()
    50   {
    51     Swing_Thread.now {
    52       Document_View(view.getTextArea) match {
    53         case Some(doc_view) => current_command = doc_view.selected_command
    54         case None =>
    55       }
    56     }
    57   }
    58 
    59   private def handle_update(restriction: Option[Set[Command]] = None)
    60   {
    61     Swing_Thread.now {
    62       if (follow_caret) handle_caret()
    63       Document_View(view.getTextArea) match {
    64         case Some(doc_view) =>
    65           current_command match {
    66             case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
    67               val document = doc_view.model.recent_document
    68               val filtered_results =
    69                 document.current_state(cmd).results filter {
    70                   case XML.Elem(Markup.TRACING, _, _) => show_tracing
    71                   case XML.Elem(Markup.DEBUG, _, _) => show_debug
    72                   case _ => true
    73                 }
    74               html_panel.render(filtered_results)
    75             case _ =>
    76           }
    77         case None =>
    78       }
    79     }
    80   }
    81 
    82 
    83   /* main actor */
    84 
    85   private val main_actor = actor {
    86     loop {
    87       react {
    88         case Session.Global_Settings => handle_resize()
    89         case Command_Set(changed) => handle_update(Some(changed))
    90         case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    91       }
    92     }
    93   }
    94 
    95   override def init()
    96   {
    97     Isabelle.session.commands_changed += main_actor
    98     Isabelle.session.global_settings += main_actor
    99   }
   100 
   101   override def exit()
   102   {
   103     Isabelle.session.commands_changed -= main_actor
   104     Isabelle.session.global_settings -= main_actor
   105   }
   106 
   107 
   108   /* resize */
   109 
   110   addComponentListener(new ComponentAdapter {
   111     val delay = Swing_Thread.delay_last(500) { handle_resize() }  // FIXME update_delay property
   112     override def componentResized(e: ComponentEvent) { delay() }
   113   })
   114 
   115 
   116   /* controls */
   117 
   118   private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   119   zoom.tooltip = "Zoom factor for basic font size"
   120 
   121   private val debug = new CheckBox("Debug") {
   122     reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
   123   }
   124   debug.selected = show_debug
   125   debug.tooltip =
   126     "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
   127 
   128   private val tracing = new CheckBox("Tracing") {
   129     reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
   130   }
   131   tracing.selected = show_tracing
   132   tracing.tooltip =
   133     "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
   134 
   135   private val auto_update = new CheckBox("Auto update") {
   136     reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
   137   }
   138   auto_update.selected = follow_caret
   139   auto_update.tooltip = "<html>Indicate automatic update following cursor movement</html>"
   140 
   141   private val update = new Button("Update") {
   142     reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
   143   }
   144   update.tooltip = "<html>Update display according to the command at cursor position</html>"
   145 
   146   val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
   147   add(controls.peer, BorderLayout.NORTH)
   148 
   149   handle_update()
   150 }