more general TTY loop;
authorwenzelm
Fri Mar 09 17:03:10 2018 +0100 (2018-03-09)
changeset 6780232d76f08023f
parent 67801 8f5f5fbe291b
child 67803 1cf4126d7bd9
more general TTY loop;
src/Pure/ML/ml_console.scala
src/Pure/System/tty_loop.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/ML/ml_console.scala	Fri Mar 09 15:43:54 2018 +0100
     1.2 +++ b/src/Pure/ML/ml_console.scala	Fri Mar 09 17:03:10 2018 +0100
     1.3 @@ -7,9 +7,6 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.io.{IOException, BufferedReader, InputStreamReader}
     1.8 -
     1.9 -
    1.10  object ML_Console
    1.11  {
    1.12    /* command line entry point */
    1.13 @@ -76,59 +73,14 @@
    1.14            session_base =
    1.15              if (raw_ml_system) None
    1.16              else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
    1.17 -      val process_output = Future.thread[Unit]("process_output") {
    1.18 -        try {
    1.19 -          var result = new StringBuilder(100)
    1.20 -          var finished = false
    1.21 -          while (!finished) {
    1.22 -            var c = -1
    1.23 -            var done = false
    1.24 -            while (!done && (result.length == 0 || process.stdout.ready)) {
    1.25 -              c = process.stdout.read
    1.26 -              if (c >= 0) result.append(c.asInstanceOf[Char])
    1.27 -              else done = true
    1.28 -            }
    1.29 -            if (result.length > 0) {
    1.30 -              System.out.print(result.toString)
    1.31 -              System.out.flush()
    1.32 -              result.length = 0
    1.33 -            }
    1.34 -            else {
    1.35 -              process.stdout.close()
    1.36 -              finished = true
    1.37 -            }
    1.38 -          }
    1.39 -        }
    1.40 -        catch { case e: IOException => case Exn.Interrupt() => }
    1.41 -      }
    1.42 -      val process_input = Future.thread[Unit]("process_input") {
    1.43 -        val reader = new BufferedReader(new InputStreamReader(System.in))
    1.44 -        POSIX_Interrupt.handler { process.interrupt } {
    1.45 -          try {
    1.46 -            var finished = false
    1.47 -            while (!finished) {
    1.48 -              reader.readLine() match {
    1.49 -                case null =>
    1.50 -                  process.stdin.close()
    1.51 -                  finished = true
    1.52 -                case line =>
    1.53 -                  process.stdin.write(line)
    1.54 -                  process.stdin.write("\n")
    1.55 -                  process.stdin.flush()
    1.56 -              }
    1.57 -            }
    1.58 -          }
    1.59 -          catch { case e: IOException => case Exn.Interrupt() => }
    1.60 -        }
    1.61 -      }
    1.62 +
    1.63 +      val tty_loop = new TTY_Loop(process.stdin, process.stdout, process.interrupt _)
    1.64        val process_result = Future.thread[Int]("process_result") {
    1.65          val rc = process.join
    1.66 -        process_input.cancel
    1.67 +        tty_loop.cancel
    1.68          rc
    1.69        }
    1.70 -
    1.71 -      process_output.join
    1.72 -      process_input.join
    1.73 +      tty_loop.join
    1.74        process_result.join
    1.75      }
    1.76    }
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/System/tty_loop.scala	Fri Mar 09 17:03:10 2018 +0100
     2.3 @@ -0,0 +1,68 @@
     2.4 +/*  Title:      Pure/System/tty_loop.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Line-oriented TTY loop.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +import java.io.{IOException, BufferedReader, BufferedWriter, InputStreamReader}
    2.14 +
    2.15 +
    2.16 +class TTY_Loop(
    2.17 +  process_writer: BufferedWriter,
    2.18 +  process_reader: BufferedReader,
    2.19 +  process_interrupt: () => Unit = () => ())
    2.20 +{
    2.21 +  private val console_output = Future.thread[Unit]("console_output") {
    2.22 +    try {
    2.23 +      var result = new StringBuilder(100)
    2.24 +      var finished = false
    2.25 +      while (!finished) {
    2.26 +        var c = -1
    2.27 +        var done = false
    2.28 +        while (!done && (result.length == 0 || process_reader.ready)) {
    2.29 +          c = process_reader.read
    2.30 +          if (c >= 0) result.append(c.asInstanceOf[Char])
    2.31 +          else done = true
    2.32 +        }
    2.33 +        if (result.length > 0) {
    2.34 +          System.out.print(result.toString)
    2.35 +          System.out.flush()
    2.36 +          result.length = 0
    2.37 +        }
    2.38 +        else {
    2.39 +          process_reader.close()
    2.40 +          finished = true
    2.41 +        }
    2.42 +      }
    2.43 +    }
    2.44 +    catch { case e: IOException => case Exn.Interrupt() => }
    2.45 +  }
    2.46 +
    2.47 +  private val console_input = Future.thread[Unit]("console_input") {
    2.48 +    val console_reader = new BufferedReader(new InputStreamReader(System.in))
    2.49 +    POSIX_Interrupt.handler { process_interrupt() } {
    2.50 +      try {
    2.51 +        var finished = false
    2.52 +        while (!finished) {
    2.53 +          console_reader.readLine() match {
    2.54 +            case null =>
    2.55 +              process_writer.close()
    2.56 +              finished = true
    2.57 +            case line =>
    2.58 +              process_writer.write(line)
    2.59 +              process_writer.write("\n")
    2.60 +              process_writer.flush()
    2.61 +          }
    2.62 +        }
    2.63 +      }
    2.64 +      catch { case e: IOException => case Exn.Interrupt() => }
    2.65 +    }
    2.66 +  }
    2.67 +
    2.68 +  def join { console_output.join; console_input.join }
    2.69 +
    2.70 +  def cancel { console_input.cancel }
    2.71 +}
     3.1 --- a/src/Pure/build-jars	Fri Mar 09 15:43:54 2018 +0100
     3.2 +++ b/src/Pure/build-jars	Fri Mar 09 17:03:10 2018 +0100
     3.3 @@ -127,6 +127,7 @@
     3.4    System/process_result.scala
     3.5    System/progress.scala
     3.6    System/system_channel.scala
     3.7 +  System/tty_loop.scala
     3.8    Thy/bibtex.scala
     3.9    Thy/html.scala
    3.10    Thy/latex.scala