view src/samer/core_/util/swing/Console.java @ 8:5e3cbbf173aa tip

Reorganise some more
author samer
date Fri, 05 Apr 2019 22:41:58 +0100
parents bf79fb79ee13
children
line wrap: on
line source
/*
 *	Console.java	
 *
 *	Copyright (c) 2000, Samer Abdallah, King's College London.
 *	All rights reserved.
 *
 *	This software is provided AS iS and WITHOUT ANY WARRANTY; 
 *	without even the implied warranty of MERCHANTABILITY or 
 *	FITNESS FOR A PARTICULAR PURPOSE.
 */

package samer.core.util.swing;
import  samer.core.*;
import  java.awt.*;
import  java.io.*;
import	javax.swing.*;

/**
		<p>
		A class which can display messages in a scrolling text
		area, which can be put in another container or its own frame.
		There is a static reference to the current Console so
		that anyone can display messages without worrying about
		who created the Console.

		<p>
		Associated with the Console are a Writer and an OutputStream
		so that any method which writes to a Java IO stream can be
		redirected to the current console.

 */

public class Console extends JTextArea implements Agent
{
	private Writer			writer=null;
	private OutputStream	ostream=null;

	public Console() { this(true); }
	public Console(boolean setAsDefault)
	{
		super("",16,40);

		// setBackground( X.color(Shell.datum("swing.output.console.background"), getBackground()));
		// setForeground( X.color(Shell.datum("swing.output.console.foreground"), getForeground()));
		Font fnt=X.font(Shell.datum("swing.output.console.font"),null);
		if (fnt!=null) setFont(fnt);

		setEditable(false);
		setLineWrap(true);

		writer  = new Writer();
		ostream = new OutputStream();
	}

	public String toString() { return "samer.core.util.swing.Console"; }
	public void write( String s) { append(s); }
	public void getCommands(Agent.Registry r) { r.add("clear").add("setfont"); }
	public void execute(String cmd, Environment env) throws Exception
	{
		if (cmd.equals("clear")) setText("");
		else if (cmd.equals("setfont")) 
			setFont(X.font(env.datum("font"),null));
	}

	public Writer getWriter() {
		if (writer==null) writer = new Writer();
		return writer;
	}

	public OutputStream getStream() {
		if (ostream==null) ostream = new OutputStream();
		return ostream;
	}

	class Writer extends java.io.Writer
	{
		StringBuffer	str;

		Writer() { str = new StringBuffer(); }

		public void write( char buf[], int off, int len) {
			str.append( buf, off, len); // indentation
		}

		public void flush() { 
//			append( str.toString()); 
			try { append( str.toString()); }
			catch(IOException ex) { /* eh? */}
			str.setLength(0); 
		}
		public void close() { }
	}
	
	class OutputStream extends java.io.OutputStream
	{
		StringBuffer	str;

		OutputStream() { str = new StringBuffer(); }

		public void write( int b) { str.append( (char)b); }		
		public void flush()	{ append( str.toString()); str.setLength(0); }
		public void close() { }
	}
}