equal
deleted
inserted
replaced
90 receiver ! new Result(message.asInstanceOf[XML.Elem])) |
90 receiver ! new Result(message.asInstanceOf[XML.Elem])) |
91 } |
91 } |
92 |
92 |
93 private def put_result(kind: String, text: String) |
93 private def put_result(kind: String, text: String) |
94 { |
94 { |
95 put_result(kind, Nil, List(XML.Text(Isabelle_System.symbols.decode(text)))) |
95 put_result(kind, Nil, List(XML.Text(Symbol.decode(text)))) |
96 } |
96 } |
97 |
97 |
98 |
98 |
99 /* input actors */ |
99 /* input actors */ |
100 |
100 |
339 if (m != -1) i += m |
339 if (m != -1) i += m |
340 } while (m != -1 && n > i) |
340 } while (m != -1 && n > i) |
341 |
341 |
342 if (i != n) throw new Protocol_Error("bad message chunk content") |
342 if (i != n) throw new Protocol_Error("bad message chunk content") |
343 |
343 |
344 YXML.parse_body_failsafe(YXML.decode_chars(Isabelle_System.symbols.decode, buf, 0, n)) |
344 YXML.parse_body_failsafe(YXML.decode_chars(Symbol.decode, buf, 0, n)) |
345 //}}} |
345 //}}} |
346 } |
346 } |
347 |
347 |
348 do { |
348 do { |
349 try { |
349 try { |