src/Pure/System/isabelle_process.scala
changeset 31797 203d5e61e3bc
parent 31498 be0f7f4f9e12
child 32448 a89f876731c5
equal deleted inserted replaced
31796:117300d72398 31797:203d5e61e3bc
    10 import java.util.concurrent.LinkedBlockingQueue
    10 import java.util.concurrent.LinkedBlockingQueue
    11 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
    11 import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
    12   InputStream, OutputStream, IOException}
    12   InputStream, OutputStream, IOException}
    13 
    13 
    14 
    14 
    15 object IsabelleProcess {
    15 object Isabelle_Process {
    16 
    16 
    17   /* results */
    17   /* results */
    18 
    18 
    19   object Kind extends Enumeration {
    19   object Kind extends Enumeration {
    20     //{{{ values and codes
    20     //{{{ values and codes
    94     def is_raw = Kind.is_raw(kind)
    94     def is_raw = Kind.is_raw(kind)
    95     def is_control = Kind.is_control(kind)
    95     def is_control = Kind.is_control(kind)
    96     def is_system = Kind.is_system(kind)
    96     def is_system = Kind.is_system(kind)
    97   }
    97   }
    98 
    98 
    99   def parse_message(isabelle_system: IsabelleSystem, result: Result) =
    99   def parse_message(isabelle_system: Isabelle_System, result: Result) =
   100   {
   100   {
   101     XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
   101     XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
   102       YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
   102       YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
   103   }
   103   }
   104 }
   104 }
   105 
   105 
   106 
   106 
   107 class IsabelleProcess(isabelle_system: IsabelleSystem,
   107 class Isabelle_Process(isabelle_system: Isabelle_System,
   108   results: EventBus[IsabelleProcess.Result], args: String*)
   108   results: EventBus[Isabelle_Process.Result], args: String*)
   109 {
   109 {
   110   import IsabelleProcess._
   110   import Isabelle_Process._
   111 
   111 
   112 
   112 
   113   /* demo constructor */
   113   /* demo constructor */
   114 
   114 
   115   def this(args: String*) =
   115   def this(args: String*) =
   116     this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
   116     this(new Isabelle_System, new EventBus[Isabelle_Process.Result] + Console.println, args: _*)
   117 
   117 
   118 
   118 
   119   /* process information */
   119   /* process information */
   120 
   120 
   121   @volatile private var proc: Process = null
   121   @volatile private var proc: Process = null
   126 
   126 
   127 
   127 
   128   /* results */
   128   /* results */
   129 
   129 
   130   def parse_message(result: Result): XML.Tree =
   130   def parse_message(result: Result): XML.Tree =
   131     IsabelleProcess.parse_message(isabelle_system, result)
   131     Isabelle_Process.parse_message(isabelle_system, result)
   132 
   132 
   133   private val result_queue = new LinkedBlockingQueue[Result]
   133   private val result_queue = new LinkedBlockingQueue[Result]
   134 
   134 
   135   private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
   135   private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
   136   {
   136   {
   228 
   228 
   229   /* stdin */
   229   /* stdin */
   230 
   230 
   231   private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
   231   private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
   232     override def run() = {
   232     override def run() = {
   233       val writer = new BufferedWriter(new OutputStreamWriter(out_stream, IsabelleSystem.charset))
   233       val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Isabelle_System.charset))
   234       var finished = false
   234       var finished = false
   235       while (!finished) {
   235       while (!finished) {
   236         try {
   236         try {
   237           //{{{
   237           //{{{
   238           val s = output.take
   238           val s = output.take
   258 
   258 
   259   /* stdout */
   259   /* stdout */
   260 
   260 
   261   private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
   261   private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
   262     override def run() = {
   262     override def run() = {
   263       val reader = new BufferedReader(new InputStreamReader(in_stream, IsabelleSystem.charset))
   263       val reader = new BufferedReader(new InputStreamReader(in_stream, Isabelle_System.charset))
   264       var result = new StringBuilder(100)
   264       var result = new StringBuilder(100)
   265 
   265 
   266       var finished = false
   266       var finished = false
   267       while (!finished) {
   267       while (!finished) {
   268         try {
   268         try {