src/Tools/jEdit/src/simplifier_trace_window.scala
author wenzelm
Tue Apr 29 13:32:13 2014 +0200 (2014-04-29)
changeset 56782 433cf57550fa
parent 56770 e160ae47db94
child 57004 c8288ce9676a
permissions -rw-r--r--
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
     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                   Output.error_message("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             Output.error_message("Simplifier_Trace_Window: unknown parent " + head.parent)
   144         }
   145     }
   146 
   147 }
   148 
   149 
   150 class Simplifier_Trace_Window(
   151   view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
   152 {
   153   Swing_Thread.require {}
   154 
   155   val area = new Pretty_Text_Area(view)
   156 
   157   size = new Dimension(500, 500)
   158   contents = new BorderPanel {
   159     layout(Component.wrap(area)) = BorderPanel.Position.Center
   160   }
   161 
   162   private val tree = trace.entries.headOption match {
   163     case Some(first) =>
   164       val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
   165       Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
   166       tree
   167     case None =>
   168       new Simplifier_Trace_Window.Root_Tree(0)
   169   }
   170 
   171   do_update(None)
   172   open()
   173   do_paint()
   174 
   175   def do_update(regex: Option[Regex])
   176   {
   177     val xml = tree.format(regex)
   178     area.update(snapshot, Command.Results.empty, xml)
   179   }
   180 
   181   def do_paint()
   182   {
   183     Swing_Thread.later {
   184       area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
   185     }
   186   }
   187 
   188   def handle_resize()
   189   {
   190     do_paint()
   191   }
   192 
   193 
   194   /* resize */
   195 
   196   private val delay_resize =
   197     Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   198 
   199   peer.addComponentListener(new ComponentAdapter {
   200     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   201     override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   202   })
   203 
   204 
   205   /* controls */
   206 
   207   val use_regex = new CheckBox("Regex")
   208 
   209   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   210     new Label("Search"),
   211     new TextField(30) {
   212       listenTo(keys)
   213       reactions += {
   214         case KeyPressed(_, Key.Enter, 0, _) =>
   215           val input = text.trim
   216           val regex =
   217             if (input.isEmpty)
   218               None
   219             else if (use_regex.selected)
   220               Some(input.r)
   221             else
   222               Some(java.util.regex.Pattern.quote(input).r)
   223           do_update(regex)
   224           do_paint()
   225       }
   226     },
   227     use_regex
   228   )
   229 
   230   peer.add(controls.peer, BorderLayout.NORTH)
   231 }