author | wenzelm |
Thu, 20 May 2010 20:56:26 +0200 | |
changeset 37014 | 1af0f718ffdc |
parent 36993 | b7cce32953f0 |
child 37017 | cf6625012282 |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/output_dockable.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Dockable window with result message output. |
|
5 |
*/ |
|
34408 | 6 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
|
34760 | 9 |
|
36015 | 10 |
import isabelle._ |
11 |
||
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
12 |
import scala.actors.Actor._ |
34760 | 13 |
|
36988 | 14 |
import scala.swing.{FlowPanel, Button, ToggleButton} |
15 |
import scala.swing.event.ButtonClicked |
|
16 |
||
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
17 |
import javax.swing.JPanel |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
18 |
import java.awt.{BorderLayout, Dimension} |
37014 | 19 |
import java.awt.event.{ComponentEvent, ComponentAdapter} |
34748 | 20 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
21 |
import org.gjt.sp.jedit.View |
34424 | 22 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
34745 | 23 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
24 |
|
34765 | 25 |
|
34791 | 26 |
class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout) |
34760 | 27 |
{ |
34424 | 28 |
if (position == DockableWindowManager.FLOATING) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
29 |
setPreferredSize(new Dimension(500, 250)) |
34771 | 30 |
|
36988 | 31 |
val controls = new FlowPanel(FlowPanel.Alignment.Right)() |
32 |
add(controls.peer, BorderLayout.NORTH) |
|
33 |
||
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
34 |
val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
35 |
add(html_panel, BorderLayout.CENTER) |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
36 |
|
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
37 |
|
36988 | 38 |
/* controls */ |
39 |
||
36989
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
40 |
private case class Render(body: List[XML.Tree]) |
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
41 |
|
36988 | 42 |
private def handle_update() |
43 |
{ |
|
44 |
Swing_Thread.now { |
|
45 |
Document_Model(view.getBuffer) match { |
|
46 |
case Some(model) => |
|
36989
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
47 |
val document = model.recent_document |
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
48 |
document.command_at(view.getTextArea.getCaretPosition) match { |
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
49 |
case Some((cmd, _)) => |
36990
449628c148cf
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
wenzelm
parents:
36989
diff
changeset
|
50 |
output_actor ! Render(document.current_state(cmd).results) |
36988 | 51 |
case None => |
52 |
} |
|
53 |
case None => |
|
54 |
} |
|
55 |
} |
|
56 |
} |
|
57 |
||
58 |
private val update = new Button("Update") { |
|
59 |
reactions += { case ButtonClicked(_) => handle_update() } |
|
60 |
} |
|
61 |
||
36989
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
62 |
val follow = new ToggleButton("Follow") |
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
63 |
follow.selected = true |
36988 | 64 |
|
65 |
||
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
66 |
/* actor wiring */ |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
67 |
|
34773 | 68 |
private val output_actor = actor { |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
69 |
loop { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
70 |
react { |
36993
b7cce32953f0
more systematic treatment of physical document wrt. font size etc.;
wenzelm
parents:
36990
diff
changeset
|
71 |
case Session.Global_Settings => html_panel.resize(Isabelle.font_size()) |
36989
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
72 |
case Render(body) => html_panel.render(body) |
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
73 |
|
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
74 |
case cmd: Command => |
36988 | 75 |
Swing_Thread.now { |
36989
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
76 |
if (follow.selected) Document_Model(view.getBuffer) else None |
36988 | 77 |
} match { |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
78 |
case None => |
36990
449628c148cf
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
wenzelm
parents:
36989
diff
changeset
|
79 |
case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
80 |
} |
34791 | 81 |
|
34773 | 82 |
case bad => System.err.println("output_actor: ignoring bad message " + bad) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
83 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
84 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
85 |
} |
34428
d69fd18f37f9
basic setup of anti-aliasing, according to jEdit property;
wenzelm
parents:
34424
diff
changeset
|
86 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
87 |
override def addNotify() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
88 |
{ |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
89 |
super.addNotify() |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
90 |
Isabelle.session.results += output_actor |
34791 | 91 |
Isabelle.session.global_settings += output_actor |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
92 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
93 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
94 |
override def removeNotify() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
95 |
{ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
96 |
Isabelle.session.results -= output_actor |
34791 | 97 |
Isabelle.session.global_settings -= output_actor |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
98 |
super.removeNotify() |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
99 |
} |
36988 | 100 |
|
101 |
||
37014 | 102 |
/* resize */ |
103 |
||
104 |
addComponentListener(new ComponentAdapter { |
|
105 |
val delay = Swing_Thread.delay_last(500) { html_panel.refresh() } |
|
106 |
override def componentResized(e: ComponentEvent) { delay() } |
|
107 |
}) |
|
108 |
||
109 |
||
36988 | 110 |
/* init controls */ |
111 |
||
36989
aaa7cac3e54a
inverted "Freeze" to "Follow", which is the default;
wenzelm
parents:
36988
diff
changeset
|
112 |
controls.contents ++= List(update, follow) |
36988 | 113 |
handle_update() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
114 |
} |