diff src/samer/core_/util/swing/Console.java @ 0:bf79fb79ee13

Initial Mercurial check in.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/samer/core_/util/swing/Console.java	Tue Jan 17 17:50:20 2012 +0000
@@ -0,0 +1,105 @@
+/*
+ *	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() { }
+	}
+}
+