author | wenzelm |
Wed, 19 May 2010 21:18:02 +0200 | |
changeset 36988 | fd641bc85222 |
parent 36817 | ed97e877ff2d |
child 36989 | aaa7cac3e54a |
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} |
34748 | 19 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
20 |
import org.gjt.sp.jedit.View |
34424 | 21 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
34745 | 22 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
|
34765 | 24 |
|
34791 | 25 |
class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout) |
34760 | 26 |
{ |
34424 | 27 |
if (position == DockableWindowManager.FLOATING) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
28 |
setPreferredSize(new Dimension(500, 250)) |
34771 | 29 |
|
36988 | 30 |
val controls = new FlowPanel(FlowPanel.Alignment.Right)() |
31 |
add(controls.peer, BorderLayout.NORTH) |
|
32 |
||
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
33 |
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
|
34 |
add(html_panel, BorderLayout.CENTER) |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
35 |
|
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
36 |
|
36988 | 37 |
/* controls */ |
38 |
||
39 |
private def handle_update() |
|
40 |
{ |
|
41 |
Swing_Thread.now { |
|
42 |
Document_Model(view.getBuffer) match { |
|
43 |
case Some(model) => |
|
44 |
model.recent_document.command_at(view.getTextArea.getCaretPosition) match { |
|
45 |
case Some((cmd, _)) => output_actor ! cmd |
|
46 |
case None => |
|
47 |
} |
|
48 |
case None => |
|
49 |
} |
|
50 |
} |
|
51 |
} |
|
52 |
||
53 |
private val update = new Button("Update") { |
|
54 |
reactions += { case ButtonClicked(_) => handle_update() } |
|
55 |
} |
|
56 |
||
57 |
private val freeze = new ToggleButton("Freeze") |
|
58 |
||
59 |
||
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
60 |
/* actor wiring */ |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
61 |
|
34773 | 62 |
private val output_actor = actor { |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
63 |
loop { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
64 |
react { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
65 |
case cmd: Command => |
36988 | 66 |
Swing_Thread.now { |
67 |
if (freeze.selected) None else Document_Model(view.getBuffer) |
|
68 |
} match { |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
69 |
case None => |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
70 |
case Some(model) => |
34867 | 71 |
val body = model.recent_document.current_state(cmd).map(_.results) getOrElse Nil |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
72 |
html_panel.render(body) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
73 |
} |
34791 | 74 |
|
36817
ed97e877ff2d
more precise pretty printing based on actual font metrics;
wenzelm
parents:
36814
diff
changeset
|
75 |
case Session.Global_Settings => html_panel.init(Isabelle.font_size()) |
36988 | 76 |
|
34773 | 77 |
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
|
78 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
79 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
80 |
} |
34428
d69fd18f37f9
basic setup of anti-aliasing, according to jEdit property;
wenzelm
parents:
34424
diff
changeset
|
81 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
82 |
override def addNotify() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
83 |
{ |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
84 |
super.addNotify() |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
85 |
Isabelle.session.results += output_actor |
34791 | 86 |
Isabelle.session.global_settings += output_actor |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
87 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
88 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
89 |
override def removeNotify() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
90 |
{ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
91 |
Isabelle.session.results -= output_actor |
34791 | 92 |
Isabelle.session.global_settings -= output_actor |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
93 |
super.removeNotify() |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
94 |
} |
36988 | 95 |
|
96 |
||
97 |
/* init controls */ |
|
98 |
||
99 |
controls.contents ++= List(update, freeze) |
|
100 |
handle_update() |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
101 |
} |