src/Pure/System/isabelle_system.scala
changeset 38253 3d4e521014f7
parent 37367 8680677265c9
child 38255 bf44a85c74cc
equal deleted inserted replaced
38252:175a5b4b2c94 38253:3d4e521014f7
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 import java.util.regex.Pattern
     9 import java.util.regex.Pattern
    10 import java.util.Locale
    10 import java.util.Locale
    11 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
    11 import java.io.{BufferedInputStream, FileInputStream, BufferedOutputStream, FileOutputStream,
    12   BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
    12   OutputStream, File, IOException}
    13   File, IOException}
       
    14 import java.awt.{GraphicsEnvironment, Font}
    13 import java.awt.{GraphicsEnvironment, Font}
    15 import java.awt.font.TextAttribute
    14 import java.awt.font.TextAttribute
    16 
    15 
    17 import scala.io.Source
    16 import scala.io.Source
    18 import scala.util.matching.Regex
    17 import scala.util.matching.Regex
   286   {
   285   {
   287     val (result, rc) = isabelle_tool("rmfifo", fifo)
   286     val (result, rc) = isabelle_tool("rmfifo", fifo)
   288     if (rc != 0) error(result)
   287     if (rc != 0) error(result)
   289   }
   288   }
   290 
   289 
   291   def fifo_stream(fifo: String): BufferedInputStream =
   290   def fifo_input_stream(fifo: String): BufferedInputStream =
   292   {
   291   {
   293     // blocks until writer is ready
   292     // block until peer is ready
   294     val stream =
   293     val stream =
   295       if (Platform.is_windows) {
   294       if (Platform.is_windows) {
       
   295         // Cygwin fifo as Windows/Java input stream
   296         val proc = execute(false, "cat", fifo)
   296         val proc = execute(false, "cat", fifo)
   297         proc.getOutputStream.close
   297         proc.getOutputStream.close
   298         proc.getErrorStream.close
   298         proc.getErrorStream.close
   299         proc.getInputStream
   299         proc.getInputStream
   300       }
   300       }
   301       else new FileInputStream(fifo)
   301       else new FileInputStream(fifo)
   302     new BufferedInputStream(stream)
   302     new BufferedInputStream(stream)
       
   303   }
       
   304 
       
   305   def fifo_output_stream(fifo: String): BufferedOutputStream =
       
   306   {
       
   307     // block until peer is ready
       
   308     val stream =
       
   309       if (Platform.is_windows) {
       
   310         // Cygwin fifo as Windows/Java output stream (beware of buffering)
       
   311         // FIXME FIXME FIXME
       
   312         val script =
       
   313           "open(FIFO, \">" + fifo + "\") || die $!; my $buffer; " +
       
   314           "while ((sysread STDIN, $buffer, 65536), length $buffer > 0)" +
       
   315           " { syswrite FIFO, $buffer; }; close FIFO;"
       
   316         val proc = execute(false, "perl", "-e", script)
       
   317         proc.getInputStream.close
       
   318         proc.getErrorStream.close
       
   319         val out = proc.getOutputStream
       
   320         new OutputStream {
       
   321           override def close() { out.close(); proc.waitFor() }
       
   322           override def flush() { out.flush() }
       
   323           override def write(b: Array[Byte]) { out.write(b) }
       
   324           override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
       
   325           override def write(b: Int) { out.write(b) }
       
   326         }
       
   327         proc.getOutputStream
       
   328       }
       
   329       else new FileOutputStream(fifo)
       
   330     new BufferedOutputStream(stream)
   303   }
   331   }
   304 
   332 
   305 
   333 
   306 
   334 
   307   /** Isabelle resources **/
   335   /** Isabelle resources **/