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