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