extern int windowMode;
extern char exclusionHeader[];
-extern int highTextStart[2], highTextEnd[2];
+extern int highTextStart[2], highTextEnd[2], endPV;
// back-end called by front-end
void SetEngineState( int which, enum ENGINE_STATE state, char * state_data );