8
|
1 package rep;
|
|
2
|
126
|
3 import rep.channel.REPSocketChannel;
|
8
|
4
|
319
|
5 public class EditorPlus {
|
8
|
6
|
356
|
7 public int eid; // globally unique
|
319
|
8 public int sid=-1; // globally unique
|
|
9 public String host;
|
|
10 public String file;
|
|
11 public REPSocketChannel<REPCommand> channel;
|
|
12
|
|
13 public EditorPlus() {
|
|
14
|
|
15 }
|
|
16
|
|
17 public EditorPlus(int eid, REPSocketChannel<REPCommand> channel) {
|
8
|
18 this.eid = eid;
|
|
19 this.channel = channel;
|
|
20 }
|
319
|
21
|
|
22 public String getName() {
|
|
23 return file;
|
|
24 }
|
|
25
|
|
26 public void setName(String string) {
|
|
27 file = string;
|
|
28 }
|
|
29
|
|
30
|
|
31 public void setSID(int sid) {
|
|
32 this.sid = sid;
|
|
33 }
|
|
34
|
|
35 public int getSID() {
|
|
36 return sid;
|
|
37 }
|
324
|
38
|
|
39 public boolean hasSession() {
|
|
40 return sid != -1;
|
|
41 }
|
319
|
42
|
8
|
43 public String toString(){
|
|
44 return ("Editor:" + eid);
|
|
45 }
|
319
|
46
|
|
47 public void setEID(int eid) {
|
|
48 this.eid = eid;
|
|
49 }
|
|
50
|
8
|
51 public int getEID(){
|
|
52 return eid;
|
|
53 }
|
319
|
54
|
|
55 public void setHost(String host){
|
349
|
56 if (channel!=null)
|
|
57 this.host = host;
|
319
|
58 }
|
|
59
|
|
60
|
|
61 public String getHost(){
|
|
62 return host;
|
|
63 }
|
|
64 public REPSocketChannel<REPCommand> getChannel(){
|
8
|
65 return channel;
|
|
66
|
|
67 }
|
319
|
68 public void setChannel(REPSocketChannel<REPCommand> channel) {
|
|
69 this.channel = channel;
|
|
70 }
|
8
|
71 }
|