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