import { Message } from 'lean-client-js-node' ; import { CodeActionContext , CodeActionProvider , Command , commands , DiagnosticSeverity , Disposable , DocumentSelector , languages , Position , Range , Selection , TextDocument , TextEditor , Uri , window } from 'vscode' ; import { InfoProvider } from './infoview' ; import { Server } from './server' ; import { regexGM , magicWord , regexM } from './trythis' ; /** Pastes suggestions provided by tactics such as `squeeze_simp` */ export class TacticSuggestions implements Disposable , CodeActionProvider { private subscriptions : Disposable [ ] = [ ] ; constructor ( private server , infoView , private leanDocs ) { const commandHandler = async ( textEditor ) => { const msg = this . findSelectedMessage ( textEditor ) ; if ( msg === null ) return ; await this . pasteIntoEditor ( msg , textEditor , null ) ; } ; const infoViewCommandHandler = async ( m , suggestion ) => { const textEditor = this . findTextEditor ( m . file_name ) ; await this . pasteIntoEditor ( m , textEditor , suggestion ) ; await window . showTextDocument ( textEditor . document , { viewColumn : textEditor . viewColumn } ) ; } ; this . subscriptions . push ( commands . registerTextEditorCommand ( 'lean.pasteTacticSuggestion' , commandHandler ) , commands . registerCommand ( '_lean.pasteTacticSuggestion' , infoViewCommandHandler ) , languages . registerCodeActionsProvider ( this . leanDocs , this ) ) ; } dispose ( ) { for ( const s of this . subscriptions ) { s . dispose ( ) ; } } private findTextEditor ( fileName ) { for ( const textEditor of window . visibleTextEditors ) { if ( textEditor . document . uri . toString ( ) === Uri . file ( fileName ) . toString ( ) ) { return textEditor ; } } } private findSelectedMessage ( textEditor ) { const curFileName = textEditor . document . fileName ; const curPosition = textEditor . selection . active ; const messages = this . server . messages . filter ( ( m ) => m . file_name === curFileName && m . pos_line === curPosition . line + 1 && m . pos_col <= curPosition . character ) . sort ( ( a , b ) => b . pos_col - a . pos_col ) ; if ( messages . length === 0 ) return null ; return messages [ 0 ] ; } private async pasteIntoEditor ( m , textEditor , suggestion ) { if ( suggestion === null ) { const suggs = regexM . exec ( m . text ) ; if ( ! suggs ) return ; suggestion = suggs [ 1 ] ; } suggestion = suggestion . trim ( ) ; const startLine = m . pos_line - 1 ; let startCol = m . pos_col ; let openBrackets = 0 ; let endLine ; let endCol ; lineLoop : for ( endLine = startLine ; endLine < textEditor . document . lineCount ; endLine ++ ) { const chars = textEditor . document . lineAt ( endLine ) . text . split ( '' ) . entries ( ) ; for ( const [ col , char ] of chars ) { if ( endLine > startLine || col > startCol ) { if ( openBrackets === 0 && [ ',' , ';' ] . includes ( char ) ) { endCol = col ; break lineLoop ; } if ( [ '(' , '[' , '{' , '⟨' , '⦃' ] . includes ( char ) ) { openBrackets ++ ; } if ( [ '⦄' , '⟩' , '}' , ']' , ')' ] . includes ( char ) ) { if ( openBrackets === 0 ) { endCol = col ; break lineLoop ; } else { openBrackets -- ; } } } } if ( openBrackets === 0 ) { endCol = textEditor . document . lineAt ( endLine ) . range . end . character ; break lineLoop ; } } const lastPos = new Position ( endLine , endCol ) ; textEditor . selection = new Selection ( lastPos , lastPos ) ; if ( suggestion . startsWith ( 'exact ' ) ) { const pre = textEditor . document . lineAt ( startLine ) . text . substring ( 0 , startCol ) ; if ( pre . endsWith ( 'by ' ) ) { startCol = startCol - 3 ; suggestion = suggestion . substring ( 6 ) ; } else if ( pre . endsWith ( 'begin ' ) ) { const post = textEditor . document . lineAt ( endLine ) . text . substring ( endCol ) ; const matches = post . match ( /^,?\s*end/g ) ; if ( matches ) { startCol = startCol - 6 ; endCol = endCol + matches [ 0 ] . length ; suggestion = suggestion . substring ( 6 ) ; } } } const range = new Range ( new Position ( startLine , startCol ) , new Position ( endLine , endCol ) ) ; await textEditor . edit ( editBuilder => { editBuilder . replace ( range , suggestion ) ; } ) ; textEditor . selection = new Selection ( textEditor . selection . active , textEditor . selection . active ) ; } provideCodeActions ( document , range , context ) { const cmds = [ ] ; for ( const diag of context . diagnostics ) { if ( diag . severity !== DiagnosticSeverity . Information ) { continue ; } const msg = this . server . messages . find ( ( m ) => m . file_name === document . fileName && m . text === diag . message ) ; for ( const [ , tactic ] of diag . message . matchAll ( regexGM ) ) { cmds . push ( { title : tactic , command : '_lean.pasteTacticSuggestion' , arguments : [ msg , tactic ] } ) ; } } return cmds ; } }