author | wenzelm |
Thu, 10 Dec 2009 22:15:19 +0100 | |
changeset 34777 | 91d6089cef88 |
parent 34775 | 49245d68f7e4 |
child 34784 | 02959dcea756 |
permissions | -rw-r--r-- |
34408 | 1 |
/* |
34765 | 2 |
* Dockable window with result message output |
34408 | 3 |
* |
34765 | 4 |
* @author Makarius |
34408 | 5 |
*/ |
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 |
|
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
10 |
import isabelle.proofdocument.{Command, HTML_Panel} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
11 |
|
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
12 |
import scala.actors.Actor._ |
34760 | 13 |
|
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
14 |
import javax.swing.JPanel |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
15 |
import java.awt.{BorderLayout, Dimension} |
34748 | 16 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.View |
34424 | 18 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
34745 | 19 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
20 |
|
34765 | 21 |
|
34773 | 22 |
class Output_Dockable(view: View, position: String) extends JPanel |
34760 | 23 |
{ |
34771 | 24 |
/* outer panel */ |
34760 | 25 |
|
34424 | 26 |
if (position == DockableWindowManager.FLOATING) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
27 |
setPreferredSize(new Dimension(500, 250)) |
34771 | 28 |
|
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
29 |
setLayout(new BorderLayout) |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34397
diff
changeset
|
30 |
|
34748 | 31 |
|
34771 | 32 |
/* HTML panel */ |
34745 | 33 |
|
34775 | 34 |
private val html_panel = |
35 |
new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null) |
|
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
36 |
add(html_panel, BorderLayout.CENTER) |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
37 |
|
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
38 |
|
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
39 |
/* actor wiring */ |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
40 |
|
34773 | 41 |
private val output_actor = actor { |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
42 |
loop { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
43 |
react { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
44 |
case cmd: Command => |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
45 |
Isabelle.plugin.theory_view(view.getBuffer) // FIXME total!?! |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
46 |
match { |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
47 |
case None => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
48 |
case Some(theory_view) => |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
49 |
val body = |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
50 |
if (cmd == null) Nil // FIXME ?? |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
51 |
else cmd.results(theory_view.current_document) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
52 |
html_panel.render(body) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
53 |
} |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
54 |
|
34773 | 55 |
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
|
56 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
57 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
58 |
} |
34428
d69fd18f37f9
basic setup of anti-aliasing, according to jEdit property;
wenzelm
parents:
34424
diff
changeset
|
59 |
|
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
60 |
private val properties_actor = actor { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
61 |
loop { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
62 |
react { |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
63 |
case _: Unit => html_panel.init(Isabelle.Int_Property("font-size")) |
34771 | 64 |
case bad => System.err.println("properties_actor: ignoring bad message " + bad) |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
65 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
66 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
67 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
68 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
69 |
override def addNotify() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
70 |
{ |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
71 |
super.addNotify() |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
72 |
Isabelle.session.results += output_actor |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
73 |
Isabelle.session.global_settings += properties_actor |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
74 |
} |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
75 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
76 |
override def removeNotify() |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
77 |
{ |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
78 |
Isabelle.session.results -= output_actor |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34775
diff
changeset
|
79 |
Isabelle.session.global_settings -= properties_actor |
34768
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
80 |
super.removeNotify() |
d8d321af1478
back to low-level JPanel, required for addNotify/removeNotify;
wenzelm
parents:
34765
diff
changeset
|
81 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
82 |
} |