author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 73340 | 0ffcad1f6130 |
child 75809 | 1dd5d4f4b69e |
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 |
|
75393 | 26 |
private object Simplifier_Trace_Window { |
27 |
sealed trait Trace_Tree { |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
28 |
// 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
|
29 |
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
|
30 |
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
|
31 |
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
|
32 |
val markup: String |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
33 |
def interesting: Boolean |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
34 |
|
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
35 |
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
|
36 |
case Right(tree) => tree |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
37 |
} |
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
|
38 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
39 |
|
75393 | 40 |
final class Root_Tree(val serial: Long) 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
|
41 |
val parent = None |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
42 |
val interesting = true |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
43 |
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
|
44 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
45 |
def format: XML.Body = |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
46 |
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
|
47 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
48 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
49 |
final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree]) |
75393 | 50 |
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
|
51 |
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
|
52 |
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
|
53 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
54 |
lazy val interesting: Boolean = |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
|
75393 | 62 |
def format: Option[XML.Tree] = { |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
63 |
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
|
64 |
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
|
65 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
66 |
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
|
67 |
children.values.toList.collect { |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
}.flatten.map(item => |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
71 |
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
|
72 |
) |
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
|
73 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
74 |
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
|
75 |
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
|
76 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
77 |
if (bodies != Nil) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
78 |
Some(res) |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
79 |
else |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
80 |
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
|
81 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
82 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
83 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
84 |
@tailrec |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55316
diff
changeset
|
85 |
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
|
86 |
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
|
87 |
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
|
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 |
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
|
90 |
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
|
91 |
case Some(parent) => |
75393 | 92 |
if (head.markup == Markup.SIMP_TRACE_HINT) { |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
93 |
head.props match { |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
94 |
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
|
95 |
if x || |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
96 |
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
|
97 |
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
|
98 |
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
|
99 |
case _ => |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
100 |
// ignore |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
101 |
} |
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
|
102 |
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
|
103 |
} |
75393 | 104 |
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
|
105 |
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
|
106 |
case None => |
57043 | 107 |
Output.error_message( |
108 |
"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
|
109 |
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
|
110 |
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
|
111 |
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
|
112 |
} |
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 |
} |
75393 | 114 |
else { |
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 |
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
|
116 |
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
|
117 |
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
|
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 |
case None => |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56770
diff
changeset
|
121 |
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
|
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 |
} |
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 |
|
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 |
|
55556 | 127 |
|
128 |
class Simplifier_Trace_Window( |
|
75393 | 129 |
view: View, |
130 |
snapshot: Document.Snapshot, |
|
131 |
trace: Simplifier_Trace.Trace |
|
132 |
) extends Frame { |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
133 |
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
|
134 |
|
57044 | 135 |
private val pretty_text_area = new Pretty_Text_Area(view) |
136 |
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
|
137 |
|
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 |
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
|
139 |
contents = new BorderPanel { |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
140 |
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
|
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 |
|
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 |
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
|
144 |
case Some(first) => |
55556 | 145 |
val tree = new Simplifier_Trace_Window.Root_Tree(first.parent) |
146 |
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
|
147 |
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
|
148 |
case None => |
55556 | 149 |
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
|
150 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
151 |
|
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
152 |
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
|
153 |
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
|
154 |
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
|
155 |
|
75393 | 156 |
def do_update(): Unit = { |
57004
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
157 |
val xml = tree.format |
c8288ce9676a
trace windows uses search feature of Pretty_Text_Area;
Lars Hupel <lars.hupel@mytum.de>
parents:
56782
diff
changeset
|
158 |
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
|
159 |
} |
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 |
|
75393 | 161 |
def do_paint(): Unit = { |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57044
diff
changeset
|
162 |
GUI_Thread.later { |
57043 | 163 |
pretty_text_area.resize( |
57044 | 164 |
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
|
165 |
} |
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 |
|
73340 | 168 |
def handle_resize(): Unit = 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
|
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 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
171 |
/* 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
|
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 |
private val delay_resize = |
71704 | 174 |
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { 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
|
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 |
peer.addComponentListener(new ComponentAdapter { |
73340 | 177 |
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() |
178 |
override def componentShown(e: ComponentEvent): Unit = 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
|
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 |
/* 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
|
183 |
|
66205 | 184 |
private val controls = |
66206 | 185 |
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
|
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.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
|
188 |
} |