01: package interact;
02:
03: import java.io.Writer;
04: import java.io.IOException;
05: import javax.swing.text.AttributeSet;
06: import javax.swing.text.BadLocationException;
07: import javax.swing.text.PlainDocument;
08: import javax.swing.text.Position;
09:
10: /**
11: This is a Document model used by IOTextArea. It maintains an
12: output position where output should be inserted. The user can type
13: one line ahead at the bottom of the document as output is coming out.
14: <p>When the user presses return, his input is sent to a Writer.
15:
16: **/
17:
18: public class OutputDocument extends PlainDocument {
19: Position outputPos = newPosition(0);
20:
21: public OutputDocument() {
22: super ();
23: }
24:
25: /** Offset in document where next output will go. **/
26: public int getOutputOffset() {
27: return this .outputPos.getOffset();
28: }
29:
30: /** Returns where caret should go. **/
31: public int handleNewline(Writer w, int dot) {
32: int outPos = this .getOutputOffset();
33: int eob = this .getLength();
34: if (dot >= outPos && w != null) {
35: try {
36: super .insertString(eob, "\n", null);
37: w.write(this .getText(outPos, eob + 1 - outPos));
38: w.flush();
39: this .outputPos = newPosition(eob + 1);
40: } catch (IOException e) {
41: e.printStackTrace();
42: } catch (BadLocationException e) {
43: e.printStackTrace();
44: }
45: return eob + 1;
46: } else
47: return dot;
48: }
49:
50: /** Create a new Position at offset handling the annoying Exception. **/
51: private Position newPosition(int offset) {
52: try {
53: return this .createPosition(offset);
54: } catch (BadLocationException e) {
55: e.printStackTrace();
56: System.out.println("Return Position(0)!");
57: return newPosition(0);
58: }
59: }
60:
61: /**
62: This is the normal method to insert a string. If the insertion
63: point is the same as the outputPos, the outputPos will move, so
64: we need to make a new one at the old offset.
65: **/
66: public void insertString(int offset, String text, AttributeSet as)
67: throws javax.swing.text.BadLocationException {
68: int oldOffset = outputPos.getOffset();
69: super .insertString(offset, text, as);
70: if (oldOffset == offset)
71: outputPos = this .newPosition(oldOffset);
72: }
73:
74: /** Use this to insert text at the output Position. **/
75: public synchronized void insertOutput(String text, AttributeSet as) {
76: int oldOffset = outputPos.getOffset();
77: int newOffset = oldOffset + text.length();
78: try {
79: super .insertString(oldOffset, text, as);
80: } // Super!
81: catch (BadLocationException e) {
82: System.out.println("This shouldn't happen!");
83: e.printStackTrace();
84: }
85: if (outputPos.getOffset() != newOffset)
86: outputPos = this.newPosition(newOffset);
87: }
88: }
|