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: 1. 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.