Thanks---this does exactly what I want. It'll be incorporated into the next revision.
Best, Frank
Date: Mon, 30 Dec 2002 13:55:34 +0000 To: Frank Pfenning fp@cs.cmu.edu CC: polyml@inf.ed.ac.uk From: David Matthews David.Matthews@deanvillage.com Subject: Re: [polyml] Handling Interrupts
On Friday, Dec 20, 2002, at 21:24 Europe/London, Frank Pfenning wrote:
Along similar lines: I have a Twelf top-level function in server that should interrupt the current computation and return to the Twelf top-level, not to an ML debugger or the ML top-level. I saw the documentation on signals, but I don't see how to achieve the desired effect because the handler will be run in a different thread.
Any advice or help would be appreciated.
I'm not certain I've understand this exactly but I think maybe the Process.interruptConsoleProcesses function may do what you want. Processes (i.e. threads) are divided into those that receive the SML90.Interrupt exception (console processes) and those that do not. The Interrupt exception is sent to a console process in one of three cases:
- If Process.interruptConsoleProcesses is called all console
processes are interrupted 2. When a process is created using Process.console a function is returned which when called raises Interrupt in that process only. 3. All console processes will receive an Interrrupt exception when ^C is pressed followed by "f", provided the handling of ^C has not been changed using Signal.signal. It is possible to change the handling of ^C so that it raises an interrupt immediately (rather than producing the => prompt) using Signal.signal(2, Signal.SIG_HANDLE(fn _ => Process.interruptConsoleProcesses())); This is what Isabelle does from what I recall.
Regards, David.