src/Pure/Tools/isabelle_process.scala
changeset 27973 18d02c0b90b6
parent 27963 c9ea82444189
child 27990 f9dd4c9ed812
     1.1 --- a/src/Pure/Tools/isabelle_process.scala	Sat Aug 23 23:07:43 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.scala	Sat Aug 23 23:07:44 2008 +0200
     1.3 @@ -16,27 +16,15 @@
     1.4  import isabelle.{Symbol, XML}
     1.5  
     1.6  
     1.7 -class IsabelleProcess(args: String*) {
     1.8 +object IsabelleProcess {
     1.9 +
    1.10 +  /* exception */
    1.11  
    1.12    class IsabelleProcessException(msg: String) extends Exception {
    1.13      override def toString = "IsabelleProcess: " + msg
    1.14    }
    1.15  
    1.16  
    1.17 -  /* process information */
    1.18 -
    1.19 -  private var proc: Process = null
    1.20 -  private var closing = false
    1.21 -  private var pid: String = null
    1.22 -  private var session: String = null
    1.23 -
    1.24 -
    1.25 -  /* encoding */
    1.26 -
    1.27 -  private val charset = "UTF-8"
    1.28 -  private val symbols = new Symbol.Interpretation
    1.29 -
    1.30 -
    1.31    /* results */
    1.32  
    1.33    object Kind extends Enumeration {
    1.34 @@ -72,36 +60,75 @@
    1.35        kind == SYSTEM
    1.36    }
    1.37  
    1.38 -  class Result(kind: Kind.Value, props: Properties, result: String) {
    1.39 -    //{{{
    1.40 +  class Result(val kind: Kind.Value, val props: Properties, val result: String) {
    1.41      override def toString = {
    1.42        val res = XML.content(YXML.parse_failsafe(result)).mkString("")
    1.43        if (props == null) kind.toString + " [[" + res + "]]"
    1.44        else kind.toString + " " + props.toString + " [[" + res + "]]"
    1.45      }
    1.46 +    def is_raw() = Kind.is_raw(kind)
    1.47 +    def is_system() = Kind.is_system(kind)
    1.48 +  }
    1.49  
    1.50 -    private var the_tree: XML.Tree = null
    1.51 -    def tree() = synchronized {
    1.52 -      if (the_tree == null) {
    1.53 -        val t = YXML.parse_failsafe(symbols.decode(result))
    1.54 -        the_tree = if (Kind.is_raw(kind)) XML.Elem(Markup.RAW, Nil, List(t)) else t
    1.55 -      }
    1.56 -      the_tree
    1.57 -    }
    1.58 -    //}}}
    1.59 -  }
    1.60 +}
    1.61 +
    1.62 +
    1.63 +class IsabelleProcess(args: String*) {
    1.64 +
    1.65 +  import IsabelleProcess._
    1.66 +
    1.67 +
    1.68 +  /* process information */
    1.69 +
    1.70 +  private var proc: Process = null
    1.71 +  private var closing = false
    1.72 +  private var pid: String = null
    1.73 +  private var the_session: String = null
    1.74 +  def session() = the_session
    1.75 +
    1.76 +
    1.77 +  /* results */
    1.78  
    1.79    val results = new LinkedBlockingQueue[Result]
    1.80  
    1.81    private def put_result(kind: Kind.Value, props: Properties, result: String) {
    1.82      if (kind == Kind.INIT && props != null) {
    1.83 -      pid = props.getProperty("pid")
    1.84 -      session = props.getProperty("session")
    1.85 +      pid = props.getProperty(Markup.PID)
    1.86 +      the_session = props.getProperty(Markup.SESSION)
    1.87      }
    1.88 -    Console.println(new Result(kind, props, result))
    1.89      results.put(new Result(kind, props, result))
    1.90    }
    1.91  
    1.92 +  val symbols = new Symbol.Interpretation
    1.93 +  def result_tree(result: Result) = YXML.parse_failsafe(symbols.decode(result.result))
    1.94 +
    1.95 +
    1.96 +  /* signals */
    1.97 +
    1.98 +  def interrupt() = synchronized {
    1.99 +    if (proc == null) throw new IsabelleProcessException("Cannot interrupt: no process")
   1.100 +    if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
   1.101 +    else {
   1.102 +      put_result(Kind.SIGNAL, null, "INT")
   1.103 +      try {
   1.104 +        if (IsabelleSystem.exec(List("kill", "-INT", pid)).waitFor != 0)
   1.105 +          put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
   1.106 +      }
   1.107 +      catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
   1.108 +    }
   1.109 +  }
   1.110 +
   1.111 +  def kill() = synchronized {
   1.112 +    if (proc == 0) throw new IsabelleProcessException("Cannot kill: no process")
   1.113 +    else {
   1.114 +      try_close()
   1.115 +      Thread.sleep(300)
   1.116 +      put_result(Kind.SIGNAL, null, "KILL")
   1.117 +      proc.destroy
   1.118 +      proc = null
   1.119 +    }
   1.120 +  }
   1.121 +
   1.122  
   1.123    /* output being piped into the process */
   1.124  
   1.125 @@ -313,29 +340,18 @@
   1.126    /** main **/
   1.127  
   1.128    {
   1.129 -    /* command line */
   1.130 -
   1.131 -    val cmdline = {
   1.132 -      val cmdline = new ArrayBuffer[String]
   1.133 +    /* exec process */
   1.134  
   1.135 -      IsabelleSystem.shell_prefix match {
   1.136 -        case None => ()
   1.137 -        case Some(prefix) => cmdline + prefix
   1.138 -      }
   1.139 -      cmdline + (IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process")
   1.140 -      cmdline + "-W"
   1.141 -      for (arg <- args) cmdline + arg
   1.142 -      cmdline.toArray
   1.143 +    try {
   1.144 +      proc = IsabelleSystem.exec(List(
   1.145 +        IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args)
   1.146      }
   1.147 -
   1.148 -    try { proc = Runtime.getRuntime.exec(cmdline) }
   1.149 -    catch {
   1.150 -      case e: IOException => throw new IsabelleProcessException(e.getMessage)
   1.151 -    }
   1.152 +    catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
   1.153  
   1.154  
   1.155 -    /* process control via threads */
   1.156 +    /* control process via threads */
   1.157  
   1.158 +    val charset = "UTF-8"
   1.159      new StdinThread(new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, charset))).start
   1.160      new StdoutThread(new BufferedReader(new InputStreamReader(proc.getInputStream, charset))).start
   1.161      new StderrThread(new BufferedReader(new InputStreamReader(proc.getErrorStream, charset))).start
   1.162 @@ -343,4 +359,3 @@
   1.163    }
   1.164  
   1.165  }
   1.166 -