Method: write(String, int, int)

1: /*******************************************************************************
2: *
3: *        Copyright (C) 2008 Fujitsu Services Ltd.
4: *
5: *        Author: Nick Battle
6: *
7: *        This file is part of VDMJ.
8: *
9: *        VDMJ is free software: you can redistribute it and/or modify
10: *        it under the terms of the GNU General Public License as published by
11: *        the Free Software Foundation, either version 3 of the License, or
12: *        (at your option) any later version.
13: *
14: *        VDMJ is distributed in the hope that it will be useful,
15: *        but WITHOUT ANY WARRANTY; without even the implied warranty of
16: *        MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
17: *        GNU General Public License for more details.
18: *
19: *        You should have received a copy of the GNU General Public License
20: *        along with VDMJ. If not, see <http://www.gnu.org/licenses/>.
21: *
22: ******************************************************************************/
23:
24: package org.overture.interpreter.messages;
25:
26: import java.io.BufferedReader;
27: import java.io.InputStreamReader;
28: import java.io.OutputStreamWriter;
29: import java.io.UnsupportedEncodingException;
30: import java.nio.charset.Charset;
31:
32: import org.overture.interpreter.debug.DBGPReader;
33: import org.overture.interpreter.debug.DBGPRedirect;
34:
35: public class Console
36: {
37:         /** The charset for the console. */
38:         public static String charset;
39:
40:         /** A print writer for stdout that uses a given encoding. */
41:         public static Redirector out;
42:
43:         /** A print writer for stderr that uses a given encoding. */
44:         public static Redirector err;
45:
46:         /** A buffered reader for stdin that uses a given encoding. */
47:         public static BufferedReader in;
48:
49:         static
50:         {
51:                 init(Charset.defaultCharset().name());
52:         }
53:
54:         public static void setCharset(String cs)
55:         {
56:                 init(cs);
57:         }
58:
59:         private static void init(String cs)
60:         {
61:                 try
62:                 {
63:                         charset = cs;
64:                         out = new StdoutRedirector(new OutputStreamWriter(System.out, charset));
65:                         err = new StderrRedirector(new OutputStreamWriter(System.err, charset));
66:                         in = new BufferedReader(new InputStreamReader(System.in, charset));
67:                 } catch (UnsupportedEncodingException e)
68:                 {
69:                         System.err.println("Console encoding exception: " + e);
70:                 }
71:         }
72:
73:         public static synchronized void directStdout(DBGPReader reader,
74:                         DBGPRedirect redirect)
75:         {
76:                 out.redirect(redirect, reader);
77:         }
78:
79:         public static synchronized void directStderr(DBGPReader reader,
80:                         DBGPRedirect redirect)
81:         {
82:                 err.redirect(redirect, reader);
83:         }
84:
85:         public static class DisabledStdOut extends StdoutRedirector
86:         {
87:
88:                 public DisabledStdOut(OutputStreamWriter out)
89:                 {
90:                         super(out);
91:                 }
92:
93:                 @Override
94:                 public void write(String s, int off, int len)
95:                 {
96:
97:                 }
98:
99:                 @Override
100:                 public void print(String line)
101:                 {
102:
103:                 }
104:
105:         }
106:
107:         public static synchronized void disableStdout()
108:         {
109:                 try
110:                 {
111:                         out = new DisabledStdOut(new OutputStreamWriter(System.out, charset));
112:                 } catch (UnsupportedEncodingException e)
113:                 {
114:                         System.err.println("Console encoding exception: " + e);
115:                 }
116:         }
117:
118:         public static synchronized void disableStderr()
119:         {
120:                 try
121:                 {
122:                         err = new DisabledStdOut(new OutputStreamWriter(System.err, charset));
123:                 } catch (UnsupportedEncodingException e)
124:                 {
125:                         System.err.println("Console encoding exception: " + e);
126:                 }
127:         }
128: }