src/Tools/jEdit/src/simplifier_trace_window.scala

interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state

/*  Title:      Tools/jEdit/src/simplifier_trace_window.scala
    Author:     Lars Hupel

Trace window with tree-style view of the simplifier trace.
*/

package isabelle.jedit


import isabelle._

import scala.annotation.tailrec

import scala.collection.immutable.SortedMap

import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
import scala.swing.event.{Key, KeyPressed}

import scala.util.matching.Regex

import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}

import javax.swing.SwingUtilities

import org.gjt.sp.jedit.View

private object Simplifier_Trace_Window
{

  import Markup.Simp_Trace_Item

  sealed trait Trace_Tree
  {
    var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
    val serial: Long
    val parent: Option[Trace_Tree]
    var hints: List[Simp_Trace_Item.Data]
    def set_interesting(): Unit
  }

  final class Root_Tree(val serial: Long) extends Trace_Tree
  {
    val parent = None
    val hints = Nil
    def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
    def set_interesting() = ()

    def format(regex: Option[Regex]): XML.Body =
      Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
  }

  final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree
  {
    val serial = data.serial
    var hints = List.empty[Simp_Trace_Item.Data]
    var interesting: Boolean = false

    def set_interesting(): Unit =
      if (!interesting)
      {
        interesting = true
        parent match {
          case Some(p) =>
            p.set_interesting()
          case None =>
        }
      }

    def format(regex: Option[Regex]): (Boolean, XML.Tree) =
    {
      def format_child(child: Elem_Tree): Option[XML.Tree] = child.format(regex) match {
        case (false, _) =>
          None
        case (true, res) =>
          Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
      }

      def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
        Pretty.block(Pretty.separate(
          XML.Text(data.text) ::
          data.content
        ))

      def body_contains(regex: Regex, body: XML.Body): Boolean =
        body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)

      val children_bodies: XML.Body =
        children.values.filter(_.interesting).flatMap(format_child).toList

      lazy val hint_bodies: XML.Body =
        hints.reverse.map(format_hint)

      val eligible = regex match {
        case None =>
          true
        case Some(r) =>
          body_contains(r, data.content) || hints.exists(h => body_contains(r, h.content))
      }

      val all =
        if (eligible)
          XML.Text(data.text) :: data.content ::: children_bodies ::: hint_bodies
        else
          XML.Text(data.text) :: children_bodies

      val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))

      (eligible || children_bodies != Nil, res)
    }
  }

  @tailrec
  def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
    rest match {
      case Nil =>
        ()
      case head :: tail =>
        lookup.get(head.parent) match {
          case Some(parent) =>
            if (head.markup == Simp_Trace_Item.HINT)
            {
              parent.hints ::= head
              walk_trace(tail, lookup)
            }
            else if (head.markup == Simp_Trace_Item.IGNORE)
            {
              parent.parent match {
                case None =>
                  System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
                case Some(tree) =>
                  tree.children -= head.parent
                  walk_trace(tail, lookup) // FIXME discard from lookup
              }
            }
            else
            {
              val entry = new Elem_Tree(head, Some(parent))
              parent.children += ((head.serial, entry))
              if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG)
                entry.set_interesting()
              walk_trace(tail, lookup + (head.serial -> entry))
            }

          case None =>
            System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent)
        }
    }

}

class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
{

  import Simplifier_Trace_Window._

  Swing_Thread.require()

  val area = new Pretty_Text_Area(view)

  size = new Dimension(500, 500)
  contents = new BorderPanel {
    layout(Component.wrap(area)) = BorderPanel.Position.Center
  }

  private val tree = trace.entries.headOption match {
    case Some(first) =>
      val tree = new Root_Tree(first.parent)
      walk_trace(trace.entries, Map(first.parent -> tree))
      tree
    case None =>
      new Root_Tree(0)
  }

  do_update(None)
  open()
  do_paint()

  def do_update(regex: Option[Regex])
  {
    val xml = tree.format(regex)
    area.update(snapshot, Command.Results.empty, xml)
  }

  def do_paint()
  {
    Swing_Thread.later {
      area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
    }
  }

  def handle_resize()
  {
    do_paint()
  }


  /* resize */

  private val delay_resize =
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }

  peer.addComponentListener(new ComponentAdapter {
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
  })


  /* controls */

  val use_regex = new CheckBox("Regex")

  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    new Label {
      text = "Search"
    },
    new TextField(30) {
      listenTo(keys)
      reactions += {
        case KeyPressed(_, Key.Enter, 0, _) =>
          val input = text.trim
          val regex =
            if (input.isEmpty)
              None
            else if (use_regex.selected)
              Some(input.r)
            else
              Some(java.util.regex.Pattern.quote(input).r)
          do_update(regex)
          do_paint()
      }
    },
    use_regex
  )

  peer.add(controls.peer, BorderLayout.NORTH)
}