1/*  Title:      Tools/jEdit/src/simplifier_trace_window.scala
2    Author:     Lars Hupel
3
4Trace window with tree-style view of the simplifier trace.
5*/
6
7package isabelle.jedit
8
9
10import isabelle._
11
12import scala.annotation.tailrec
13import scala.collection.immutable.SortedMap
14import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
15import scala.swing.event.{Key, KeyPressed}
16import scala.util.matching.Regex
17
18import java.awt.BorderLayout
19import java.awt.event.{ComponentEvent, ComponentAdapter}
20
21import javax.swing.SwingUtilities
22
23import org.gjt.sp.jedit.View
24
25
26private 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
136class 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 =
196    Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
197
198  peer.add(controls.peer, BorderLayout.NORTH)
199}
200