equal
deleted
inserted
replaced
82 private var pid: String = null |
82 private var pid: String = null |
83 private var the_session: String = null |
83 private var the_session: String = null |
84 def session() = the_session |
84 def session() = the_session |
85 |
85 |
86 |
86 |
87 /* symbols */ |
|
88 |
|
89 val symbols = new Symbol.Interpretation |
|
90 def decode_result(result: Result) = YXML.parse_failsafe(symbols.decode(result.result)) |
|
91 |
|
92 |
|
93 /* results */ |
87 /* results */ |
94 |
88 |
95 private val results = new LinkedBlockingQueue[Result] |
89 private val results = new LinkedBlockingQueue[Result] |
96 |
90 |
97 private def put_result(kind: Kind.Value, props: Properties, result: String) { |
91 private def put_result(kind: Kind.Value, props: Properties, result: String) { |