author | wenzelm |
Wed, 15 Jan 2020 19:54:50 +0100 | |
changeset 71383 | 8313dca6dee9 |
parent 70301 | 9f2a6856b912 |
child 71713 | 928fd852f3e2 |
permissions | -rw-r--r-- |
67802 | 1 |
/* Title: Pure/System/tty_loop.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Line-oriented TTY loop. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
67836 | 10 |
import java.io.{IOException, Writer, Reader, InputStreamReader, BufferedReader} |
67802 | 11 |
|
12 |
||
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67836
diff
changeset
|
13 |
class TTY_Loop(writer: Writer, reader: Reader, |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67836
diff
changeset
|
14 |
writer_lock: AnyRef = new Object, |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67836
diff
changeset
|
15 |
interrupt: Option[() => Unit] = None) |
67802 | 16 |
{ |
17 |
private val console_output = Future.thread[Unit]("console_output") { |
|
18 |
try { |
|
19 |
var result = new StringBuilder(100) |
|
20 |
var finished = false |
|
21 |
while (!finished) { |
|
22 |
var c = -1 |
|
23 |
var done = false |
|
71383 | 24 |
while (!done && (result.isEmpty || reader.ready)) { |
67833 | 25 |
c = reader.read |
67802 | 26 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
27 |
else done = true |
|
28 |
} |
|
71383 | 29 |
if (result.nonEmpty) { |
67802 | 30 |
System.out.print(result.toString) |
31 |
System.out.flush() |
|
70301 | 32 |
result.clear |
67802 | 33 |
} |
34 |
else { |
|
67833 | 35 |
reader.close() |
67802 | 36 |
finished = true |
37 |
} |
|
38 |
} |
|
39 |
} |
|
40 |
catch { case e: IOException => case Exn.Interrupt() => } |
|
41 |
} |
|
42 |
||
43 |
private val console_input = Future.thread[Unit]("console_input") { |
|
44 |
val console_reader = new BufferedReader(new InputStreamReader(System.in)) |
|
67808 | 45 |
def body |
46 |
{ |
|
67802 | 47 |
try { |
48 |
var finished = false |
|
49 |
while (!finished) { |
|
50 |
console_reader.readLine() match { |
|
51 |
case null => |
|
67833 | 52 |
writer.close() |
67802 | 53 |
finished = true |
54 |
case line => |
|
67839
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67836
diff
changeset
|
55 |
writer_lock.synchronized { |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67836
diff
changeset
|
56 |
writer.write(line) |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67836
diff
changeset
|
57 |
writer.write("\n") |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67836
diff
changeset
|
58 |
writer.flush() |
0c2ed45ece20
explicit Server.Context with output channels (concurrent write);
wenzelm
parents:
67836
diff
changeset
|
59 |
} |
67802 | 60 |
} |
61 |
} |
|
62 |
} |
|
63 |
catch { case e: IOException => case Exn.Interrupt() => } |
|
64 |
} |
|
67833 | 65 |
interrupt match { |
67808 | 66 |
case None => body |
67833 | 67 |
case Some(int) => POSIX_Interrupt.handler { int() } { body } |
67808 | 68 |
} |
67802 | 69 |
} |
70 |
||
71 |
def join { console_output.join; console_input.join } |
|
72 |
||
73 |
def cancel { console_input.cancel } |
|
74 |
} |