src/Tools/jEdit/src/info_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56883 38c6b70e5e53
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
     1 /*  Title:      Tools/jEdit/src/info_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window with info text.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.swing.Button
    13 import scala.swing.event.ButtonClicked
    14 
    15 import java.awt.BorderLayout
    16 import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
    17 
    18 import org.gjt.sp.jedit.View
    19 
    20 
    21 object Info_Dockable
    22 {
    23   /* implicit arguments -- owned by Swing thread */
    24 
    25   private var implicit_snapshot = Document.Snapshot.init
    26   private var implicit_results = Command.Results.empty
    27   private var implicit_info: XML.Body = Nil
    28 
    29   private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
    30   {
    31     Swing_Thread.require {}
    32 
    33     implicit_snapshot = snapshot
    34     implicit_results = results
    35     implicit_info = info
    36   }
    37 
    38   private def reset_implicit(): Unit =
    39     set_implicit(Document.Snapshot.init, Command.Results.empty, Nil)
    40 
    41   def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
    42   {
    43     set_implicit(snapshot, results, info)
    44     view.getDockableWindowManager.floatDockableWindow("isabelle-info")
    45   }
    46 }
    47 
    48 
    49 class Info_Dockable(view: View, position: String) extends Dockable(view, position)
    50 {
    51   /* component state -- owned by Swing thread */
    52 
    53   private var zoom_factor = 100
    54 
    55   private val snapshot = Info_Dockable.implicit_snapshot
    56   private val results = Info_Dockable.implicit_results
    57   private val info = Info_Dockable.implicit_info
    58 
    59   private val window_focus_listener =
    60     new WindowFocusListener {
    61       def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) }
    62       def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
    63     }
    64 
    65 
    66   /* pretty text area */
    67 
    68   private val pretty_text_area = new Pretty_Text_Area(view)
    69   set_content(pretty_text_area)
    70 
    71   pretty_text_area.update(snapshot, results, info)
    72 
    73   private def handle_resize()
    74   {
    75     Swing_Thread.require {}
    76 
    77     pretty_text_area.resize(
    78       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    79   }
    80 
    81 
    82   /* resize */
    83 
    84   private val delay_resize =
    85     Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    86 
    87   addComponentListener(new ComponentAdapter {
    88     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    89   })
    90 
    91   private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    92   zoom.tooltip = "Zoom factor for basic font size"
    93 
    94   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
    95   add(controls.peer, BorderLayout.NORTH)
    96 
    97 
    98   /* main */
    99 
   100   private val main =
   101     Session.Consumer[Session.Global_Options](getClass.getName) {
   102       case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
   103     }
   104 
   105   override def init()
   106   {
   107     GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
   108     PIDE.session.global_options += main
   109     handle_resize()
   110   }
   111 
   112   override def exit()
   113   {
   114     GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
   115     PIDE.session.global_options -= main
   116     delay_resize.revoke()
   117   }
   118 }