author | wenzelm |
Tue, 27 Jun 2017 21:56:56 +0200 | |
changeset 66206 | 2d2082db735a |
parent 66205 | e9fa94f43a15 |
child 71704 | b9a5eb0f3b43 |
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 => |
57043 | 114 |
Output.error_message( |
115 |
"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
|
116 |
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
|
117 |
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
|
118 |
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
|
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 |
} |
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 |
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
|
122 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
123 |
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
|
124 |
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
|
125 |
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
|
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 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
128 |
case None => |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56770
diff
changeset
|
129 |
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
|
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 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
134 |
|
55556 | 135 |
|
136 |
class Simplifier_Trace_Window( |
|
137 |
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
|
138 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
139 |
GUI_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
|
140 |
|
57044 | 141 |
private val pretty_text_area = new Pretty_Text_Area(view) |
142 |
private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() } |
|
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
|
143 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
144 |
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
|
145 |
contents = new BorderPanel { |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
146 |
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
|
147 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
148 |
|
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 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
170 |
GUI_Thread.later { |
57043 | 171 |
pretty_text_area.resize( |
57044 | 172 |
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100)) |
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
|
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 |
|
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 |
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
|
177 |
{ |
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 |
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
|
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 |
|
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 |
/* 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
|
183 |
|
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 |
private val delay_resize = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
185 |
GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } |
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
|
186 |
|
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 |
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
|
188 |
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
|
189 |
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
|
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 |
|
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 |
/* 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
|
194 |
|
66205 | 195 |
private val controls = |
66206 | 196 |
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) |
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 |
} |