1/* Title: Tools/jEdit/src/simplifier_trace_dockable.scala 2 Author: Lars Hupel 3 4Dockable window with interactive simplifier trace. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11import isabelle.jedit_base.Dockable 12 13import scala.swing.{Button, CheckBox, Orientation, Separator} 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 Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) 23{ 24 GUI_Thread.require {} 25 26 27 /* component state -- owned by GUI thread */ 28 29 private var current_snapshot = Document.State.init.snapshot() 30 private var current_command = Command.empty 31 private var current_results = Command.Results.empty 32 private var current_id = 0L 33 private var do_update = true 34 35 36 private val text_area = new Pretty_Text_Area(view) 37 set_content(text_area) 38 39 private def update_contents() 40 { 41 val snapshot = current_snapshot 42 val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results) 43 44 answers.contents.clear() 45 context.questions.values.toList match { 46 case q :: _ => 47 val data = q.data 48 val content = Pretty.separate(XML.Text(data.text) :: data.content) 49 text_area.update(snapshot, Command.Results.empty, content) 50 q.answers.foreach { answer => 51 answers.contents += new Button(answer.string) { 52 reactions += { 53 case ButtonClicked(_) => 54 Simplifier_Trace.send_reply(PIDE.session, data.serial, answer) 55 } 56 } 57 } 58 case Nil => 59 text_area.update(snapshot, Command.Results.empty, Nil) 60 } 61 62 do_paint() 63 } 64 65 private def show_trace() 66 { 67 val trace = Simplifier_Trace.generate_trace(current_results) 68 new Simplifier_Trace_Window(view, current_snapshot, trace) 69 } 70 71 private def do_paint() 72 { 73 GUI_Thread.later { 74 text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale"))) 75 } 76 } 77 78 private def handle_resize() 79 { 80 do_paint() 81 } 82 83 private def handle_update(follow: Boolean) 84 { 85 val (new_snapshot, new_command, new_results, new_id) = 86 PIDE.editor.current_node_snapshot(view) match { 87 case Some(snapshot) => 88 if (follow && !snapshot.is_outdated) { 89 PIDE.editor.current_command(view, snapshot) match { 90 case Some(cmd) => 91 (snapshot, cmd, snapshot.command_results(cmd), cmd.id) 92 case None => 93 (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L) 94 } 95 } 96 else (current_snapshot, current_command, current_results, current_id) 97 case None => (current_snapshot, current_command, current_results, current_id) 98 } 99 100 current_snapshot = new_snapshot 101 current_command = new_command 102 current_results = new_results 103 current_id = new_id 104 update_contents() 105 } 106 107 108 /* main */ 109 110 private val main = 111 Session.Consumer[Any](getClass.getName) { 112 case _: Session.Global_Options => 113 GUI_Thread.later { handle_resize() } 114 115 case changed: Session.Commands_Changed => 116 GUI_Thread.later { handle_update(do_update) } 117 118 case Session.Caret_Focus => 119 GUI_Thread.later { handle_update(do_update) } 120 121 case Simplifier_Trace.Event => 122 GUI_Thread.later { handle_update(do_update) } 123 } 124 125 override def init() 126 { 127 PIDE.session.global_options += main 128 PIDE.session.commands_changed += main 129 PIDE.session.caret_focus += main 130 PIDE.session.trace_events += main 131 handle_update(true) 132 } 133 134 override def exit() 135 { 136 PIDE.session.global_options -= main 137 PIDE.session.commands_changed -= main 138 PIDE.session.caret_focus -= main 139 PIDE.session.trace_events -= main 140 delay_resize.revoke() 141 } 142 143 144 /* resize */ 145 146 private val delay_resize = 147 GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } 148 149 addComponentListener(new ComponentAdapter { 150 override def componentResized(e: ComponentEvent) { delay_resize.invoke() } 151 override def componentShown(e: ComponentEvent) { delay_resize.invoke() } 152 }) 153 154 155 /* controls */ 156 157 private val controls = 158 Wrap_Panel( 159 List( 160 new CheckBox("Auto update") { 161 selected = do_update 162 reactions += { 163 case ButtonClicked(_) => 164 do_update = this.selected 165 handle_update(do_update) 166 } 167 }, 168 new Button("Update") { 169 reactions += { 170 case ButtonClicked(_) => 171 handle_update(true) 172 } 173 }, 174 new Separator(Orientation.Vertical), 175 new Button("Show trace") { 176 reactions += { 177 case ButtonClicked(_) => 178 show_trace() 179 } 180 }, 181 new Button("Clear memory") { 182 reactions += { 183 case ButtonClicked(_) => 184 Simplifier_Trace.clear_memory() 185 } 186 })) 187 188 private val answers = Wrap_Panel(Nil, Wrap_Panel.Alignment.Left) 189 190 add(controls.peer, BorderLayout.NORTH) 191 add(answers.peer, BorderLayout.SOUTH) 192} 193