src/Tools/jEdit/src/simplifier_trace_window.scala
author wenzelm
Wed May 21 16:21:11 2014 +0200 (2014-05-21)
changeset 57044 042d6e58cb40
parent 57043 0f44d6dbd2a4
child 57612 990ffb84489b
permissions -rw-r--r--
more uniform Font_Info.Zoom_Box;
misc tuning and clarification;
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@57004
    30
    // FIXME replace with immutable tree builder
lars@57004
    31
    var children: SortedMap[Long, Either[Simplifier_Trace.Item.Data, Elem_Tree]] = SortedMap.empty
lars@55316
    32
    val serial: Long
lars@55316
    33
    val parent: Option[Trace_Tree]
lars@57004
    34
    val markup: String
lars@57004
    35
    def interesting: Boolean
lars@57004
    36
lars@57004
    37
    def tree_children: List[Elem_Tree] = children.values.toList.collect {
lars@57004
    38
      case Right(tree) => tree
lars@57004
    39
    }
lars@55316
    40
  }
lars@55316
    41
lars@55316
    42
  final class Root_Tree(val serial: Long) extends Trace_Tree
lars@55316
    43
  {
lars@55316
    44
    val parent = None
lars@57004
    45
    val interesting = true
lars@57004
    46
    val markup = ""
lars@55316
    47
lars@57004
    48
    def format: XML.Body =
lars@57004
    49
      Pretty.separate(tree_children.flatMap(_.format))
lars@55316
    50
  }
lars@55316
    51
wenzelm@55553
    52
  final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
wenzelm@55553
    53
    extends Trace_Tree
lars@55316
    54
  {
lars@55316
    55
    val serial = data.serial
lars@57004
    56
    val markup = data.markup
lars@55316
    57
lars@57004
    58
    lazy val interesting: Boolean =
lars@57004
    59
      data.markup == Markup.SIMP_TRACE_STEP ||
lars@57004
    60
      data.markup == Markup.SIMP_TRACE_LOG ||
lars@57004
    61
      tree_children.exists(_.interesting)
lars@55316
    62
lars@57004
    63
    private def body_contains(regex: Regex, body: XML.Body): Boolean =
lars@57004
    64
      body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
lars@57004
    65
lars@57004
    66
    def format: Option[XML.Tree] =
lars@55316
    67
    {
wenzelm@55553
    68
      def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
lars@57004
    69
        Pretty.block(Pretty.separate(XML.Text(data.text) :: data.content))
lars@55316
    70
lars@57004
    71
      lazy val bodies: XML.Body =
lars@57004
    72
        children.values.toList.collect {
lars@57004
    73
          case Left(data) => Some(format_hint(data))
lars@57004
    74
          case Right(tree) if tree.interesting => tree.format
lars@57004
    75
        }.flatten.map(item =>
lars@57004
    76
          XML.Elem(Markup(Markup.ITEM, Nil), List(item))
lars@57004
    77
        )
lars@55316
    78
lars@57004
    79
      val all = XML.Text(data.text) :: data.content ::: bodies
lars@55316
    80
      val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
lars@55316
    81
lars@57004
    82
      if (bodies != Nil)
lars@57004
    83
        Some(res)
lars@57004
    84
      else
lars@57004
    85
        None
lars@55316
    86
    }
lars@55316
    87
  }
lars@55316
    88
lars@55316
    89
  @tailrec
wenzelm@55553
    90
  def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
