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;
     1 /*
     2  * Dockable window for raw process output
     3  *
     4  * @author Fabian Immler, TU Munich
     5  * @author Johannes Hölzl, TU Munich
     6  */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import java.awt.{Dimension, Graphics, GridLayout}
    12 import javax.swing.{JPanel, JTextArea, JScrollPane}
    13 
    14 import org.gjt.sp.jedit.View
    15 import org.gjt.sp.jedit.gui.DockableWindowManager
    16 
    17 
    18 class Raw_Output_Dockable(view: View, position: String) extends JPanel
    19 {
    20   if (position == DockableWindowManager.FLOATING)
    21     setPreferredSize(new Dimension(500, 250))
    22 
    23   setLayout(new GridLayout(1, 1))
    24   add(new JScrollPane(new JTextArea))
    25 
    26   def set_text(output_text_view: JTextArea) {
    27     removeAll()
    28     add(new JScrollPane(output_text_view))
    29     revalidate()
    30   }
    31 }