author | Lars Hupel <lars.hupel@mytum.de> |
Mon, 19 May 2014 19:17:15 +0200 | |
changeset 57004 | c8288ce9676a |
parent 56782 | 433cf57550fa |
child 57031 | 30ee1453a954 |
permissions | -rw-r--r-- |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/simplifier_trace_window.scala |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
2 |
Author: Lars Hupel |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
3 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
4 |
Trace window with tree-style view of the simplifier trace. |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
5 |
*/ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
6 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
7 |
package isabelle.jedit |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
8 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
9 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
10 |
import isabelle._ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
11 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
12 |
import scala.annotation.tailrec |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
13 |
import scala.collection.immutable.SortedMap |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
14 |
import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
15 |
import scala.swing.event.{Key, KeyPressed} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
16 |
import scala.util.matching.Regex |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
17 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
18 |
import java.awt.BorderLayout |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
19 |
import java.awt.event.{ComponentEvent, ComponentAdapter} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
20 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
21 |
import javax.swing.SwingUtilities |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
22 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
23 |
import org.gjt.sp.jedit.View |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
24 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
25 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
26 |
private object Simplifier_Trace_Window |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
27 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
28 |
sealed trait Trace_Tree |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
29 |
{ |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
30 |
// FIXME replace with immutable tree builder |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
31 |
var children: SortedMap[Long, Either[Simplifier_Trace.Item.Data, Elem_Tree]] = SortedMap.empty |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
32 |
val serial: Long |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
33 |
val parent: Option[Trace_Tree] |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
34 |
val markup: String |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
35 |
def interesting: Boolean |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
36 |
|
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
37 |
def tree_children: List[Elem_Tree] = children.values.toList.collect { |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
38 |
case Right(tree) => tree |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
39 |
} |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
40 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
41 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
42 |
final class Root_Tree(val serial: Long) extends Trace_Tree |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
43 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
44 |
val parent = None |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
45 |
val interesting = true |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
46 |
val markup = "" |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
47 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
48 |
def format: XML.Body = |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
49 |
Pretty.separate(tree_children.flatMap(_.format)) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
50 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
51 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
52 |
final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree]) |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
53 |
extends Trace_Tree |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
54 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
55 |
val serial = data.serial |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
56 |
val markup = data.markup |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
57 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
58 |
lazy val interesting: Boolean = |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
59 |
data.markup == Markup.SIMP_TRACE_STEP || |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
60 |
data.markup == Markup.SIMP_TRACE_LOG || |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
61 |
tree_children.exists(_.interesting) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
62 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
63 |
private def body_contains(regex: Regex, body: XML.Body): Boolean = |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
64 |
body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
65 |
|
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
66 |
def format: Option[XML.Tree] = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
67 |
{ |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
68 |
def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree = |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
69 |
Pretty.block(Pretty.separate(XML.Text(data.text) :: data.content)) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
70 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
71 |
lazy val bodies: XML.Body = |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
72 |
children.values.toList.collect { |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
73 |
case Left(data) => Some(format_hint(data)) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
74 |
case Right(tree) if tree.interesting => tree.format |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
75 |
}.flatten.map(item => |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
76 |
XML.Elem(Markup(Markup.ITEM, Nil), List(item)) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
77 |
) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
78 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
79 |
val all = XML.Text(data.text) :: data.content ::: bodies |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
80 |
val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all)))) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
81 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
82 |
if (bodies != Nil) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
83 |
Some(res) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
84 |
else |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
85 |
None |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
86 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
87 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
88 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
89 |
@tailrec |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
90 |
def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit = |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
91 |
rest match { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
92 |
case Nil => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
93 |
() |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
94 |
case head :: tail => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
95 |
lookup.get(head.parent) match { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
96 |
case Some(parent) => |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
97 |
if (head.markup == Markup.SIMP_TRACE_HINT) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
98 |
{ |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
99 |
head.props match { |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
100 |
case Simplifier_Trace.Success(x) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
101 |
if x || |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
102 |
parent.markup == Markup.SIMP_TRACE_LOG || |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
103 |
parent.markup == Markup.SIMP_TRACE_STEP => |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
104 |
parent.children += ((head.serial, Left(head))) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
105 |
case _ => |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
106 |
// ignore |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
107 |
} |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
108 |
walk_trace(tail, lookup) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
109 |
} |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
110 |
else if (head.markup == Markup.SIMP_TRACE_IGNORE) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
111 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
112 |
parent.parent match { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
113 |
case None => |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56770
diff
changeset
|
114 |
Output.error_message("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
115 |
case Some(tree) => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
116 |
tree.children -= head.parent |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
117 |
walk_trace(tail, lookup) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
118 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
119 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
120 |
else |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
121 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
122 |
val entry = new Elem_Tree(head, Some(parent)) |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
123 |
parent.children += ((head.serial, Right(entry))) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
124 |
walk_trace(tail, lookup + (head.serial -> entry)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
125 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
126 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
127 |
case None => |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56770
diff
changeset
|
128 |
Output.error_message("Simplifier_Trace_Window: unknown parent " + head.parent) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
129 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
130 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
131 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
132 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
133 |
|
55556 | 134 |
|
135 |
class Simplifier_Trace_Window( |
|
136 |
view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
137 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
55825
diff
changeset
|
138 |
Swing_Thread.require {} |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
139 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
140 |
val pretty_text_area = new Pretty_Text_Area(view) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
141 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
142 |
size = new Dimension(500, 500) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
143 |
contents = new BorderPanel { |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
144 |
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
145 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
146 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
147 |
trace.entries.foreach(System.err.println) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
148 |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
149 |
private val tree = trace.entries.headOption match { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
150 |
case Some(first) => |
55556 | 151 |
val tree = new Simplifier_Trace_Window.Root_Tree(first.parent) |
152 |
Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree)) |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
153 |
tree |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
154 |
case None => |
55556 | 155 |
new Simplifier_Trace_Window.Root_Tree(0) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
156 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
157 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
158 |
do_update() |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
159 |
open() |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
160 |
do_paint() |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
161 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
162 |
def do_update() |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
163 |
{ |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
164 |
val xml = tree.format |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
165 |
pretty_text_area.update(snapshot, Command.Results.empty, xml) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
166 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
167 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
168 |
def do_paint() |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
169 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
170 |
Swing_Thread.later { |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
171 |
pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale"))) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
172 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
173 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
174 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
175 |
def handle_resize() |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
176 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
177 |
do_paint() |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
178 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
179 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
180 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
181 |
/* resize */ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
182 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
183 |
private val delay_resize = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
184 |
Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
185 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
186 |
peer.addComponentListener(new ComponentAdapter { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
187 |
override def componentResized(e: ComponentEvent) { delay_resize.invoke() } |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56750
diff
changeset
|
188 |
override def componentShown(e: ComponentEvent) { delay_resize.invoke() } |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
189 |
}) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
190 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
191 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
192 |
/* controls */ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
193 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
194 |
private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
195 |
pretty_text_area.search_label, |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
196 |
pretty_text_area.search_pattern) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
197 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
198 |
peer.add(controls.peer, BorderLayout.NORTH) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
199 |
} |