src/Tools/jEdit/src/simplifier_trace_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56770 e160ae47db94
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
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@56662
    23
  Swing_Thread.require {}
lars@55316
    24
lars@55316
    25
  /* component state -- owned by Swing 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
  private var do_auto_reply = false
lars@55316
    33
lars@55316
    34
lars@55316
    35
  private val text_area = new Pretty_Text_Area(view)
lars@55316
    36
  set_content(text_area)
lars@55316
    37
lars@55316
    38
  private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
lars@55316
    39
  {
lars@55316
    40
    val data = question.data
lars@55316
    41
lars@55316
    42
    def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
lars@55316
    43
      XML.Wrapped_Elem(
lars@55316
    44
        Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
lars@55316
    45
        Nil,
lars@55316
    46
        List(XML.Text(answer.string))
lars@55316
    47
      )
lars@55316
    48
lars@55316
    49
    def make_block(body: XML.Body): XML.Body =
lars@55316
    50
      List(Pretty.Block(0, body))
lars@55316
    51
lars@55316
    52
    val all = Pretty.separate(
lars@55316
    53
      XML.Text(data.text) ::
lars@55316
    54
      data.content :::
lars@55316
    55
      make_block(Library.separate(XML.Text(", "), question.answers map make_button))
lars@55316
    56
    )
lars@55316
    57
lars@55316
    58
    XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
lars@55316
    59
  }
lars@55316
    60
lars@55316
    61
  private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
lars@55316
    62
  {
wenzelm@56662
    63
    Swing_Thread.require {}
lars@55316
    64
    val questions = context.questions.values
lars@55316
    65
    if (do_auto_reply && !questions.isEmpty)
lars@55316
    66
    {
lars@55316
    67
      questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
lars@55316
    68
      handle_update(do_update)
lars@55316
    69
    }
lars@55316
    70
    else
lars@55316
    71
    {
lars@55316
    72
      val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
lars@55316
    73
      text_area.update(snapshot, Command.Results.empty, contents)
lars@55316
    74
      do_paint()
lars@55316
    75
    }
lars@55316
    76
  }
lars@55316
    77
lars@55316
    78
  private def show_trace()
lars@55316
    79
  {
wenzelm@56299
    80
    val trace = Simplifier_Trace.generate_trace(current_results)
lars@55316
    81
    new Simplifier_Trace_Window(view, current_snapshot, trace)
lars@55316
    82
  }
lars@55316
    83
lars@55316
    84
  private def do_paint()
lars@55316
    85
  {
lars@55316
    86
    Swing_Thread.later {
wenzelm@55825
    87
      text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
lars@55316
    88
    }
lars@55316
    89
  }
lars@55316
    90
lars@55316
    91
  private def update_contents()
lars@55316
    92
  {
lars@55316
    93
    set_context(
lars@55316
    94
      current_snapshot,
wenzelm@56299
    95
      Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
lars@55316
    96
    )
lars@55316
    97
  }
lars@55316
    98
lars@55316
    99
  private def handle_resize()
lars@55316
   100
  {
lars@55316
   101
    do_paint()
lars@55316
   102
  }
lars@55316
   103
lars@55316
   104
  private def handle_update(follow: Boolean)
lars@55316
   105
  {
wenzelm@56299
   106
    val (new_snapshot, new_command, new_results, new_id) =
lars@55316
   107
      PIDE.editor.current_node_snapshot(view) match {
lars@55316
   108
        case Some(snapshot) =>
lars@55316
   109
          if (follow && !snapshot.is_outdated) {
lars@55316
   110
            PIDE.editor.current_command(view, snapshot) match {
lars@55316
   111
              case Some(cmd) =>
wenzelm@56299
   112
                (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id)
lars@55316
   113
              case None =>
wenzelm@56299
   114
                (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L)
lars@55316
   115
            }
lars@55316
   116
          }
wenzelm@56299
   117
          else (current_snapshot, current_command, current_results, current_id)
wenzelm@56299
   118
        case None => (current_snapshot, current_command, current_results, current_id)
lars@55316
   119
      }
lars@55316
   120
lars@55316
   121
    current_snapshot = new_snapshot
wenzelm@56299
   122
    current_command = new_command
wenzelm@56299
   123
    current_results = new_results
lars@55316
   124
    current_id = new_id
lars@55316
   125
    update_contents()
lars@55316
   126
  }
lars@55316
   127
lars@55316
   128
wenzelm@56715
   129
  /* main */
