more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
package GraphBrowser;
class ParseError extends Exception {
public ParseError(String s) { super(s); }
}