src/Tools/jEdit/src/simplifier_trace_window.scala
author wenzelm
Tue Feb 18 18:29:02 2014 +0100 (2014-02-18)
changeset 55553 99409ccbe04a
parent 55316 885500f4aa6a
child 55556 60ba93d8f9e5
permissions -rw-r--r--
more standard names for protocol and markup elements;
lars@55316
     1
/*  Title:      Tools/jEdit/src/simplifier_trace_window.scala
lars@55316
     2
    Author:     Lars Hupel
lars@55316
     3
lars@55316
     4
Trace window with tree-style view of the 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.annotation.tailrec
lars@55316
    13
import scala.collection.immutable.SortedMap
lars@55316
    14
import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
lars@55316
    15
import scala.swing.event.{Key, KeyPressed}
lars@55316
    16
import scala.util.matching.Regex
lars@55316
    17
lars@55316
    18
import java.awt.BorderLayout
lars@55316
    19
import java.awt.event.{ComponentEvent, ComponentAdapter}
lars@55316
    20
lars@55316
    21
import javax.swing.SwingUtilities
lars@55316
    22
lars@55316
    23
import org.gjt.sp.jedit.View
lars@55316
    24
wenzelm@55553
    25
lars@55316
    26
private object Simplifier_Trace_Window
lars@55316
    27
{
lars@55316
    28
  sealed trait Trace_Tree
lars@55316
    29
  {
lars@55316
    30
    var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
lars@55316
    31
    val serial: Long
lars@55316
    32
    val parent: Option[Trace_Tree]
wenzelm@55553
    33
    var hints: List[Simplifier_Trace.Item.Data]
lars@55316
    34
    def set_interesting(): Unit
lars@55316
    35
  }
lars@55316
    36
lars@55316
    37
  final class Root_Tree(val serial: Long) extends Trace_Tree
lars@55316
    38
  {
lars@55316
    39
    val parent = None
lars@55316
    40
    val hints = Nil
wenzelm@55553
    41
    def hints_=(xs: List[Simplifier_Trace.Item.Data]) =
wenzelm@55553
    42
      throw new IllegalStateException("Root_Tree.hints")
lars@55316
    43
    def set_interesting() = ()
lars@55316
    44
lars@55316
    45
    def format(regex: Option[Regex]): XML.Body =
lars@55316
    46
      Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
lars@55316
    47
  }
lars@55316
    48
wenzelm@55553
    49
  final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
wenzelm@55553
    50
    extends Trace_Tree
lars@55316
    51
  {
lars@55316
    52
    val serial = data.serial
wenzelm@55553
    53
    var hints = List.empty[Simplifier_Trace.Item.Data]
lars@55316
    54
    var interesting: Boolean = false
lars@55316
    55
lars@55316
    56
    def set_interesting(): Unit =
lars@55316
    57
      if (!interesting)
lars@55316
    58
      {
lars@55316
    59
        interesting = true
lars@55316
    60
        parent match {
lars@55316
    61
          case Some(p) =>
lars@55316
    62
            p.set_interesting()
lars@55316
    63
          case None =>
lars@55316
    64
        }
lars@55316
    65
      }
lars@55316
    66
lars@55316
    67
    def format(regex: Option[Regex]): (Boolean, XML.Tree) =
lars@55316
    68
    {
lars@55316
    69
      def format_child(child: Elem_Tree): Option[XML.Tree] = child.format(regex) match {
lars@55316
    70
        case (false, _) =>
lars@55316
    71
          None
lars@55316
    72
        case (true, res) =>
lars@55316
    73
          Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
lars@55316
    74
      }
lars@55316
    75
wenzelm@55553
    76
      def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
lars@55316
    77
        Pretty.block(Pretty.separate(
lars@55316
    78
          XML.Text(data.text) ::
lars@55316
    79
          data.content
lars@55316
    80
        ))
lars@55316
    81
lars@55316
    82
      def body_contains(regex: Regex, body: XML.Body): Boolean =
lars@55316
    83
        body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
lars@55316
    84
lars@55316
    85
      val children_bodies: XML.Body =
lars@55316
    86
        children.values.filter(_.interesting).flatMap(format_child).toList
lars@55316
    87
lars@55316
    88
      lazy val hint_bodies: XML.Body =
lars@55316
    89
        hints.reverse.map(format_hint)
lars@55316
    90
lars@55316
    91
      val eligible = regex match {
lars@55316
    92
        case None =>
lars@55316
    93
          true
lars@55316
    94
        case Some(r) =>
lars@55316
    95
          body_contains(r, data.content) || hints.exists(h => body_contains(r, h.content))
lars@55316
    96
      }
lars@55316
    97
lars@55316
    98
      val all =
lars@55316
    99
        if (eligible)
lars@55316
   100
          XML.Text(data.text) :: data.content ::: children_bodies ::: hint_bodies
lars@55316
   101
        else
lars@55316
   102
          XML.Text(data.text) :: children_bodies
lars@55316
   103
lars@55316
   104
      val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
lars@55316
   105
lars@55316
   106
      (eligible || children_bodies != Nil, res)
lars@55316
   107
    }
lars@55316
   108
  }
lars@55316
   109
lars@55316
   110
  @tailrec
wenzelm@55553
   111
  def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
lars@55316
   112
    rest match {
lars@55316
   113
      case Nil =>
lars@55316
   114
        ()
lars@55316
   115
      case head :: tail =>
lars@55316
   116
        lookup.get(head.parent) match {
lars@55316
   117
          case Some(parent) =>
wenzelm@55553
   118
            if (head.markup == Markup.SIMP_TRACE_HINT)
lars@55316
   119
            {
lars@55316
   120
              parent.hints ::= head
lars@55316
   121
              walk_trace(tail, lookup)
lars@55316
   122
            }
wenzelm@55553
   123
            else if (head.markup == Markup.SIMP_TRACE_IGNORE)
lars@55316
   124
            {
lars@55316
   125
              parent.parent match {
lars@55316
   126
                case None =>
lars@55316
   127
                  System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
lars@55316
   128
                case Some(tree) =>
lars@55316
   129
                  tree.children -= head.parent
lars@55316
   130
                  walk_trace(tail, lookup) // FIXME discard from lookup
lars@55316
   131
              }
lars@55316
   132
            }
lars@55316
   133
            else
lars@55316
   134
            {
lars@55316
   135
              val entry = new Elem_Tree(head, Some(parent))
lars@55316
   136
              parent.children += ((head.serial, entry))
wenzelm@55553
   137
              if (head.markup == Markup.SIMP_TRACE_STEP || head.markup == Markup.SIMP_TRACE_LOG)
lars@55316
   138
                entry.set_interesting()
lars@55316
   139
              walk_trace(tail, lookup + (head.serial -> entry))
lars@55316
   140
            }
lars@55316
   141
lars@55316
   142
          case None =>
lars@55316
   143
            System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent)
lars@55316
   144
        }
lars@55316
   145
    }
lars@55316
   146
lars@55316
   147
}
lars@55316
   148
lars@55316
   149
class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
lars@55316
   150
{
lars@55316
   151
lars@55316
   152
  import Simplifier_Trace_Window._
lars@55316
   153
lars@55316
   154
  Swing_Thread.require()
lars@55316
   155
lars@55316
   156
  val area = new Pretty_Text_Area(view)
lars@55316
   157
lars@55316
   158
  size = new Dimension(500, 500)
lars@55316
   159
  contents = new BorderPanel {
lars@55316
   160
    layout(Component.wrap(area)) = BorderPanel.Position.Center
lars@55316
   161
  }
lars@55316
   162
lars@55316
   163
  private val tree = trace.entries.headOption match {
lars@55316
   164
    case Some(first) =>
lars@55316
   165
      val tree = new Root_Tree(first.parent)
lars@55316
   166
      walk_trace(trace.entries, Map(first.parent -> tree))
lars@55316
   167
      tree
lars@55316
   168
    case None =>
lars@55316
   169
      new Root_Tree(0)
lars@55316
   170
  }
lars@55316
   171
lars@55316
   172
  do_update(None)
lars@55316
   173
  open()
lars@55316
   174
  do_paint()
lars@55316
   175
lars@55316
   176
  def do_update(regex: Option[Regex])
lars@55316
   177
  {
lars@55316
   178
    val xml = tree.format(regex)
lars@55316
   179
    area.update(snapshot, Command.Results.empty, xml)
lars@55316
   180
  }
lars@55316
   181
lars@55316
   182
  def do_paint()
lars@55316
   183
  {
lars@55316
   184
    Swing_Thread.later {
lars@55316
   185
      area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
lars@55316
   186
    }
lars@55316
   187
  }
lars@55316
   188
lars@55316
   189
  def handle_resize()
lars@55316
   190
  {
lars@55316
   191
    do_paint()
lars@55316
   192
  }
lars@55316
   193
lars@55316
   194
lars@55316
   195
  /* resize */
