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