src/Tools/jEdit/src/jedit/raw_output_dockable.scala
changeset 34759 bfea7839d9e1
parent 34671 d179fcb04cbc
child 34760 dc7f5e0d9d27
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Tue Dec 08 14:49:01 2009 +0100
     1.3 @@ -0,0 +1,31 @@
     1.4 +/*
     1.5 + * Dockable window for raw process output
     1.6 + *
     1.7 + * @author Fabian Immler, TU Munich
     1.8 + * @author Johannes Hölzl, TU Munich
     1.9 + */
    1.10 +
    1.11 +package isabelle.jedit
    1.12 +
    1.13 +
    1.14 +import java.awt.{Dimension, Graphics, GridLayout}
    1.15 +import javax.swing.{JPanel, JTextArea, JScrollPane}
    1.16 +
    1.17 +import org.gjt.sp.jedit.View
    1.18 +import org.gjt.sp.jedit.gui.DockableWindowManager
    1.19 +
    1.20 +
    1.21 +class OutputDockable(view : View, position : String) extends JPanel {
    1.22 +
    1.23 +  if (position == DockableWindowManager.FLOATING)
    1.24 +    setPreferredSize(new Dimension(500, 250))
    1.25 +
    1.26 +  setLayout(new GridLayout(1, 1))
    1.27 +  add(new JScrollPane(new JTextArea))
    1.28 +
    1.29 +  def set_text(output_text_view: JTextArea) {
    1.30 +    removeAll()
    1.31 +    add(new JScrollPane(output_text_view))
    1.32 +    revalidate()
    1.33 +  }
    1.34 +}