author | wenzelm |
Tue, 08 Dec 2009 12:10:55 +0100 | |
changeset 34757 | adf4e0f27d54 |
parent 34671 | d179fcb04cbc |
permissions | -rw-r--r-- |
34408 | 1 |
/* |
2 |
* Dockable window for raw process output |
|
3 |
* |
|
4 |
* @author Fabian Immler, TU Munich |
|
5 |
* @author Johannes Hölzl, TU Munich |
|
6 |
*/ |
|
7 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
34671 | 11 |
import java.awt.{Dimension, Graphics, GridLayout} |
34424 | 12 |
import javax.swing.{JPanel, JTextArea, JScrollPane} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
13 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
14 |
import org.gjt.sp.jedit.View |
34424 | 15 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
16 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
18 |
class OutputDockable(view : View, position : String) extends JPanel { |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34318
diff
changeset
|
19 |
|
34424 | 20 |
if (position == DockableWindowManager.FLOATING) |
21 |
setPreferredSize(new Dimension(500, 250)) |
|
22 |
||
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34318
diff
changeset
|
23 |
setLayout(new GridLayout(1, 1)) |
34424 | 24 |
add(new JScrollPane(new JTextArea)) |
34671 | 25 |
|
26 |
def set_text(output_text_view: JTextArea) { |
|
27 |
removeAll() |
|
28 |
add(new JScrollPane(output_text_view)) |
|
29 |
revalidate() |
|
30 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
31 |
} |