118 |
111 |
119 |
112 |
120 /* signals */ |
113 /* signals */ |
121 |
114 |
122 def interrupt() = synchronized { |
115 def interrupt() = synchronized { |
123 if (proc == null) throw new IsabelleProcessException("Cannot interrupt: no process") |
116 if (proc == null) error("Cannot interrupt Isabelle: no process") |
124 if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid") |
117 if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid") |
125 else { |
118 else { |
126 try { |
119 try { |
127 if (IsabelleSystem.exec(List("kill", "-INT", pid)).waitFor == 0) |
120 if (IsabelleSystem.exec(List("kill", "-INT", pid)).waitFor == 0) |
128 put_result(Kind.SIGNAL, null, "INT") |
121 put_result(Kind.SIGNAL, null, "INT") |
129 else |
122 else |
130 put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed") |
123 put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed") |
131 } |
124 } |
132 catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) } |
125 catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) } |
133 } |
126 } |
134 } |
127 } |
135 |
128 |
136 def kill() = synchronized { |
129 def kill() = synchronized { |
137 if (proc == 0) throw new IsabelleProcessException("Cannot kill: no process") |
130 if (proc == 0) error("Cannot kill Isabelle: no process") |
138 else { |
131 else { |
139 try_close() |
132 try_close() |
140 Thread.sleep(500) |
133 Thread.sleep(500) |
141 put_result(Kind.SIGNAL, null, "KILL") |
134 put_result(Kind.SIGNAL, null, "KILL") |
142 proc.destroy |
135 proc.destroy |
149 /* output being piped into the process */ |
142 /* output being piped into the process */ |
150 |
143 |
151 private val output = new LinkedBlockingQueue[String] |
144 private val output = new LinkedBlockingQueue[String] |
152 |
145 |
153 def output_raw(text: String) = synchronized { |
146 def output_raw(text: String) = synchronized { |
154 if (proc == null) throw new IsabelleProcessException("Cannot output: no process") |
147 if (proc == null) error("Cannot output to Isabelle: no process") |
155 if (closing) throw new IsabelleProcessException("Cannot output: already closing") |
148 if (closing) error("Cannot output to Isabelle: already closing") |
156 output.put(text) |
149 output.put(text) |
157 } |
150 } |
158 |
151 |
159 def output_sync(text: String) = output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n") |
152 def output_sync(text: String) = output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n") |
160 |
153 |
359 |
352 |
360 try { |
353 try { |
361 proc = IsabelleSystem.exec(List( |
354 proc = IsabelleSystem.exec(List( |
362 IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args) |
355 IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args) |
363 } |
356 } |
364 catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) } |
357 catch { |
|
358 case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage) |
|
359 } |
365 |
360 |
366 |
361 |
367 /* control process via threads */ |
362 /* control process via threads */ |
368 |
363 |
369 val charset = "UTF-8" |
364 val charset = "UTF-8" |