src/Tools/jEdit/src/output_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56880 f8c1d2583699
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
     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 
    39   private def handle_resize()
    40   {
    41     Swing_Thread.require {}
    42 
    43     pretty_text_area.resize(
    44       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    45   }
    46 
    47   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
    48   {
    49     Swing_Thread.require {}
    50 
    51     val (new_snapshot, new_command, new_results) =
    52       PIDE.editor.current_node_snapshot(view) match {
    53         case Some(snapshot) =>
    54           if (follow && !snapshot.is_outdated) {
    55             PIDE.editor.current_command(view, snapshot) match {
    56               case Some(cmd) =>
    57                 (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd))
    58               case None =>
    59                 (Document.Snapshot.init, Command.empty, Command.Results.empty)
    60             }
    61           }
    62           else (current_snapshot, current_command, current_results)
    63         case None => (current_snapshot, current_command, current_results)
    64       }
    65 
    66     val new_output =
    67       if (!restriction.isDefined || restriction.get.contains(new_command)) {
    68         val rendering = Rendering(new_snapshot, PIDE.options.value)
    69         rendering.output_messages(new_results)
    70       }
    71       else current_output
    72 
    73     if (new_output != current_output)
    74       pretty_text_area.update(new_snapshot, new_results, Pretty.separate(new_output))
    75 
    76     current_snapshot = new_snapshot
    77     current_command = new_command
    78     current_results = new_results
    79     current_output = new_output
    80   }
    81 
    82 
    83   /* main */
    84 
    85   private val main =
    86     Session.Consumer[Any](getClass.getName) {
    87       case _: Session.Global_Options =>
    88         Swing_Thread.later { handle_resize() }
    89 
    90       case changed: Session.Commands_Changed =>
    91         val restriction = if (changed.assignment) None else Some(changed.commands)
    92         Swing_Thread.later { handle_update(do_update, restriction) }
    93 
    94       case Session.Caret_Focus =>
    95         Swing_Thread.later { handle_update(do_update, None) }
    96     }
    97 
    98   override def init()
    99   {
   100     PIDE.session.global_options += main
   101     PIDE.session.commands_changed += main
   102     PIDE.session.caret_focus += main
   103     handle_update(true, None)
   104   }
   105 
   106   override def exit()
   107   {
   108     PIDE.session.global_options -= main
   109     PIDE.session.commands_changed -= main
   110     PIDE.session.caret_focus -= main
   111     delay_resize.revoke()
   112   }
   113 
   114 
   115   /* resize */
   116 
   117   private val delay_resize =
   118     Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   119 
   120   addComponentListener(new ComponentAdapter {
   121     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   122   })
   123 
   124 
   125   /* controls */
   126 
   127   private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
   128     tooltip = "Zoom factor for output font size"
   129   }
   130 
   131   private val auto_update = new CheckBox("Auto update") {
   132     tooltip = "Indicate automatic update following cursor movement"
   133     reactions += {
   134       case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
   135     selected = do_update
   136   }
   137 
   138   private val update = new Button("Update") {
   139     tooltip = "Update display according to the command at cursor position"
   140     reactions += { case ButtonClicked(_) => handle_update(true, None) }
   141   }
   142 
   143   private val detach = new Button("Detach") {
   144     tooltip = "Detach window with static copy of current output"
   145     reactions += {
   146       case ButtonClicked(_) =>
   147         Info_Dockable(view, current_snapshot, current_results, Pretty.separate(current_output))
   148     }
   149   }
   150 
   151   private val controls =
   152     new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom)
   153   add(controls.peer, BorderLayout.NORTH)
   154 }