View Javadoc

1   /********************************************************************************
2    *
3    *	Copyright (c) 2009 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.overturetool.vdmj.messages;
25  
26  import java.io.OutputStreamWriter;
27  import java.io.PrintWriter;
28  
29  import org.overturetool.vdmj.debug.DBGPReader;
30  import org.overturetool.vdmj.debug.DBGPRedirect;
31  
32  abstract public class Redirector extends PrintWriter
33  {
34  	protected DBGPRedirect type;
35  	protected DBGPReader dbgp;
36  
37  	public Redirector(OutputStreamWriter out)
38  	{
39  		super(out, true);
40  		this.type = DBGPRedirect.DISABLE;
41  		this.dbgp = null;
42  	}
43  
44  	public void redirect(DBGPRedirect t, DBGPReader d)
45  	{
46  		this.type = t;
47  		this.dbgp = d;
48  	}
49  
50  	@Override
51  	public void println(String line)
52  	{
53  		print(line + "\n");
54  		flush();
55  	}
56  }