src/Tools/jEdit/src/simplifier_trace_window.scala
changeset 55316 885500f4aa6a
child 55553 99409ccbe04a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Feb 04 09:04:59 2014 +0000
     1.3 @@ -0,0 +1,237 @@
     1.4 +/*  Title:      Tools/jEdit/src/simplifier_trace_window.scala
     1.5 +    Author:     Lars Hupel
     1.6 +
     1.7 +Trace window with tree-style view of the simplifier trace.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +import scala.annotation.tailrec
    1.16 +
    1.17 +import scala.collection.immutable.SortedMap
    1.18 +
    1.19 +import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
    1.20 +import scala.swing.event.{Key, KeyPressed}
    1.21 +
    1.22 +import scala.util.matching.Regex
    1.23 +
    1.24 +import java.awt.BorderLayout
    1.25 +import java.awt.event.{ComponentEvent, ComponentAdapter}
    1.26 +
    1.27 +import javax.swing.SwingUtilities
    1.28 +
    1.29 +import org.gjt.sp.jedit.View
    1.30 +
    1.31 +private object Simplifier_Trace_Window
    1.32 +{
    1.33 +
    1.34 +  import Markup.Simp_Trace_Item
    1.35 +
    1.36 +  sealed trait Trace_Tree
    1.37 +  {
    1.38 +    var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
    1.39 +    val serial: Long
    1.40 +    val parent: Option[Trace_Tree]
    1.41 +    var hints: List[Simp_Trace_Item.Data]
    1.42 +    def set_interesting(): Unit
    1.43 +  }
    1.44 +
    1.45 +  final class Root_Tree(val serial: Long) extends Trace_Tree
    1.46 +  {
    1.47 +    val parent = None
    1.48 +    val hints = Nil
    1.49 +    def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
    1.50 +    def set_interesting() = ()
    1.51 +
    1.52 +    def format(regex: Option[Regex]): XML.Body =
    1.53 +      Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
    1.54 +  }
    1.55 +
    1.56 +  final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree
    1.57 +  {
    1.58 +    val serial = data.serial
    1.59 +    var hints = List.empty[Simp_Trace_Item.Data]
    1.60 +    var interesting: Boolean = false
    1.61 +
    1.62 +    def set_interesting(): Unit =
    1.63 +      if (!interesting)
    1.64 +      {
    1.65 +        interesting = true
    1.66 +        parent match {
    1.67 +          case Some(p) =>
    1.68 +            p.set_interesting()
    1.69 +          case None =>
    1.70 +        }
    1.71 +      }
    1.72 +
    1.73 +    def format(regex: Option[Regex]): (Boolean, XML.Tree) =
    1.74 +    {
    1.75 +      def format_child(child: Elem_Tree): Option[XML.Tree] = child.format(regex) match {
    1.76 +        case (false, _) =>
    1.77 +          None
    1.78 +        case (true, res) =>
    1.79 +          Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
    1.80 +      }
    1.81 +
    1.82 +      def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
    1.83 +        Pretty.block(Pretty.separate(
    1.84 +          XML.Text(data.text) ::
    1.85 +          data.content
    1.86 +        ))
    1.87 +
    1.88 +      def body_contains(regex: Regex, body: XML.Body): Boolean =
    1.89 +        body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
    1.90 +
    1.91 +      val children_bodies: XML.Body =
    1.92 +        children.values.filter(_.interesting).flatMap(format_child).toList
    1.93 +
    1.94 +      lazy val hint_bodies: XML.Body =
    1.95 +        hints.reverse.map(format_hint)
    1.96 +
    1.97 +      val eligible = regex match {
    1.98 +        case None =>
    1.99 +          true
   1.100 +        case Some(r) =>
   1.101 +          body_contains(r, data.content) || hints.exists(h => body_contains(r, h.content))
   1.102 +      }
   1.103 +
   1.104 +      val all =
   1.105 +        if (eligible)
   1.106 +          XML.Text(data.text) :: data.content ::: children_bodies ::: hint_bodies
   1.107 +        else
   1.108 +          XML.Text(data.text) :: children_bodies
   1.109 +
   1.110 +      val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
   1.111 +
   1.112 +      (eligible || children_bodies != Nil, res)
   1.113 +    }
   1.114 +  }
   1.115 +
   1.116 +  @tailrec
   1.117 +  def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
   1.118 +    rest match {
   1.119 +      case Nil =>
   1.120 +        ()
   1.121 +      case head :: tail =>
   1.122 +        lookup.get(head.parent) match {
   1.123 +          case Some(parent) =>
   1.124 +            if (head.markup == Simp_Trace_Item.HINT)
   1.125 +            {
   1.126 +              parent.hints ::= head
   1.127 +              walk_trace(tail, lookup)
   1.128 +            }
   1.129 +            else if (head.markup == Simp_Trace_Item.IGNORE)
   1.130 +            {
   1.131 +              parent.parent match {
   1.132 +                case None =>
   1.133 +                  System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
   1.134 +                case Some(tree) =>
   1.135 +                  tree.children -= head.parent
   1.136 +                  walk_trace(tail, lookup) // FIXME discard from lookup
   1.137 +              }
   1.138 +            }
   1.139 +            else
   1.140 +            {
   1.141 +              val entry = new Elem_Tree(head, Some(parent))
   1.142 +              parent.children += ((head.serial, entry))
   1.143 +              if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG)
   1.144 +                entry.set_interesting()
   1.145 +              walk_trace(tail, lookup + (head.serial -> entry))
   1.146 +            }
   1.147 +
   1.148 +          case None =>
   1.149 +            System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent)
   1.150 +        }
   1.151 +    }
   1.152 +
   1.153 +}
   1.154 +
   1.155 +class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
   1.156 +{
   1.157 +
   1.158 +  import Simplifier_Trace_Window._
   1.159 +
   1.160 +  Swing_Thread.require()
   1.161 +
   1.162 +  val area = new Pretty_Text_Area(view)
   1.163 +
   1.164 +  size = new Dimension(500, 500)
   1.165 +  contents = new BorderPanel {
   1.166 +    layout(Component.wrap(area)) = BorderPanel.Position.Center
   1.167 +  }
   1.168 +
   1.169 +  private val tree = trace.entries.headOption match {
   1.170 +    case Some(first) =>
   1.171 +      val tree = new Root_Tree(first.parent)
   1.172 +      walk_trace(trace.entries, Map(first.parent -> tree))
   1.173 +      tree
   1.174 +    case None =>
   1.175 +      new Root_Tree(0)
   1.176 +  }
   1.177 +
   1.178 +  do_update(None)
   1.179 +  open()
   1.180 +  do_paint()
   1.181 +
   1.182 +  def do_update(regex: Option[Regex])
   1.183 +  {
   1.184 +    val xml = tree.format(regex)
   1.185 +    area.update(snapshot, Command.Results.empty, xml)
   1.186 +  }
   1.187 +
   1.188 +  def do_paint()
   1.189 +  {
   1.190 +    Swing_Thread.later {
   1.191 +      area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
   1.192 +    }
   1.193 +  }
   1.194 +
   1.195 +  def handle_resize()
   1.196 +  {
   1.197 +    do_paint()
   1.198 +  }
   1.199 +
   1.200 +
   1.201 +  /* resize */
   1.202 +
   1.203 +  private val delay_resize =
   1.204 +    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   1.205 +
   1.206 +  peer.addComponentListener(new ComponentAdapter {
   1.207 +    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   1.208 +    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
   1.209 +  })
   1.210 +
   1.211 +
   1.212 +  /* controls */
   1.213 +
   1.214 +  val use_regex = new CheckBox("Regex")
   1.215 +
   1.216 +  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   1.217 +    new Label {
   1.218 +      text = "Search"
   1.219 +    },
   1.220 +    new TextField(30) {
   1.221 +      listenTo(keys)
   1.222 +      reactions += {
   1.223 +        case KeyPressed(_, Key.Enter, 0, _) =>
   1.224 +          val input = text.trim
   1.225 +          val regex =
   1.226 +            if (input.isEmpty)
   1.227 +              None
   1.228 +            else if (use_regex.selected)
   1.229 +              Some(input.r)
   1.230 +            else
   1.231 +              Some(java.util.regex.Pattern.quote(input).r)
   1.232 +          do_update(regex)
   1.233 +          do_paint()
   1.234 +      }
   1.235 +    },
   1.236 +    use_regex
   1.237 +  )
   1.238 +
   1.239 +  peer.add(controls.peer, BorderLayout.NORTH)
   1.240 +}