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).

Change History (1)

comment:1 Changed 11 years ago by David Aspinall

Milestone: Future

Milestone Future deleted

Note: See TracTickets for help on using tickets.