src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Thu May 08 00:14:06 2014 +0200 (2014-05-08)
changeset 56906 408b526911f7
parent 56886 87ebb99786ed
child 56907 0f3c375fd27c
permissions -rw-r--r--
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
     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 Swing thread */
    24 
    25   private var zoom_factor = 100
    26   private var do_update = true
    27   private var current_snapshot = Document.Snapshot.init
    28   private var current_command = Command.empty
    29   private var current_results = Command.Results.empty
    30   private var current_output: List[XML.Tree] = Nil
    31 
    32 
    33   /* pretty text area */
    34 
    35   val pretty_text_area = new Pretty_Text_Area(view)
    36   set_content(pretty_text_area)
    37 
    38   override val detach_operation = Some(() => pretty_text_area.detach)
    39 
    40 
    41   private def handle_resize()
    42   {
    43     Swing_Thread.require {}
    44 
    45     pretty_text_area.resize(
    46       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    47   }
    48 
    49   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
    50   {
    51     Swing_Thread.require {}
    52 
    53     val (new_snapshot, new_command, new_results) =
    54       PIDE.editor.current_node_snapshot(view) match {
    55         case Some(snapshot) =>
    56           if (follow && !snapshot.is_outdated) {
    57             PIDE.editor.current_command(view, snapshot) match {
    58               case Some(cmd) =>
    59                 (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd))
    60               case None =>
    61                 (Document.Snapshot.init, Command.empty, Command.Results.empty)
    62             }
    63           }
    64           else (current_snapshot, current_command, current_results)
    65         case None => (current_snapshot, current_command, current_results)
    66       }
    67 
    68     val new_output =
    69       if (!restriction.isDefined || restriction.get.contains(new_command)) {
    70         val rendering = Rendering(new_snapshot, PIDE.options.value)
    71         rendering.output_messages(new_results)
    72       }
    73       else current_output
    74 
    75     if (new_output != current_output)
    76       pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output))
    77 
    78     current_snapshot = new_snapshot
    79     current_command = new_command
    80     current_results = new_results
    81     current_output = new_output
    82   }
    83 
    84 
    85   /* main */
    86 
    87   private val main =
    88     Session.Consumer[Any](getClass.getName) {
    89       case _: Session.Global_Options =>
    90         Swing_Thread.later { handle_resize() }
    91 
    92       case changed: Session.Commands_Changed =>
    93         val restriction = if (changed.assignment) None else Some(changed.commands)
    94         Swing_Thread.later { handle_update(do_update, restriction) }
    95 
    96       case Session.Caret_Focus =>
    97         Swing_Thread.later { handle_update(do_update, None) }
    98     }
    99 
   100   override def init()
   101   {
   102     PIDE.session.global_options += main
   103     PIDE.session.commands_changed += main
   104     PIDE.session.caret_focus += main
   105     handle_update(true, None)
   106   }
   107 
   108   override def exit()
   109   {
   110     PIDE.session.global_options -= main
   111     PIDE.session.commands_changed -= main
   112     PIDE.session.caret_focus -= main
   113     delay_resize.revoke()
   114   }
   115 
   116 
   117   /* resize */
   118 
   119   private val delay_resize =
   120     Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   121 
   122   addComponentListener(new ComponentAdapter {
   123     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   124   })
   125 
   126 
   127   /* controls */
   128 
   129   private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
   130     tooltip = "Zoom factor for output font size"
   131   }
   132 
   133   private val auto_update = new CheckBox("Auto update") {
   134     tooltip = "Indicate automatic update following cursor movement"
   135     reactions += {
   136       case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
   137     selected = do_update
   138   }
   139 
   140   private val update = new Button("Update") {
   141     tooltip = "Update display according to the command at cursor position"
   142     reactions += { case ButtonClicked(_) => handle_update(true, None) }
   143   }
   144 
   145   private val controls =
   146     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   147       auto_update, update, pretty_text_area.detach_button,
   148       pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
   149   add(controls.peer, BorderLayout.NORTH)
   150 }