src/Tools/jEdit/src/info_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 60750 7694aa52ad56
child 64865 778c64c17363
permissions -rw-r--r--
tuned signature;
     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 GUI 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     GUI_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 GUI thread */
    52 
    53   private val snapshot = Info_Dockable.implicit_snapshot
    54   private val results = Info_Dockable.implicit_results
    55   private val info = Info_Dockable.implicit_info
    56 
    57   private val window_focus_listener =
    58     new WindowFocusListener {
    59       def windowGainedFocus(e: WindowEvent) { Info_Dockable.set_implicit(snapshot, results, info) }
    60       def windowLostFocus(e: WindowEvent) { Info_Dockable.reset_implicit() }
    61     }
    62 
    63 
    64   /* pretty text area */
    65 
    66   private val pretty_text_area = new Pretty_Text_Area(view)
    67   set_content(pretty_text_area)
    68 
    69   pretty_text_area.update(snapshot, results, info)
    70 
    71   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
    72 
    73   private def handle_resize()
    74   {
    75     GUI_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     GUI_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     override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
    90   })
    91 
    92   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    93     pretty_text_area.search_label, pretty_text_area.search_field, zoom)
    94   add(controls.peer, BorderLayout.NORTH)
    95 
    96 
    97   /* main */
    98 
    99   private val main =
   100     Session.Consumer[Session.Global_Options](getClass.getName) {
   101       case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
   102     }
   103 
   104   override def init()
   105   {
   106     GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
   107     PIDE.session.global_options += main
   108     handle_resize()
   109   }
   110 
   111   override def exit()
   112   {
   113     GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
   114     PIDE.session.global_options -= main
   115     delay_resize.revoke()
   116   }
   117 }