module author Paolo Masci
 *  date copyright import { PvsDefinition } from '../common/serverInterface' ; import { TextDocument , Position , CancellationToken , Hover , Range } from 'vscode-languageserver' ; import { MarkedString } from 'vscode-languageserver-types' ; import { PvsDefinitionProvider } from "./pvsDefinitionProvider" ; import * as language from "../common/languageKeywords" ; import * as fsUtils from '../common/fsUtils' ; import * as utils from '../common/languageUtils' ; export class PvsHoverProvider { /**`
     * Pointer to the definition provider
     */ private definitionProvider : PvsDefinitionProvider ; param definitionProvider constructor ( definitionProvider ) { this . definitionProvider = definitionProvider ; } param desc param position param token async provideHover ( desc , token ? ) { if ( desc && desc . txt && desc . uri && desc . position ) { let contents = [ ] ; const line = fsUtils . getText ( desc . txt , { start : { line : desc . position . line } , end : { line : desc . position . line } } ) ; const commentRegex = new RegExp ( language . PVS_COMMENT_REGEXP_SOURCE ) ; const matchComment = commentRegex . exec ( line ) ; const isComment = matchComment && matchComment . index <= desc . position . character ; if ( isComment ) { return null ; } const ans = await this . definitionProvider . getDefinition ( desc ) ; if ( ans ) { const definitions = ans . definitions ; if ( definitions && definitions . length > 0 ) { const sameTheoryDefs = definitions . filter ( ( def ) => { return def . symbolDeclarationFile === desc . uri ; } ) ; const def = ( sameTheoryDefs && sameTheoryDefs . length > 0 ) ? sameTheoryDefs [ 0 ] : definitions [ 0 ] ; if ( def . error ) { contents . push ( def . error . message ) ; } else { if ( def . comment ) { contents . push ( { value : def . comment , language : "pvs" } ) ; } if ( definitions . length > 1 ) { contents . push ( `Symbol ${ ans . symbolName } is overloaded: ${ definitions . length } definitions found.` ) ; contents . push ( `This tooltip shows one definition. Use peek-definition to view all definitions.` ) ; } if ( def . symbolTheory && def . symbolDeclaration ) { if ( def . symbolDeclarationRange && def . symbolDeclarationFile ) { const fileName = fsUtils . getFileName ( def . symbolDeclarationFile ) ; const link = `[${ fileName } (Ln ${ def . symbolDeclarationRange . start . line }, Col ${ def . symbolDeclarationRange . start . character })]` + `(file://${ def . symbolDeclarationFile }` + `#L${ def . symbolDeclarationRange . start . line })` ; contents . push ( link ) ; } const content = { value : def . symbolDeclaration , language : "pvs" } ; contents . push ( content ) ; } } } else { const link = `[${ ans . symbolName }](file://${ desc . uri }#L${ desc . position . line + 1 })` ; contents . push ( `No definition found for ${ link }` ) ; } } return { contents : contents , range : { start : desc . position , end : desc . position } } ; } return null ; } }