lars@55316
   196
lars@55316
   197
  private val delay_resize =
lars@55316
   198
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
lars@55316
   199
lars@55316
   200
  peer.addComponentListener(new ComponentAdapter {
lars@55316
   201
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
lars@55316
   202
    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
lars@55316
   203
  })
lars@55316
   204
lars@55316
   205
lars@55316
   206
  /* controls */
lars@55316
   207
lars@55316
   208
  val use_regex = new CheckBox("Regex")
lars@55316
   209
lars@55316
   210
  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
lars@55316
   211
    new Label {
lars@55316
   212
      text = "Search"
lars@55316
   213
    },
lars@55316
   214
    new TextField(30) {
lars@55316
   215
      listenTo(keys)
lars@55316
   216
      reactions += {
lars@55316
   217
        case KeyPressed(_, Key.Enter, 0, _) =>
lars@55316
   218
          val input = text.trim
lars@55316
   219
          val regex =
lars@55316
   220
            if (input.isEmpty)
lars@55316
   221
              None
lars@55316
   222
            else if (use_regex.selected)
lars@55316
   223
              Some(input.r)
lars@55316
   224
            else
lars@55316
   225
              Some(java.util.regex.Pattern.quote(input).r)
lars@55316
   226
          do_update(regex)
lars@55316
   227
          do_paint()
lars@55316
   228
      }
lars@55316
   229
    },
lars@55316
   230
    use_regex
lars@55316
   231
  )
lars@55316
   232
lars@55316
   233
  peer.add(controls.peer, BorderLayout.NORTH)
lars@55316
   234
}