module author Paolo Masci
 *  date copyright import { CancellationToken , CodeLens , CodeLensRequest , Range , CodeLensParams , Position } from 'vscode-languageserver' ; import * as fsUtils from '../common/fsUtils' ; import * as utils from '../common/languageUtils' ; import { CopyProofliteRequest , GotoFileDescriptor , ProveFormulaRequest , PvsFormula , PvsTheory } from '../common/serverInterface' ; import { PvsLanguageServer } from '../pvsLanguageServer' ; export class PvsCodeLensProvider { protected pvsLanguageServer : PvsLanguageServer ; param pvsLanguageServer constructor ( pvsLanguageServer ) { this . pvsLanguageServer = pvsLanguageServer ; } param document param position param token provideCodeLens ( document , token ? ) { if ( document && ! this . pvsLanguageServer . isPreludeFile ( document . uri ) ) { let fileName = fsUtils . getFileName ( document . uri ) ; const fileExtension = fsUtils . getFileExtension ( document . uri ) ; const contextFolder = fsUtils . getContextFolder ( document . uri ) ; let match = null ; const codeLens = [ ] ; const content = document . txt . replace ( utils . commentRegexp , "" ) ; if ( fileExtension === ".pvs" ) { const regex = new RegExp ( utils . theoryOrDatatypeRegexp ) ; while ( match = regex . exec ( content ) ) { if ( match . length > 1 && match [ 1 ] ) { const theoryName = match [ 1 ] ; const docUp = content . slice ( 0 , match . index + theoryName . length ) ; const lines = docUp . split ( "\n" ) ; const line = lines . length - 1 ; const character = lines [ lines . length - 1 ] . indexOf ( theoryName ) ; const theory = { fileName , fileExtension , contextFolder , theoryName , } ; const range = { start : { line , character } , end : { line , character : character + theoryName . length } } ; codeLens . push ( { range , command : { title : "typecheck-file" , command : "vscode-pvs.typecheck-file" , arguments : [ theory ] } } ) ; codeLens . push ( { range , command : { title : "evaluate-in-pvsio" , command : "vscode-pvs.pvsio-evaluator" , arguments : [ theory ] } } ) ; } } } if ( fileExtension === ".pvs" || fileExtension === ".tccs" ) { const regex = new RegExp ( utils . theoremRegexp ) ; while ( match = regex . exec ( content ) ) { if ( match . length > 1 && match [ 1 ] ) { const formulaName = match [ 1 ] ; const docUp = content . slice ( 0 , match . index + formulaName . length ) ; const lines = docUp . split ( "\n" ) ; const line = lines . length - 1 ; const character = lines [ lines . length - 1 ] . indexOf ( match [ 1 ] ) ; let theoryName = fsUtils . findTheoryName ( content , line ) ; if ( theoryName ) { const formula = { fileName , fileExtension , contextFolder , theoryName : ( fileExtension === ".tccs" ) ? theoryName . substr ( 0 , theoryName . length - 5 ) : theoryName , formulaName , line : fileExtension === ".tccs" ? line - 3 : line } ; const range = { start : { line , character } , end : { line , character : character + formulaName . length } } ; codeLens . push ( { range , command : { title : "prove" , command : "vscode-pvs.prove-formula" , arguments : [ formula ] } } ) ; codeLens . push ( { range , command : { title : "status-proofchain" , command : "vscode-pvs.status-proofchain" , arguments : [ formula ] } } ) ; codeLens . push ( { range , command : { title : "show-prooflite" , command : "vscode-pvs.show-prooflite" , arguments : [ formula ] } } ) ; } } } } if ( fileExtension === ".tccs" ) { const regex = new RegExp ( /\(at (line (\d+), column (\d+))\)(?:[\s%]+for[\s%]+(.*)[\s%]+expected\b)?/g ) ; while ( match = regex . exec ( document . txt ) ) { const lines = document . txt . slice ( 0 , match . index ) . split ( "\n" ) ; let line = lines . length - 1 ; const character = lines [ line ] . length ; const docDown = document . txt . slice ( match . index ) ; const regexObligation = new RegExp ( utils . tccRegexp ) ; const matchObligation = regexObligation . exec ( docDown ) ; if ( matchObligation ?. length && matchObligation [ 1 ] ) { line += docDown . slice ( 0 , matchObligation . index ) ?. split ( "\n" ) ?. length - 1 ; } const range = { start : { line , character } , end : { line , character : character + match [ 0 ] . length } } ; const gotoPosition = { line : + match [ 2 ] - 1 , character : + match [ 3 ] } ; const gotoRange = { start : gotoPosition , end : { line : gotoPosition . line , character : gotoPosition . character } } ; const gotoDesc = { contextFolder , fileName , fileExtension : ".pvs" , pos : gotoPosition , range : gotoRange } ; codeLens . push ( { range , command : { title : `(goto ${ match [ 1 ] })` , command : "vscode-pvs.goto-pvs-file" , arguments : [ gotoDesc ] } } ) ; } } if ( fileExtension === ".prlite" || fileExtension === ".prl" ) { const regex = new RegExp ( utils . proofRegexp ) ; while ( match = regex . exec ( content ) ) { if ( match . length > 1 && match [ 1 ] ) { const formulaName = match [ 1 ] ; const theoryName = fileName ; const matchFileName = utils . proofliteTagsRegexp ( { theoryName , formulaName } ) . exec ( document . txt ) ; if ( matchFileName && matchFileName . length > 1 ) { fileName = fsUtils . getFileName ( matchFileName [ 1 ] ) ; } const docUp = content . slice ( 0 , match . index + theoryName . length ) ; const lines = docUp . split ( "\n" ) ; const line = lines . length - 1 ; const character = 0 ; const realContextFolder = contextFolder . endsWith ( "/pvsbin" ) || contextFolder . endsWith ( "/pvsbin/" ) ? contextFolder . substring ( 0 , contextFolder . lastIndexOf ( "/pvsbin" ) ) : contextFolder ; const proveFormulaArgs = { fileName , fileExtension : ( utils . tccFormulaRegexp . test ( formulaName ) ) ? ".tccs" : ".pvs" , contextFolder : realContextFolder , theoryName , formulaName , origin : "prooflite" , proofFile : { fileName , fileExtension , contextFolder } } ; const range = { start : { line , character } , end : { line , character : character + theoryName . length } } ; codeLens . push ( { range , command : { title : "prove" , command : "vscode-pvs.prove-formula" , arguments : [ proveFormulaArgs ] } } ) ; const matchProoflite = utils . proofliteRegexp ( { theoryName , formulaName } ) . exec ( content ) ; const prooflite = matchProoflite && matchProoflite . length ? matchProoflite [ 0 ] . trim ( ) : null ; const insertProofliteArgs = { fileName , fileExtension : ( utils . tccFormulaRegexp . test ( formulaName ) ) ? ".tccs" : ".pvs" , contextFolder : realContextFolder , theoryName , formulaName , prooflite } ; codeLens . push ( { range , command : { title : "copy-prooflite" , command : "vscode-pvs.copy-prooflite" , arguments : [ insertProofliteArgs ] } } ) ; } } } if ( fileExtension === ".pvs" ) { const regexs = [ new RegExp ( utils . linearPlotTupleTupleListRegexp ) , new RegExp ( utils . linearPlotRegexp ) , new RegExp ( utils . linearPlotSimpleRegexp ) , new RegExp ( utils . scatterPlotRegexp ) ] ; for ( let i = 0 ; i < regexs . length ; i ++ ) { while ( match = regexs [ i ] . exec ( content ) ) { if ( match . length > 1 && match [ 1 ] ) { const formulaName = match [ 1 ] ; const docUp = content . slice ( 0 , match . index + formulaName . length ) ; const lines = docUp . split ( "\n" ) ; const line = lines . length - 1 ; const character = lines [ lines . length - 1 ] . indexOf ( match [ 1 ] ) ; if ( fileName ) { const args = { path : document . uri , expr : formulaName } ; const range = { start : { line , character } , end : { line , character : character + formulaName . length } } ; codeLens . push ( { range , command : { title : "plot-expression" , command : "vscode-pvs.plot-expression" , arguments : [ args ] } } ) ; } } } } } return Promise . resolve ( codeLens ) ; } return Promise . resolve ( [ ] ) ; } resolveCodeLens ( codeLens , token ? ) { return codeLens ; } async onCodeLens ( args , txt ) { const uri = args ?. textDocument ?. uri ; if ( fsUtils . isPvsFile ( uri ) ) { let codelens = await this . provideCodeLens ( { txt , uri } ) ; return codelens ; } return null ; } }