author | wenzelm |
Fri, 02 May 2014 20:07:55 +0200 | |
changeset 56832 | 93f05fa757dd |
parent 56770 | e160ae47db94 |
child 57593 | 2f7d91242b99 |
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_dockable.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 |
Dockable window with interactive 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.swing.{Button, CheckBox, Orientation, Separator} |
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.swing.event.ButtonClicked |
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 |
|
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 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
|
16 |
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
|
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 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
|
19 |
|
55556 | 20 |
|
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
|
21 |
class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) |
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 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56299
diff
changeset
|
23 |
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
|
24 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
25 |
/* component state -- owned by Swing thread */ |
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 |
|
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 |
private var current_snapshot = Document.State.init.snapshot() |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
28 |
private var current_command = Command.empty |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
29 |
private var current_results = Command.Results.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 |
private var current_id = 0L |
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 |
private var do_update = true |
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 |
private var do_auto_reply = false |
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 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
34 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
35 |
private val text_area = new Pretty_Text_Area(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
|
36 |
set_content(text_area) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
37 |
|
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 |
private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.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
|
39 |
{ |
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 |
val data = question.data |
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 |
def make_button(answer: Simplifier_Trace.Answer): XML.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 |
XML.Wrapped_Elem( |
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 |
Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
45 |
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
|
46 |
List(XML.Text(answer.string)) |
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 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
49 |
def make_block(body: XML.Body): XML.Body = |
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 |
List(Pretty.Block(0, body)) |
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 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
52 |
val all = Pretty.separate( |
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 |
XML.Text(data.text) :: |
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 |
data.content ::: |
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 |
make_block(Library.separate(XML.Text(", "), question.answers map make_button)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
56 |
) |
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 |
|
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 |
XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(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
|
59 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
60 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
61 |
private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context) |
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 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56299
diff
changeset
|
63 |
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
|
64 |
val questions = context.questions.values |
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 |
if (do_auto_reply && !questions.isEmpty) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
66 |
{ |
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 |
questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer)) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
68 |
handle_update(do_update) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
69 |
} |
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 |
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
|
71 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
72 |
val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut)) |
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 |
text_area.update(snapshot, Command.Results.empty, contents) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
74 |
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
|
75 |
} |
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 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
77 |
|
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 |
private def show_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
|
79 |
{ |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
80 |
val trace = Simplifier_Trace.generate_trace(current_results) |
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 |
new Simplifier_Trace_Window(view, current_snapshot, 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
|
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 |
private 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
|
85 |
{ |
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 |
Swing_Thread.later { |
55825 | 87 |
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
|
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 |
} |
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 |
|
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 |
private def update_contents() |
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 |
{ |
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 |
set_context( |
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 |
current_snapshot, |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
95 |
Simplifier_Trace.handle_results(PIDE.session, current_id, current_results) |
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
|
96 |
) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
97 |
} |
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 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
99 |
private 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
|
100 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
101 |
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
|
102 |
} |
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 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
104 |
private def handle_update(follow: Boolean) |
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 |
{ |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
106 |
val (new_snapshot, new_command, new_results, new_id) = |
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
|
107 |
PIDE.editor.current_node_snapshot(view) 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
|
108 |
case Some(snapshot) => |
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 |
if (follow && !snapshot.is_outdated) { |
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 |
PIDE.editor.current_command(view, snapshot) 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
|
111 |
case Some(cmd) => |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
112 |
(snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id) |
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
|
113 |
case None => |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
114 |
(Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L) |
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 |
} |
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 |
} |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
117 |
else (current_snapshot, current_command, current_results, current_id) |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
118 |
case None => (current_snapshot, current_command, current_results, current_id) |
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 |
current_snapshot = new_snapshot |
56299
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
122 |
current_command = new_command |
8201790fdeb9
more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents:
55825
diff
changeset
|
123 |
current_results = new_results |
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 |
current_id = new_id |
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 |
update_contents() |
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 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
129 |
/* main */ |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
130 |
|
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
131 |
private val main = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
132 |
Session.Consumer[Any](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
133 |
case _: Session.Global_Options => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
134 |
Swing_Thread.later { 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
|
135 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
136 |
case changed: Session.Commands_Changed => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
137 |
Swing_Thread.later { handle_update(do_update) } |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
138 |
|
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
139 |
case Session.Caret_Focus => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
140 |
Swing_Thread.later { handle_update(do_update) } |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
141 |
|
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
142 |
case Simplifier_Trace.Event => |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
143 |
Swing_Thread.later { handle_update(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
|
144 |
} |
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 |
override def init() |
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 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56299
diff
changeset
|
148 |
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
|
149 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
150 |
PIDE.session.global_options += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
151 |
PIDE.session.commands_changed += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
152 |
PIDE.session.caret_focus += main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
153 |
PIDE.session.trace_events += main |
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
|
154 |
handle_update(true) |
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 |
} |
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 |
override def exit() |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
158 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56299
diff
changeset
|
159 |
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
|
160 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
161 |
PIDE.session.global_options -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
162 |
PIDE.session.commands_changed -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
163 |
PIDE.session.caret_focus -= main |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
164 |
PIDE.session.trace_events -= main |
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 |
delay_resize.revoke() |
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 |
|
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 |
/* 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
|
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 |
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
|
172 |
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
|
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 |
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
|
175 |
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:
56715
diff
changeset
|
176 |
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
|
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 |
|
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 |
/* 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
|
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 |
private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( |
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 |
new CheckBox("Auto update") { |
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 |
selected = do_update |
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 |
reactions += { |
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 |
case ButtonClicked(_) => |
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 |
do_update = this.selected |
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 |
handle_update(do_update) |
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 |
new Button("Update") { |
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 |
reactions += { |
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 |
case ButtonClicked(_) => |
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 |
handle_update(true) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
195 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
196 |
}, |
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 |
new Separator(Orientation.Vertical), |
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 |
new CheckBox("Auto reply") { |
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 |
selected = do_auto_reply |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
200 |
reactions += { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
201 |
case ButtonClicked(_) => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
202 |
do_auto_reply = this.selected |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
203 |
handle_update(do_update) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
204 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
205 |
}, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
206 |
new Separator(Orientation.Vertical), |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
207 |
new Button("Show 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
|
208 |
reactions += { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
209 |
case ButtonClicked(_) => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
210 |
show_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
|
211 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
212 |
}, |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
213 |
new Button("Clear memory") { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
214 |
reactions += { |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
215 |
case ButtonClicked(_) => |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
216 |
Simplifier_Trace.clear_memory() |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
217 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
218 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
219 |
) |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
220 |
|
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
221 |
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
|
222 |
} |