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 + /* exec process */
1.131
1.132 - val cmdline = {
1.133 - val cmdline = new ArrayBuffer[String]
1.134 + try {
1.135 + proc = IsabelleSystem.exec(List(
1.136 + IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args)
1.137 + }
1.138 + catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
1.139
1.140 - IsabelleSystem.shell_prefix match {
1.141 - case None => ()
1.142 - case Some(prefix) => cmdline + prefix
1.143 - }
1.144 - cmdline + (IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process")
1.145 - cmdline + "-W"
1.146 - for (arg <- args) cmdline + arg
1.147 - cmdline.toArray
1.148 - }
1.149
1.150 - try { proc = Runtime.getRuntime.exec(cmdline) }
1.151 - catch {
1.152 - case e: IOException => throw new IsabelleProcessException(e.getMessage)
1.153 - }
1.154 + /* control process via threads */
1.155
1.156 -
1.157 - /* process control via threads */
1.158 -
1.159 + val charset = "UTF-8"
1.160 new StdinThread(new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, charset))).start
1.161 new StdoutThread(new BufferedReader(new InputStreamReader(proc.getInputStream, charset))).start
1.162 new StderrThread(new BufferedReader(new InputStreamReader(proc.getErrorStream, charset))).start
1.163 @@ -343,4 +359,3 @@
1.164 }
1.165
1.166 }
1.167 -