1/* Title: Tools/jEdit/src/state_dockable.scala 2 Author: Makarius 3 4Dockable window for proof state output. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11import isabelle.jedit_base.Dockable 12 13import scala.swing.{Button, CheckBox} 14import scala.swing.event.ButtonClicked 15 16import java.awt.BorderLayout 17import java.awt.event.{ComponentEvent, ComponentAdapter} 18 19import org.gjt.sp.jedit.View 20 21 22class State_Dockable(view: View, position: String) extends Dockable(view, position) 23{ 24 GUI_Thread.require {} 25 26 27 /* text area */ 28 29 val pretty_text_area = new Pretty_Text_Area(view) 30 set_content(pretty_text_area) 31 32 override def detach_operation = pretty_text_area.detach_operation 33 34 private val print_state = 35 new Query_Operation(PIDE.editor, view, "print_state", _ => (), 36 (snapshot, results, body) => 37 pretty_text_area.update(snapshot, results, Pretty.separate(body))) 38 39 40 /* resize */ 41 42 private val delay_resize = 43 GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } 44 45 addComponentListener(new ComponentAdapter { 46 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } 47 override def componentShown(e: ComponentEvent) { delay_resize.invoke() } 48 }) 49 50 private def handle_resize() 51 { 52 GUI_Thread.require {} 53 54 pretty_text_area.resize( 55 Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) 56 } 57 58 59 /* update */ 60 61 def update_request(): Unit = 62 GUI_Thread.require { print_state.apply_query(Nil) } 63 64 def update() 65 { 66 GUI_Thread.require {} 67 68 PIDE.editor.current_node_snapshot(view) match { 69 case Some(snapshot) => 70 (PIDE.editor.current_command(view, snapshot), print_state.get_location) match { 71 case (Some(command1), Some(command2)) if command1.id == command2.id => 72 case _ => update_request() 73 } 74 case None => 75 } 76 } 77 78 79 /* auto update */ 80 81 private var auto_update_enabled = true 82 83 private def auto_update(): Unit = 84 GUI_Thread.require { if (auto_update_enabled) update() } 85 86 87 /* controls */ 88 89 private val auto_update_button = new CheckBox("Auto update") { 90 tooltip = "Indicate automatic update following cursor movement" 91 reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() } 92 selected = auto_update_enabled 93 } 94 95 private val update_button = new Button("<html><b>Update</b></html>") { 96 tooltip = "Update display according to the command at cursor position" 97 reactions += { case ButtonClicked(_) => update_request() } 98 } 99 100 private val locate_button = new Button("Locate") { 101 tooltip = "Locate printed command within source text" 102 reactions += { case ButtonClicked(_) => print_state.locate_query() } 103 } 104 105 private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } 106 107 private val controls = 108 Wrap_Panel( 109 List(auto_update_button, update_button, 110 locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)) 111 112 add(controls.peer, BorderLayout.NORTH) 113 114 115 /* main */ 116 117 private val main = 118 Session.Consumer[Any](getClass.getName) { 119 case _: Session.Global_Options => 120 GUI_Thread.later { handle_resize() } 121 122 case changed: Session.Commands_Changed => 123 if (changed.assignment) GUI_Thread.later { auto_update() } 124 125 case Session.Caret_Focus => 126 GUI_Thread.later { auto_update() } 127 } 128 129 override def init() 130 { 131 PIDE.session.global_options += main 132 PIDE.session.commands_changed += main 133 PIDE.session.caret_focus += main 134 handle_resize() 135 print_state.activate() 136 auto_update() 137 } 138 139 override def exit() 140 { 141 print_state.deactivate() 142 PIDE.session.caret_focus -= main 143 PIDE.session.global_options -= main 144 PIDE.session.commands_changed -= main 145 delay_resize.revoke() 146 } 147} 148