isabelle: src/Tools/jEdit/src/jedit/raw_output_dockable.scala@dc7f5e0d9d27 (annotated)

34408 ad7b6c4813c8 added some headers and comments; wenzelm parents: 34406 diff changeset	1	/*
ad7b6c4813c8 added some headers and comments; wenzelm parents: 34406 diff changeset	2	* Dockable window for raw process output
ad7b6c4813c8 added some headers and comments; wenzelm parents: 34406 diff changeset	3	*
ad7b6c4813c8 added some headers and comments; wenzelm parents: 34406 diff changeset	4	* @author Fabian Immler, TU Munich
ad7b6c4813c8 added some headers and comments; wenzelm parents: 34406 diff changeset	5	* @author Johannes Hölzl, TU Munich
ad7b6c4813c8 added some headers and comments; wenzelm parents: 34406 diff changeset	6	*/
ad7b6c4813c8 added some headers and comments; wenzelm parents: 34406 diff changeset	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 d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34424 diff changeset	11	import java.awt.{Dimension, Graphics, GridLayout}
34424 c880492754d0 setPreferredSize for floating dockables; wenzelm parents: 34408 diff changeset	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 c880492754d0 setPreferredSize for floating dockables; wenzelm parents: 34408 diff changeset	15	import org.gjt.sp.jedit.gui.DockableWindowManager
c880492754d0 setPreferredSize for floating dockables; wenzelm parents: 34408 diff changeset	16
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	17
34760 dc7f5e0d9d27 misc modernization of names; wenzelm parents: 34759 diff changeset	18	class Raw_Output_Dockable(view: View, position: String) extends JPanel
dc7f5e0d9d27 misc modernization of names; wenzelm parents: 34759 diff changeset	19	{
34424 c880492754d0 setPreferredSize for floating dockables; wenzelm parents: 34408 diff changeset	20	if (position == DockableWindowManager.FLOATING)
c880492754d0 setPreferredSize for floating dockables; wenzelm parents: 34408 diff changeset	21	setPreferredSize(new Dimension(500, 250))
c880492754d0 setPreferredSize for floating dockables; wenzelm parents: 34408 diff changeset	22
34406 f81cd75ae331 restructured: independent provers in different buffers immler@in.tum.de parents: 34318 diff changeset	23	setLayout(new GridLayout(1, 1))
34424 c880492754d0 setPreferredSize for floating dockables; wenzelm parents: 34408 diff changeset	24	add(new JScrollPane(new JTextArea))
34671 d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34424 diff changeset	25
d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34424 diff changeset	26	def set_text(output_text_view: JTextArea) {
d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34424 diff changeset	27	removeAll()
d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34424 diff changeset	28	add(new JScrollPane(output_text_view))
d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34424 diff changeset	29	revalidate()
d179fcb04cbc output_info specific to prover immler@in.tum.de parents: 34424 diff changeset	30	}
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	31	}

author	wenzelm
	Tue, 08 Dec 2009 16:30:20 +0100
changeset 34760	dc7f5e0d9d27
parent 34759	bfea7839d9e1
child 34772	1a79c9b9af82
permissions	-rw-r--r--