Opened 17 years ago

Last modified 11 years ago

#99 new defect

Reliable interrupts

Reported by: David Aspinall Owned by: David Aspinall
Priority: major Milestone:
Component: 4:prover-isabelle Keywords:
Cc:

Description


Change History (2)

comment:1 Changed 16 years ago by Makarius

Interrupts should work properly as follows:

  • On the JVM side, invoke "kill" command with PID as provided by Isabelle process (cf. option -W).
  • On the Isabelle side, use the official toplevel, together with the Isabelle.command command, or with in-line XML commands that may be available at some later stage.

Alternatively, refrain from implementing a separate process wrapper, but use the one of post-Isabelle2007 versions (cf. Isabelle/lib/classes/isabelle/IsabelleProcess.java, which is meant to become rock-solid eventually). This essentially means to move most PGIP wrapping out of Isabelle, into the JVM, past the process wrapper.

comment:2 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.1.0

Milestone PG-Eclipse-1.1.0 deleted

Note: See TracTickets for help on using tickets.