Opened 17 years ago
Last modified 11 years ago
#151 new defect
Make interface multiple-thread aware
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 4:prover-isabelle | Keywords: | |
Cc: |
Description
New multiple thread support in Isabelle should be exploited by close connection with the interface, to allow flexible spawning, interrupting and progress reporting.
We also need to add further support to PGIP for this, although it is already possible to indicate commands which can be dealt with asynchronously by the prover (e.g., we want =<parsescript>= and =<showid>= messages to be in this category).
Note: See
TracTickets for help on using
tickets.
Milestone Future deleted