wenzelm@56715
   130
wenzelm@56715
   131
  private val main =
wenzelm@56715
   132
    Session.Consumer[Any](getClass.getName) {
wenzelm@56715
   133
      case _: Session.Global_Options =>
wenzelm@56715
   134
        Swing_Thread.later { handle_resize() }
lars@55316
   135
wenzelm@56715
   136
      case changed: Session.Commands_Changed =>
wenzelm@56715
   137
        Swing_Thread.later { handle_update(do_update) }
wenzelm@56715
   138
wenzelm@56715
   139
      case Session.Caret_Focus =>
wenzelm@56715
   140
        Swing_Thread.later { handle_update(do_update) }
wenzelm@56715
   141
wenzelm@56715
   142
      case Simplifier_Trace.Event =>
wenzelm@56715
   143
        Swing_Thread.later { handle_update(do_update) }
lars@55316
   144
    }
lars@55316
   145
lars@55316
   146
  override def init()
lars@55316
   147
  {
wenzelm@56662
   148
    Swing_Thread.require {}
lars@55316
   149
wenzelm@56715
   150
    PIDE.session.global_options += main
wenzelm@56715
   151
    PIDE.session.commands_changed += main
wenzelm@56715
   152
    PIDE.session.caret_focus += main
wenzelm@56715
   153
    PIDE.session.trace_events += main
lars@55316
   154
    handle_update(true)
lars@55316
   155
  }
lars@55316
   156
lars@55316
   157
  override def exit()
lars@55316
   158
  {
wenzelm@56662
   159
    Swing_Thread.require {}
lars@55316
   160
wenzelm@56715
   161
    PIDE.session.global_options -= main
wenzelm@56715
   162
    PIDE.session.commands_changed -= main
wenzelm@56715
   163
    PIDE.session.caret_focus -= main
wenzelm@56715
   164
    PIDE.session.trace_events -= main
lars@55316
   165
    delay_resize.revoke()
lars@55316
   166
  }
lars@55316
   167
lars@55316
   168
lars@55316
   169
  /* resize */
lars@55316
   170
lars@55316
   171
  private val delay_resize =
lars@55316
   172
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
lars@55316
   173
lars@55316
   174
  addComponentListener(new ComponentAdapter {
lars@55316
   175
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
lars@55316
   176
    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
lars@55316
   177
  })
lars@55316
   178
lars@55316
   179
lars@55316
   180
  /* controls */
lars@55316
   181
lars@55316
   182
  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
lars@55316
   183
    new CheckBox("Auto update") {
lars@55316
   184
      selected = do_update
lars@55316
   185
      reactions += {
lars@55316
   186
        case ButtonClicked(_) =>
lars@55316
   187
          do_update = this.selected
lars@55316
   188
          handle_update(do_update)
lars@55316
   189
      }
lars@55316
   190
    },
lars@55316
   191
    new Button("Update") {
lars@55316
   192
      reactions += {
lars@55316
   193
        case ButtonClicked(_) =>
lars@55316
   194
          handle_update(true)
lars@55316
   195
      }
lars@55316
   196
    },
lars@55316
   197
    new Separator(Orientation.Vertical),
lars@55316
   198
    new CheckBox("Auto reply") {
lars@55316
   199
      selected = do_auto_reply
lars@55316
   200
      reactions += {
lars@55316
   201
        case ButtonClicked(_) =>
lars@55316
   202
          do_auto_reply = this.selected
lars@55316
   203
          handle_update(do_update)
lars@55316
   204
      }
lars@55316
   205
    },
lars@55316
   206
    new Separator(Orientation.Vertical),
lars@55316
   207
    new Button("Show trace") {
lars@55316
   208
      reactions += {
lars@55316
   209
        case ButtonClicked(_) =>
lars@55316
   210
          show_trace()
lars@55316
   211
      }
lars@55316
   212
    },
lars@55316
   213
    new Button("Clear memory") {
lars@55316
   214
      reactions += {
lars@55316
   215
        case ButtonClicked(_) =>
lars@55316
   216
          Simplifier_Trace.clear_memory()
lars@55316
   217
      }
lars@55316
   218
    }
lars@55316
   219
  )
lars@55316
   220
lars@55316
   221
  add(controls.peer, BorderLayout.NORTH)
lars@55316
   222
}