src/Tools/jEdit/src/jedit/raw_output_dockable.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34772 1a79c9b9af82
permissions -rw-r--r--
misc modernization of names;
wenzelm@34408
     1
/*
wenzelm@34408
     2
 * Dockable window for raw process output
wenzelm@34408
     3
 *
wenzelm@34408
     4
 * @author Fabian Immler, TU Munich
wenzelm@34408
     5
 * @author Johannes Hölzl, TU Munich
wenzelm@34408
     6
 */
wenzelm@34408
     7
wenzelm@34318
     8
package isabelle.jedit
wenzelm@34318
     9
wenzelm@34318
    10
immler@34671
    11
import java.awt.{Dimension, Graphics, GridLayout}
wenzelm@34424
    12
import javax.swing.{JPanel, JTextArea, JScrollPane}
wenzelm@34318
    13
wenzelm@34318
    14
import org.gjt.sp.jedit.View
wenzelm@34424
    15
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@34424
    16
wenzelm@34318
    17
wenzelm@34760
    18
class Raw_Output_Dockable(view: View, position: String) extends JPanel
wenzelm@34760
    19
{
wenzelm@34424
    20
  if (position == DockableWindowManager.FLOATING)
wenzelm@34424
    21
    setPreferredSize(new Dimension(500, 250))
wenzelm@34424
    22
immler@34406
    23
  setLayout(new GridLayout(1, 1))
wenzelm@34424
    24
  add(new JScrollPane(new JTextArea))
immler@34671
    25
immler@34671
    26
  def set_text(output_text_view: JTextArea) {
immler@34671
    27
    removeAll()
immler@34671
    28
    add(new JScrollPane(output_text_view))
immler@34671
    29
    revalidate()
immler@34671
    30
  }
wenzelm@34318
    31
}