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