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