src/Tools/jEdit/src/jedit/OutputDockable.scala
author wenzelm
Mon, 19 Jan 2009 20:33:26 +0100
changeset 34481 660c639870a4
parent 34424 c880492754d0
child 34671 d179fcb04cbc
permissions -rw-r--r--
replaced type parameter C by Command (thanks to globally simultaneous scope);

/*
 * Dockable window for raw process output
 *
 * @author Fabian Immler, TU Munich
 * @author Johannes Hölzl, TU Munich
 */

package isabelle.jedit


import java.awt.{Dimension, GridLayout}
import javax.swing.{JPanel, JTextArea, JScrollPane}

import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.gui.DockableWindowManager


class OutputDockable(view : View, position : String) extends JPanel {

  if (position == DockableWindowManager.FLOATING)
    setPreferredSize(new Dimension(500, 250))

  setLayout(new GridLayout(1, 1))
  add(new JScrollPane(new JTextArea))
}