import { Connection } from "vscode-languageserver" ; import { PvsError } from "./common/pvs-gui" ; import { ProofExecDidFailToStartProof , serverEvent } from "./common/serverInterface" ; import * as fsUtils from './common/fsUtils' ; import { ProcessCode } from "./pvsProcess" ; export class PvsErrorManager { protected connection : Connection ; /**
     * Constructor
     */ constructor ( connection ) { this . connection = connection ; } /**
     * Handler for prove-formula errors
     */ handleProveFormulaError ( desc ) { console . error ( desc ?. response ) ; const evt = { action : "did-fail-to-start-proof" , msg : desc ?. response ?. error ?. message } ; this . connection ?. sendNotification ( serverEvent . proverEvent , evt ) ; if ( desc ?. autorun ) { this . connection ?. sendRequest ( serverEvent . autorunFormulaResponse , { status : "untried" , error : `Unable to run proof ${ desc ?. request ?. formulaName }` } ) ; } else { this . connection ?. sendNotification ( `server.status.end-important-task-${ desc . taskId }` , desc ) ; } } /**
     * Handler for start-evaluator errors
     */ handleEvaluationError ( desc ) { if ( desc ) { if ( desc . taskId ) { const msg = `Typecheck errors in ${ desc . request . fileName }${ desc . request . fileExtension }.\nPlease fix the typecheck errors before trying to start the evaluator on theory ${ desc . request . theoryName }.` ; this . notifyEndImportantTaskWithErrors ( { id : desc . taskId , msg } ) ; } else { const msg = ( desc . response . error && desc . response . error . message ) ? desc . response . error . message : `Error: PVSio crashed into Lisp. Please start a new evaluator session.` ; this . notifyError ( { msg } ) ; console . error ( `[pvs-language-server] ${ msg }` ) ; } } } /**
     * Handler for typecheck-file errors
     */ handleTypecheckError ( desc ) { if ( desc && desc . response && desc . response . error ) { if ( desc . response . error . data ) { const fname = ( desc . response . error . data . file_name ) ? desc . response . error . data . file_name : fsUtils . desc2fname ( desc . request ) ; const msg = desc . response . error . data . error_string || "" ; if ( desc . taskId ) { if ( fname === fsUtils . desc2fname ( desc . request ) ) { this . notifyEndImportantTaskWithErrors ( { id : desc . taskId , msg : `Typecheck errors in ${ desc . request . fileName }${ desc . request . fileExtension }: ${ msg }` } ) ; } else { this . notifyEndImportantTaskWithErrors ( { id : desc . taskId , msg : `File ${ fsUtils . getFileName ( fname ) }${ fsUtils . getFileExtension ( fname ) } imported by ${ desc . request . fileName }${ desc . request . fileExtension } contains typecheck errors.` } ) ; } } } else if ( desc . response . error . message ) { this . notifyEndImportantTaskWithErrors ( { id : desc . taskId , msg : desc . response . error . message } ) ; } } } /**
     * Handler for show-tccs errors
     */ handleShowTccsError ( desc ) { if ( desc ) { const msg = ( desc ?. response ?. error ) ? JSON . stringify ( desc . response . error ) : `Error: tccs could not be generated (please check pvs-server output for details)` ; this . notifyError ( { msg } ) ; console . error ( `[pvs-language-server.showTccs] Error: tccs could not be generated` , desc . response ) ; } } param success handleStartPvsServerError ( success ) { switch ( success ) { case ProcessCode . SUCCESS : { break ; } case ProcessCode . PVSNOTFOUND : { this . connection ?. sendRequest ( serverEvent . pvsNotFound ) ; break ; } case ProcessCode . UNSUPPORTEDPLATFORM : { const platform = process . platform ; this . connection ?. sendRequest ( serverEvent . pvsServerFail , { msg : `Error: Unsupported platform '${ platform }'.` } ) ; break ; } default : { this . connection ?. sendRequest ( serverEvent . pvsServerFail ) ; break ; } } } notifyEndImportantTaskWithErrors ( desc ) { this . connection ?. sendNotification ( `server.status.end-important-task-${ desc . id }-with-errors` , desc ) ; } notifyPvsFailure ( opt ? ) { this . connection ?. sendNotification ( "server.status.pvs-failure" , opt ) ; } notifyError ( desc ) { this . connection ?. sendNotification ( "server.status.error" , desc ) ; } notifyPvsNotFound ( pvsPath ) { const msg = `PVS executable not found at ${ pvsPath }` ; console . error ( msg ) ; this . connection ?. sendRequest ( serverEvent . pvsNotFound , msg ) ; } }