src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 65190 0dd2ad9dbfc2
permissions -rw-r--r--
tuned signature;
     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.swing.{Button, CheckBox}
    13 import scala.swing.event.ButtonClicked
    14 
    15 import java.awt.BorderLayout
    16 import java.awt.event.{ComponentEvent, ComponentAdapter}
    17 
    18 import org.gjt.sp.jedit.View
    19 
    20 
    21 class Output_Dockable(view: View, position: String) extends Dockable(view, position)
    22 {
    23   /* component state -- owned by GUI thread */
    24 
    25   private var do_update = true
    26   private var current_snapshot = Document.Snapshot.init
    27   private var current_command = Command.empty
    28   private var current_results = Command.Results.empty
    29   private var current_output: List[XML.Tree] = Nil
    30 
    31 
    32   /* pretty text area */
    33 
    34   val pretty_text_area = new Pretty_Text_Area(view)
    35   set_content(pretty_text_area)
    36 
    37   override def detach_operation = pretty_text_area.detach_operation
    38 
    39 
    40   private def handle_resize()
    41   {
    42     GUI_Thread.require {}
    43 
    44     pretty_text_area.resize(
    45       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    46   }
    47 
    48   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
    49   {
    50     GUI_Thread.require {}
    51 
    52     val (new_snapshot, new_command, new_results) =
    53       PIDE.editor.current_node_snapshot(view) match {
    54         case Some(snapshot) =>
    55           if (follow && !snapshot.is_outdated) {
    56             PIDE.editor.current_command(view, snapshot) match {
    57               case Some(cmd) =>
    58                 (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd))
    59               case None =>
    60                 (Document.Snapshot.init, Command.empty, Command.Results.empty)
    61             }
    62           }
    63           else (current_snapshot, current_command, current_results)
    64         case None => (current_snapshot, current_command, current_results)
    65       }
    66 
    67     val new_output =
    68       if (!restriction.isDefined || restriction.get.contains(new_command)) {
    69         val rendering = JEdit_Rendering(new_snapshot, PIDE.options.value)
    70         rendering.output_messages(new_results)
    71       }
    72       else current_output
    73 
    74     if (new_output != current_output)
    75       pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output))
    76 
    77     current_snapshot = new_snapshot
    78     current_command = new_command
    79     current_results = new_results
    80     current_output = new_output
    81   }
    82 
    83 
    84   /* controls */
    85 
    86   /* output state */
    87 
    88   private def output_state: Boolean = PIDE.options.bool("editor_output_state")
    89   private def output_state_=(b: Boolean)
    90   {
    91     if (output_state != b) {
    92       PIDE.options.bool("editor_output_state") = b
    93       PIDE.session.update_options(PIDE.options.value)
    94       PIDE.editor.flush(hidden = true)
    95       PIDE.editor.flush()
    96     }
    97   }
    98 
    99   private val output_state_button = new CheckBox("Proof state")
   100   {
   101     tooltip = "Output of proof state (normally shown on State panel)"
   102     reactions += { case ButtonClicked(_) => output_state = selected }
   103     selected = output_state
   104   }
   105 
   106   private val auto_update_button = new CheckBox("Auto update") {
   107     tooltip = "Indicate automatic update following cursor movement"
   108     reactions += {
   109       case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
   110     selected = do_update
   111   }
   112 
   113   private val update_button = new Button("Update") {
   114     tooltip = "Update display according to the command at cursor position"
   115     reactions += { case ButtonClicked(_) => handle_update(true, None) }
   116   }
   117 
   118   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
   119 
   120   private val controls =
   121     new Wrap_Panel(Wrap_Panel.Alignment.Right)(output_state_button, auto_update_button,
   122       update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   123   add(controls.peer, BorderLayout.NORTH)
   124 
   125 
   126   /* main */
   127 
   128   private val main =
   129     Session.Consumer[Any](getClass.getName) {
   130       case _: Session.Global_Options =>
   131         GUI_Thread.later {
   132           handle_resize()
   133           output_state_button.selected = output_state
   134           handle_update(do_update, None)
   135         }
   136 
   137       case changed: Session.Commands_Changed =>
   138         val restriction = if (changed.assignment) None else Some(changed.commands)
   139         GUI_Thread.later { handle_update(do_update, restriction) }
   140 
   141       case Session.Caret_Focus =>
   142         GUI_Thread.later { handle_update(do_update, None) }
   143     }
   144 
   145   override def init()
   146   {
   147     PIDE.session.global_options += main
   148     PIDE.session.commands_changed += main
   149     PIDE.session.caret_focus += main
   150     handle_update(true, None)
   151   }
   152 
   153   override def exit()
   154   {
   155     PIDE.session.global_options -= main
   156     PIDE.session.commands_changed -= main
   157     PIDE.session.caret_focus -= main
   158     delay_resize.revoke()
   159   }
   160 
   161 
   162   /* resize */
   163 
   164   private val delay_resize =
   165     GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   166 
   167   addComponentListener(new ComponentAdapter {
   168     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   169     override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   170   })
   171 }