lars@55316
    91
    rest match {
lars@55316
    92
      case Nil =>
lars@55316
    93
        ()
lars@55316
    94
      case head :: tail =>
lars@55316
    95
        lookup.get(head.parent) match {
lars@55316
    96
          case Some(parent) =>
wenzelm@55553
    97
            if (head.markup == Markup.SIMP_TRACE_HINT)
lars@55316
    98
            {
lars@57004
    99
              head.props match {
lars@57004
   100
                case Simplifier_Trace.Success(x)
lars@57004
   101
                  if x ||
lars@57004
   102
                     parent.markup == Markup.SIMP_TRACE_LOG ||
lars@57004
   103
                     parent.markup == Markup.SIMP_TRACE_STEP =>
lars@57004
   104
                  parent.children += ((head.serial, Left(head)))
lars@57004
   105
                case _ =>
lars@57004
   106
                  // ignore
lars@57004
   107
              }
lars@55316
   108
              walk_trace(tail, lookup)
lars@55316
   109
            }
wenzelm@55553
   110
            else if (head.markup == Markup.SIMP_TRACE_IGNORE)
lars@55316
   111
            {
lars@55316
   112
              parent.parent match {
lars@55316
   113
                case None =>
wenzelm@57043
   114
                  Output.error_message(
wenzelm@57043
   115
                    "Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
lars@55316
   116
                case Some(tree) =>
lars@55316
   117
                  tree.children -= head.parent
lars@57004
   118
                  walk_trace(tail, lookup)
lars@55316
   119
              }
lars@55316
   120
            }
lars@55316
   121
            else
lars@55316
   122
            {
lars@55316
   123
              val entry = new Elem_Tree(head, Some(parent))
lars@57004
   124
              parent.children += ((head.serial, Right(entry)))
lars@55316
   125
              walk_trace(tail, lookup + (head.serial -> entry))
lars@55316
   126
            }
lars@55316
   127
lars@55316
   128
          case None =>
wenzelm@56782
   129
            Output.error_message("Simplifier_Trace_Window: unknown parent " + head.parent)
lars@55316
   130
        }
lars@55316
   131
    }
lars@55316
   132
lars@55316
   133
}
lars@55316
   134
wenzelm@55556
   135
wenzelm@55556
   136
class Simplifier_Trace_Window(
wenzelm@55556
   137
  view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
lars@55316
   138
{
wenzelm@56662
   139
  Swing_Thread.require {}
lars@55316
   140
wenzelm@57044
   141
  private val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@57044
   142
  private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
lars@55316
   143
lars@55316
   144
  size = new Dimension(500, 500)
lars@55316
   145
  contents = new BorderPanel {
lars@57004
   146
    layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
lars@55316
   147
  }
lars@55316
   148
lars@55316
   149
  private val tree = trace.entries.headOption match {
lars@55316
   150
    case Some(first) =>
wenzelm@55556
   151
      val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
wenzelm@55556
   152
      Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
lars@55316
   153
      tree
lars@55316
   154
    case None =>
wenzelm@55556
   155
      new Simplifier_Trace_Window.Root_Tree(0)
lars@55316
   156
  }
lars@55316
   157
lars@57004
   158
  do_update()
lars@55316
   159
  open()
lars@55316
   160
  do_paint()
lars@55316
   161
lars@57004
   162
  def do_update()
lars@55316
   163
  {
lars@57004
   164
    val xml = tree.format
lars@57004
   165
    pretty_text_area.update(snapshot, Command.Results.empty, xml)
lars@55316
   166
  }
lars@55316
   167
lars@55316
   168
  def do_paint()
lars@55316
   169
  {
lars@55316
   170
    Swing_Thread.later {
wenzelm@57043
   171
      pretty_text_area.resize(
wenzelm@57044
   172
        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
lars@55316
   173
    }
lars@55316
   174
  }
lars@55316
   175
lars@55316
   176
  def handle_resize()
lars@55316
   177
  {
lars@55316
   178
    do_paint()
lars@55316
   179
  }
lars@55316
   180
lars@55316
   181
lars@55316
   182
  /* resize */
lars@55316
   183
lars@55316
   184
  private val delay_resize =
lars@55316
   185
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
lars@55316
   186
lars@55316
   187
  peer.addComponentListener(new ComponentAdapter {
lars@55316
   188
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@56770
   189
    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
lars@55316
   190
  })
lars@55316
   191
lars@55316
   192
lars@55316
   193
  /* controls */
lars@55316
   194
lars@55316
   195
  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
lars@57004
   196
    pretty_text_area.search_label,
wenzelm@57043
   197
    pretty_text_area.search_field,
wenzelm@57043
   198
    zoom)
lars@55316
   199
lars@55316
   200
  peer.add(controls.peer, BorderLayout.NORTH)
lars@55316
   201
}