blob: debb26e0c3f897eb0260bb4f6821870f94d3f638 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
package bjc.everge;
import java.io.PrintStream;
/**
* Options for processing ReplPairs.
*
* @author Ben Culkin.
*/
public class ReplOpts {
/**
* The default priority.
*/
public int defPrior = 0;
/**
* The default stage.
*/
public int defStage = 0;
/**
* Whether to process multi-line defns.
*/
public boolean defMulti = false;
/**
* Default status.
*/
public StageStatus defStatus = StageStatus.BOTH;
/**
* Enable debug info.
*/
public boolean isDebug = true;
/**
* Enable trace info.
*/
public boolean isTrace = false;
/**
* Enable performance info.
*/
public boolean isPerf = false;
/**
* The stream to print normal output on.
*/
public PrintStream outStream = System.out;
/**
* The stream to print error output on.
*/
public PrintStream errStream = System.err;
@Override
public int hashCode() {
final int prime = 31;
int result = 1;
result = prime * result + (defMulti ? 1231 : 1237);
result = prime * result + defPrior;
result = prime * result + defStage;
result = prime * result + ((defStatus == null) ? 0 : defStatus.hashCode());
result = prime * result + (isDebug ? 1231 : 1237);
result = prime * result + (isPerf ? 1231 : 1237);
result = prime * result + (isTrace ? 1231 : 1237);
return result;
}
@Override
public boolean equals(Object obj) {
if (this == obj)
return true;
if (obj == null)
return false;
if (getClass() != obj.getClass())
return false;
ReplOpts other = (ReplOpts) obj;
if (defMulti != other.defMulti)
return false;
if (defPrior != other.defPrior)
return false;
if (defStage != other.defStage)
return false;
if (defStatus != other.defStatus)
return false;
if (isDebug != other.isDebug)
return false;
if (isPerf != other.isPerf)
return false;
if (isTrace != other.isTrace)
return false;
return true;
}
}
|
