equal
deleted
inserted
replaced
17 */ |
17 */ |
18 |
18 |
19 package isabelle |
19 package isabelle |
20 |
20 |
21 |
21 |
22 import java.io.{BufferedInputStream, BufferedOutputStream, BufferedReader, BufferedWriter, |
22 import java.io.{BufferedInputStream, BufferedOutputStream, InputStreamReader, OutputStreamWriter, |
23 InputStreamReader, OutputStreamWriter, IOException} |
23 IOException} |
24 import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress} |
24 import java.net.{Socket, SocketException, SocketTimeoutException, ServerSocket, InetAddress} |
25 |
25 |
26 |
26 |
27 object Server |
27 object Server |
28 { |
28 { |
107 |
107 |
108 def close() { socket.close } |
108 def close() { socket.close } |
109 |
109 |
110 def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) } |
110 def set_timeout(t: Time) { socket.setSoTimeout(t.ms.toInt) } |
111 |
111 |
112 def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop = |
|
113 new TTY_Loop( |
|
114 new BufferedWriter(new OutputStreamWriter(socket.getOutputStream)), |
|
115 new BufferedReader(new InputStreamReader(socket.getInputStream)), |
|
116 interrupt = interrupt) |
|
117 |
|
118 private val in = new BufferedInputStream(socket.getInputStream) |
112 private val in = new BufferedInputStream(socket.getInputStream) |
119 private val out = new BufferedOutputStream(socket.getOutputStream) |
113 private val out = new BufferedOutputStream(socket.getOutputStream) |
|
114 |
|
115 def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop = |
|
116 new TTY_Loop(new OutputStreamWriter(out), new InputStreamReader(in), interrupt = interrupt) |
120 |
117 |
121 def read_message(): Option[String] = |
118 def read_message(): Option[String] = |
122 try { |
119 try { |
123 Bytes.read_line(in).map(_.text) match { |
120 Bytes.read_line(in).map(_.text) match { |
124 case Some(Value.Int(n)) => |
121 case Some(Value.Int(n)) => |