module author Paolo Masci
 *  date copyright import { RenameParams , WorkspaceEdit , TextEdit , Range , Position , Connection } from "vscode-languageserver" ; import { FormulaDescriptor , PvsFormula , TheoryDescriptor , PvsTheory , serverEvent , ServerDidRenameFile } from "../common/serverInterface" ; import * as utils from '../common/languageUtils' ; import * as fsUtils from '../common/fsUtils' ; export class PvsRenameProvider { protected connection : Connection ; constructor ( connection ) { this . connection = connection ; } async provideRename ( desc ) { const changes = { } ; if ( desc && desc . txt && desc . uri && desc . position ) { const fname = desc . uri ; const lines = desc . txt . split ( "\n" ) ; if ( lines && lines . length > desc . position . line ) { const ln = lines [ desc . position . line ] ; let character = desc . position . character ; const line = desc . position . line ; let range = utils . getWordRange ( desc . txt , desc . position ) ; const theories = await fsUtils . listTheoriesInFile ( fname , { content : desc . txt } ) ; if ( theories && theories . length ) { const candidates = theories . filter ( ( tdesc ) => { return tdesc . position . line === desc . position . line + 1 ; } ) ; if ( candidates && candidates . length ) { const theoryName = candidates [ 0 ] . theoryName ; const fileName = fsUtils . getFileName ( fname ) ; const fileExtension = fsUtils . getFileExtension ( fname ) ; const contextFolder = fsUtils . getContextFolder ( fname ) ; if ( theoryName !== desc . newName ) { if ( ! range || range . start . character === range . end . character ) { character = ln . indexOf ( theoryName ) ; range = utils . getWordRange ( desc . txt , { line , character } ) ; } if ( range ) { const newTheoryName = desc . newName ; console . log ( `[rename-provider] Renaming theory ${ theoryName } to ${ newTheoryName }` ) ; const mod = ln . substring ( 0 , range . start . character ) + newTheoryName + ln . substring ( range . end . character ) ; const newLines = lines . slice ( 0 , desc . position . line ) . concat ( mod ) . concat ( lines . slice ( desc . position . line + 1 , lines . length + 1 ) ) ; const theoryEndRegexp = utils . endTheoryOrDatatypeRegexp ( theoryName ) ; const newContent = newLines . join ( "\n" ) . replace ( theoryEndRegexp , `$1${ newTheoryName }$3` ) ; await fsUtils . writeFile ( fname , newContent ) ; const textEdit = { range , newText : desc . newName } ; changes [ desc . uri ] = [ textEdit ] ; const newShasum = fsUtils . shasum ( newContent ) ; const theory = { fileName , fileExtension , contextFolder , theoryName } ; await fsUtils . renameTheoryInProofFile ( theory , { newTheoryName , newShasum } ) ; if ( theoryName === fileName && fileExtension === ".pvs" ) { const new_fname = fsUtils . desc2fname ( { fileName : newTheoryName , contextFolder , fileExtension : ".pvs" } ) ; const fileAlreadyExists = await fsUtils . fileExists ( new_fname ) ; if ( ! fileAlreadyExists ) { const success = await fsUtils . renameFile ( fname , new_fname ) ; if ( success && this . connection ) { const evt = { action : "did-rename-file" , old_fname : fname , new_fname } ; this . connection . sendNotification ( serverEvent . workspaceEvent , evt ) ; } } } return { changes } ; } } } } const theorems = await fsUtils . listTheoremsInFile ( fname , { content : desc . txt } ) ; if ( theorems && theorems . length ) { const candidates = theorems . filter ( ( fdesc ) => { return fdesc . position . line === desc . position . line + 1 ; } ) ; if ( candidates && candidates . length ) { const formulaName = candidates [ 0 ] . formulaName ; if ( formulaName !== desc . newName ) { if ( ! range || range . start . character === range . end . character ) { character = ln . indexOf ( formulaName ) ; range = utils . getWordRange ( desc . txt , { line , character } ) ; } if ( range ) { const newFormulaName = desc . newName ; console . log ( `[rename-provider] Renaming formula ${ formulaName } to ${ newFormulaName }` ) ; const mod = ln . substring ( 0 , range . start . character ) + newFormulaName + ln . substring ( range . end . character ) ; const newLines = lines . slice ( 0 , desc . position . line ) . concat ( mod ) . concat ( lines . slice ( desc . position . line + 1 , lines . length + 1 ) ) ; const newContent = newLines . join ( "\n" ) ; await fsUtils . writeFile ( fname , newContent ) ; const textEdit = { range , newText : desc . newName } ; changes [ desc . uri ] = [ textEdit ] ; const newShasum = fsUtils . shasum ( newContent ) ; const theoryName = fsUtils . findTheoryName ( desc . txt , line ) ; const formula = { fileName : fsUtils . getFileName ( fname ) , fileExtension : fsUtils . getFileExtension ( fname ) , contextFolder : fsUtils . getContextFolder ( fname ) , theoryName , formulaName } ; await fsUtils . renameFormulaInProofFile ( formula , { newFormulaName , newShasum } ) ; return { changes } ; } } } } } } return null ; } }