src/Tools/jEdit/src/simplifier_trace_window.scala
author wenzelm
Tue Feb 18 18:51:03 2014 +0100 (2014-02-18)
changeset 55556 60ba93d8f9e5
parent 55553 99409ccbe04a
child 55825 694833e3e4a0
permissions -rw-r--r--
tuned imports;
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
wenzelm@55556
   149
wenzelm@55556
   150
class Simplifier_Trace_Window(
wenzelm@55556
   151
  view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
lars@55316
   152
{
lars@55316
   153
  Swing_Thread.require()
lars@55316
   154
lars@55316
   155
  val area = new Pretty_Text_Area(view)
lars@55316
   156
lars@55316
   157
  size = new Dimension(500, 500)
lars@55316
   158
  contents = new BorderPanel {
lars@55316
   159
    layout(Component.wrap(area)) = BorderPanel.Position.Center
lars@55316
   160
  }
lars@55316
   161
lars@55316
   162
  private val tree = trace.entries.headOption match {
lars@55316
   163
    case Some(first) =>
wenzelm@55556
   164
      val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
wenzelm@55556
   165
      Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
lars@55316
   166
      tree
lars@55316
   167
    case None =>
wenzelm@55556
   168
      new Simplifier_Trace_Window.Root_Tree(0)
lars@55316
   169
  }
lars@55316
   170
lars@55316
   171
  do_update(None)
lars@55316
   172
  open()
lars@55316
   173
  do_paint()
lars@55316
   174
lars@55316
   175
  def do_update(regex: Option[Regex])
lars@55316
   176
  {
lars@55316
   177
    val xml = tree.format(regex)
lars@55316
   178
    area.update(snapshot, Command.Results.empty, xml)
lars@55316
   179
  }
lars@55316
   180
lars@55316
   181
  def do_paint()
lars@55316
   182
  {
lars@55316
   183
    Swing_Thread.later {
lars@55316
   184
      area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
lars@55316
   185
    }
lars@55316
   186
  }
lars@55316
   187
lars@55316
   188
  def handle_resize()
lars@55316
   189
  {
lars@55316
   190
    do_paint()
lars@55316
   191
  }
lars@55316
   192
lars@55316
   193
lars@55316
   194
  /* resize */
lars@55316
   195
lars@55316
   196
  private val delay_resize =
lars@55316
   197
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
lars@55316
   198
lars@55316
   199
  peer.addComponentListener(new ComponentAdapter {
lars@55316
   200
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
lars@55316
   201
    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
lars@55316
   202
  })
lars@55316
   203
lars@55316
   204
lars@55316
   205
  /* controls */
lars@55316
   206
lars@55316
   207
  val use_regex = new CheckBox("Regex")
lars@55316
   208
lars@55316
   209
  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
lars@55316
   210
    new Label {
lars@55316
   211
      text = "Search"
lars@55316
   212
    },
lars@55316
   213
    new TextField(30) {
lars@55316
   214
      listenTo(keys)
lars@55316
   215
      reactions += {
lars@55316
   216
        case KeyPressed(_, Key.Enter, 0, _) =>
lars@55316
   217
          val input = text.trim
lars@55316
   218
          val regex =
lars@55316
   219
            if (input.isEmpty)
lars@55316
   220
              None
lars@55316
   221
            else if (use_regex.selected)
lars@55316
   222
              Some(input.r)
lars@55316
   223
            else
lars@55316
   224
              Some(java.util.regex.Pattern.quote(input).r)
lars@55316
   225
          do_update(regex)
lars@55316
   226
          do_paint()
lars@55316
   227
      }
lars@55316
   228
    },
lars@55316
   229
    use_regex
lars@55316
   230
  )
lars@55316
   231
lars@55316
   232
  peer.add(controls.peer, BorderLayout.NORTH)
lars@55316
   233
}