import { ITheme , Terminal as XTerm } from 'xterm' ; import { CommandDescriptor , CommandsMap , MathObjects , HintsObject , Position } from './common/serverInterface' ; import * as colorUtils from './common/colorUtils' ; import { pvsColorTheme } from './common/languageKeywords' ; import { xTermDetectColorTheme , interruptCommand , SessionType , UpdateCommandHistoryData , XTermEvent } from './common/xtermInterface' ; import * as Backbone from 'backbone' ; import { checkPar , commentRegexp , evaluatorCommands , EVALUATOR_COMMANDS , PROOF_COMMANDS , PROOF_TACTICS , proverCommands , splitCommands , VSCODE_COMMANDS } from './common/languageUtils' ; import { htmlColorCode , XTermColorTheme } from './common/colorUtils' ; import { getMathSymbols } from './common/mathSymbols' ; interface KeyEvent { key : string ; domEvent : KeyboardEvent ; } ; interface MatchBrackets { pos1 ? : Position ; pos2 : Position ; } ; const MIN_POS = { line : 1 , character : 1 } ; enum ContentEvent { rebase = "rebase" , didAutocompleteContent = "didAutocompleteContent" } ; interface RebaseEvent { pos : Position ; } ; export function welcomeMessage ( session , integratedHelpSize ) { const msg = session === "prover" ? `
        - Please enter proof command at the prover prompt
        - Double click expands definitions${ integratedHelpSize > 2 ? "\n- " : ". " }Copy / Paste text with ${ isLinux ( ) ? "Ctrl+" : "Command+" }C / ${ isLinux ( ) ? "Ctrl+" : "Command+" }V
        ` : `
        - Please enter a PVS expression followed by ';'
        - or a Lisp expression followed by '!'
        ` ; return msg . trim ( ) . replace ( /\n/g , "<br>" ) ; } const MIN_VIEWPORT_COLS = 128 ; const MIN_VIEWPORT_ROWS = 8 ; /**
 * Utility function, detects the operating system
 */ export function getOs ( ) { const version = navigator ?. appVersion ; if ( version ?. includes ( " Win " ) ) { return "Windows" ; } if ( version ?. includes ( " Mac " ) ) { return "MacOSX" ; } if ( version ?. includes ( " X11 " ) || version . includes ( " Linux " ) ) { return "Linux" ; } ; return version || "" ; } /**
 * Utility function, returns true if the OS is Linux
 */ function isLinux ( ) { return getOs ( ) === "Linux" ; } /**
 * Utility class, wraps the content of a line
 */ class LineWrapper { static maxCols : number = MIN_VIEWPORT_COLS ; /**
     * Utility function, wraps lines by introducing additional \n if the line exceeds a target length
     */ static wrapLines ( data ) { const lines = data ?. split ( "\n" ) ; let ans = [ ] ; for ( let i = 0 ; i < lines . length ; i ++ ) { const line = lines [ i ] ; if ( colorUtils . getPlainText ( line ) . length < LineWrapper . maxCols ) { ans . push ( line ) ; } else { const sublines = LineWrapper . splitBreakable ( line , { maxLen : MIN_VIEWPORT_COLS } ) ; let ln = "" ; for ( let i = 0 ; i < sublines . length ; i ++ ) { const subln = sublines [ i ] ; const subln_length = colorUtils . getPlainText ( subln ) . length ; const ln_length = colorUtils . getPlainText ( ln ) . length ; if ( ln_length > 0 && ( ln_length + subln_length >= LineWrapper . maxCols ) ) { ans . push ( ln ) ; ln = subln ; } else { ln += sublines [ i ] ; } } if ( ln . length > 0 ) { ans . push ( ln ) ; } } } return ans . join ( "\n" ) ; } /**
     * Utility function, breaks a string into an array of sub-strings at breakable points
     */ static splitBreakable ( str , opt ? ) { opt = opt || { } ; let ans = [ ] ; if ( str ) { const breakablePoints = new RegExp ( /[\)\]\;\,\.\` ]/g ) ; let match = breakablePoints . exec ( str ) ; let prevIndex = 0 ; const tmp = [ ] ; while ( match ) { tmp . push ( str . slice ( prevIndex , match . index ) ) ; prevIndex = match . index ; match = breakablePoints . exec ( str ) ; } tmp . push ( str . slice ( prevIndex ) ) ; if ( opt . maxLen ) { for ( let i = 0 ; i < tmp . length ; i ++ ) { for ( let l = 0 ; l < tmp [ i ] . length ; l += opt . maxLen ) { const frag = tmp [ i ] . slice ( l , l + opt . maxLen ) ; ans . push ( frag ) ; } } } else { ans = tmp ; } } return ans ; } } /**
 * Virtual content of the terminal, keeps track of the content of the cursor position
 */ export class Content extends Backbone . Model { protected lines : string [ ] = [ ] ; protected pos : Position = { ... MIN_POS } ; protected prevPos : Position = { ... MIN_POS } ; protected base : Position = { ... MIN_POS } ; /**
     * Constructor
     */ constructor ( ) { super ( ) ; console . log ( "[xterm-content] Init complete" , { pos : this . pos , prevPos : this . prevPos , lines : this . lines } ) ; } /**
     * Internal function, updates previous cursor position
     */ protected savePos ( ) { this . prevPos = { character : this . pos . character , line : this . pos . line } ; } /**
     * Clears the content and moves the cursor to its initial position (top-left corner)
     */ deleteContent ( ) { this . pos = { ... MIN_POS } ; this . prevPos = { ... MIN_POS } ; this . base = { ... MIN_POS } ; this . lines = [ ] ; } /**
     * get current cursor position, one-based cols and lines
     */ cursorPosition ( ) { return { character : this . pos . character , line : this . pos . line } ; } /**
     * Gets the base (home) position of the cursor in the command line
     */ getHomePosition ( ) { return { character : this . base . character , line : this . base . line } ; } /**
     * Utility function, returns true if the cursor is located at the home position, i.e., at the base position
     */ cursorIsAtHomePosition ( ) { return this . pos . line === this . base . line && this . pos . character === this . base . character ; } /**
     * get previous cursor position, one-based cols and lines
     */ previousCursorPosition ( ) { return { character : this . prevPos . character , line : this . prevPos . line } ; } /**
     * Returns the entire content
     */ text ( ) { return this . lines . join ( "\n" ) ; } /**
     * Returns the command entered at the input line (i.e., everything after the base index)
     */ command ( opt ? ) { opt = opt || { } ; return opt . beforeCursor ? this . textBetween ( this . base , this . pos ) : this . textAfter ( this . base ) ; } /**
     * Replaces the content of the command line with the provided command
     */ setCommand ( cmd , opt ? ) { this . clearCommandLine ( ) ; const wrapped = LineWrapper . wrapLines ( cmd ) ; this . writeData ( wrapped ) ; if ( opt ?. cursorToHome ) { this . cursorTo ( this . base ) ; } this . trigger ( ContentEvent . didAutocompleteContent ) ; } /**
     * get line text at given position (position is 1-based)
     */ textLineAt ( pos ) { const lineIndex = typeof pos === "number" ? ( pos - 1 ) : ( pos ?. line - 1 ) ; if ( lineIndex >= 0 && lineIndex < this . lines . length ) { const textLine = this . lines [ lineIndex ] ; return textLine ; } return "" ; } /**
     * Returns the line of text after the cursor, including the character at the cursor position
     */ textLineAfter ( pos ) { const colIndex = pos ?. character - 1 ; const textLine = this . textLineAt ( pos ) ; if ( colIndex >= 0 && colIndex < textLine . length ) { const textLineAfter = textLine . substr ( colIndex ) ; return textLineAfter ; } return "" ; } /**
     * Returns the line of text before the cursor
     * from the start of the line (which could be behind base)
     * **excluding** the character at the cursor position
     */ textLineBefore ( pos ) { const colIndex = pos ?. character - 1 ; const textLine = this . textLineAt ( pos ) ; if ( colIndex >= 0 ) { return textLine . substr ( 0 , colIndex ) ; } console . warn ( "[xterm-content] Warning, textLineBefore position column out of range" , { pos , textLine , lines : this . lines , colIndex } ) ; return "" ; } /**
     * Returns the lines below the cursor, **excluding** the character at the cursor position
     */ linesBelow ( pos ) { const lineIndex = pos ?. line - 1 ; if ( lineIndex >= 0 ) { return this . lines . slice ( lineIndex + 1 ) ; } return [ ] ; } /**
     * Returns the lines of text before the cursor, **excluding** the line of the cursor
     */ linesAbove ( pos ) { const lineIndex = pos ?. line - 1 ; if ( lineIndex >= 0 ) { return this . lines . slice ( 0 , lineIndex ) ; } return [ ] ; } /**
     * Returns the lines below the cursor, **excluding** first and last lines
     */ linesBetween ( pos1 , pos2 ) { const lineIndex1 = pos1 ?. line ; const lineIndex2 = pos2 ?. line - 1 ; if ( lineIndex1 >= 0 && lineIndex2 >= 0 && lineIndex2 >= lineIndex1 ) { return this . lines . slice ( lineIndex1 , lineIndex2 ) ; } return [ ] ; } /**
     * Returns text between positions pos1 pos2. Character at pos1 is included. Character at pos2 is excluded
     */ textBetween ( pos1 , pos2 ) { if ( pos1 && pos2 ) { const line1 = this . textLineAfter ( pos1 ) ; if ( pos1 . line === pos2 . line && pos2 . character >= pos1 . character ) { return line1 . substring ( 0 , pos2 . character - pos1 . character ) ; } if ( pos2 . line > pos1 . line ) { const line2 = this . textLineBefore ( pos2 ) ; const linesBetween = this . linesBetween ( pos1 , pos2 ) ; return line1 + "\n" + ( linesBetween . length ? linesBetween . join ( "\n" ) + "\n" : "" ) + line2 ; } } return "" ; } /**
     * Returns the entire text after the cursor
     * **including** the character at the cursor position
     */ textAfter ( pos ) { const currLine = this . textLineAfter ( pos ) ; const linesAfter = [ currLine ] . concat ( this . linesBelow ( pos ) ) ; return linesAfter . join ( "\n" ) ; } /**
     * Returns the entire text before the cursor
     * from the start of the line (which could be behind base)
     * and **excluding** the character at the cursor position
     */ textBefore ( pos ) { const currLine = this . textLineBefore ( pos ) ; const linesBefore = this . linesAbove ( pos ) . concat ( [ currLine ] ) ; return linesBefore . join ( "\n" ) ; } /**
     * Rebase the index, useful to make the text before the cursor read-only
     */ rebase ( opt ? ) { if ( opt ?. prompt ) { if ( this . lines . length ) { this . lines = [ opt . prompt ] ; this . pos = { line : 1 , character : this . lines [ 0 ] . length + 1 } ; this . prevPos = { line : 1 , character : this . lines [ 0 ] . length + 1 } ; } } this . base = { line : this . pos . line , character : this . pos . character } ; const evt = { pos : this . pos } ; this . trigger ( ContentEvent . rebase , evt ) ; } /**
     * Trim content, to discard old lines that are not needed anymore
     */ trimLines ( n ) { if ( n > 0 ) { this . lines = this . lines . slice ( n ) ; this . base . line = this . base . line > n ? this . base . line - n : 0 ; this . prevPos . line = this . prevPos . line ? this . prevPos . line - n : 0 ; this . pos . line = this . pos . line > n ? this . pos . line - n : 0 ; } } /**
     * writes text at the cursor position
     */ writeData ( data ) { if ( data ) { const plainText = colorUtils . getPlainText ( data ) ; const newText = plainText . replace ( /\r?\n/g , "\n" ) . replace ( /\r\n?/g , "\n" ) ; const textBeforeCursor = this . textBefore ( this . pos ) + newText ; const textAfterCursor = this . textAfter ( this . pos ) ; this . lines = ( textBeforeCursor + textAfterCursor ) . split ( "\n" ) ; this . savePos ( ) ; this . pos . line = textBeforeCursor . split ( "\n" ) . length || MIN_POS . line ; this . pos . character = this . endCol ( this . pos . line ) + 1 ; } } /**
     * autocompletes the current input with the provided substitution
     */ autocomplete ( data ) { if ( data && data . substitution ) { const textBeforeCursor = this . textBefore ( this . pos ) ; const completedText = textBeforeCursor . substring ( 0 , textBeforeCursor . length - data . match ?. length ) + data . substitution ; let textAfterCursor = this . textAfter ( this . pos ) ; if ( textAfterCursor ?. length && ! /[\s\(\)\[\]\"]/g . test ( textAfterCursor [ 0 ] ) ) { let termEndIndex = 0 ; for ( let i = 0 ; i < textAfterCursor . length && ! /[\s\(\)\[\]]/g . test ( textAfterCursor [ i ] ) ; i ++ ) { termEndIndex = i ; } textAfterCursor = textAfterCursor . slice ( termEndIndex + 1 ) ; } const completedTextWrapped = LineWrapper . wrapLines ( completedText ) ; const wrapped = completedTextWrapped ?. split ( "\n" ) ?. length > 1 ? completedTextWrapped : LineWrapper . wrapLines ( completedText + textAfterCursor ) ; this . lines = ( wrapped ) . split ( "\n" ) ; this . savePos ( ) ; this . pos . line = completedTextWrapped . split ( "\n" ) . length || MIN_POS . line ; this . pos . character = completedTextWrapped . split ( "\n" ) [ this . pos . line - 1 ] . length + 1 ; this . trigger ( ContentEvent . didAutocompleteContent ) ; } } /**
     * Returns the text at the cursor position
     */ charAtCursorPosition ( ) { return this . charAt ( this . pos ) ; } /**
     * Returns the text at the given position
     */ charAt ( pos ) { const lineIndex = pos ?. line - 1 ; if ( lineIndex >= 0 && lineIndex < this . lines . length ) { const selectedLine = this . lines [ lineIndex ] ; const colIndex = pos ?. character - 1 ; if ( colIndex >= 0 && colIndex < selectedLine . length ) { return selectedLine [ colIndex ] ; } } return "" ; } /**
     * Deletes the character at the given position
     */ deleteCharAt ( pos ) { const lineIndex = pos ?. line - 1 ; if ( lineIndex >= 0 && lineIndex < this . lines . length ) { const selectedLine = this . lines [ lineIndex ] ; const colIndex = pos ?. character - 1 ; if ( colIndex >= 0 && colIndex < selectedLine . length ) { const deleted = selectedLine [ colIndex ] ; const textLine = selectedLine . substring ( 0 , colIndex ) + selectedLine . substr ( colIndex + 1 ) ; this . lines [ lineIndex ] = textLine ; return deleted ; } } return "" ; } /**
     * Inserts the character at the given position and moves the cursor after the inserted character
     */ insertCharAt ( pos , char ) { const lineIndex = pos ?. line - 1 ; if ( lineIndex === 0 && this . lines . length === 0 ) { this . lines = [ "" ] ; } if ( lineIndex >= 0 && lineIndex < this . lines . length ) { const colIndex = pos ?. character - 1 ; if ( colIndex >= 0 ) { const textLineBefore = this . textLineBefore ( pos ) ; const textLineAfter = this . textLineAfter ( pos ) ; const textLine = textLineBefore + char + textLineAfter ; this . lines [ lineIndex ] = textLine ; this . savePos ( ) ; this . pos . character ++ ; return true ; } } console . warn ( "[xterm-content] Warning: line out of range @insertCharAt" , { lineIndex , pos , char , lines : this . lines } ) ; return false ; } /**
     * Deletes the current content of the command line
     */ clearCommandLine ( ) { const prompt = this . textLineBefore ( this . base ) ; this . lines = [ prompt ] ; this . pos = { line : 1 , character : this . lines [ 0 ] . length + 1 } ; this . prevPos = { line : 1 , character : this . lines [ 0 ] . length + 1 } ; } /**
     * Cursor right. Returns true if the cursor could be moved, based on the current content and base marker.
     */ onArrowRight ( ) { const currentLine = this . textLineAt ( this . pos ) ; if ( this . pos . character <= currentLine . length ) { this . savePos ( ) ; this . pos . character ++ ; return true ; } if ( this . pos . line < this . endLine ( ) ) { this . savePos ( ) ; this . pos . line ++ ; this . pos . character = this . startCol ( this . pos . line ) ; return true ; } return false ; } /**
     * Internal function, returns the start column number for a given line
     */ protected startCol ( line ) { return ( line === this . base . line ) ? this . base . character : MIN_POS . character ; } /**
     * Internal function, returns the end column number for a given line
     */ protected endCol ( line , opt ? ) { opt = opt || { } ; const lineIndex = line - 1 ; if ( lineIndex < this . lines . length ) { let col = this . lines [ lineIndex ] . length ; if ( col && opt . allowBesideEnd ) { col ++ ; } if ( col < MIN_POS . character ) { col = MIN_POS . character ; } if ( line === this . base . line && col < this . base . character ) { col = this . base . character ; } return col ; } console . warn ( "[xterm-content] Warning: line index out of bounds @endCol" , { line , lineIndex } ) ; return opt . allowBesideEnd ? MIN_POS . character + 1 : MIN_POS . character ; } /**
     * Returns max line number
     */ startLine ( ) { return this . base . line ; } /**
     * Returns max line number
     */ endLine ( ) { return this . lines . length ; } /**
     * Cursor left. Returns true if the cursor could be moved, based on the current content.
     */ onArrowLeft ( ) { this . savePos ( ) ; const minCol = this . startCol ( this . pos . line ) ; if ( this . pos . character > minCol ) { this . pos . character -- ; return true ; } if ( this . pos . line > this . base . line ) { this . pos . line -- ; this . pos . character = this . endCol ( this . pos . line , { allowBesideEnd : true } ) ; return true ; } return false ; } /**
     * Cursor up. Returns true if the cursor could be moved, based on the current content.
     */ onArrowUp ( ) { if ( this . pos . line > this . base . line ) { this . savePos ( ) ; this . pos . line = this . pos . line - 1 ; const maxCol = this . endCol ( this . pos . line , { allowBesideEnd : true } ) ; const minCol = this . startCol ( this . pos . line ) ; this . pos . character = this . pos . character > maxCol ? maxCol : this . pos . character < minCol ? minCol : this . pos . character ; return true ; } return false ; } /**
     * Cursor down. Returns true if the cursor could be moved, based on the current content.
     */ onArrowDown ( ) { if ( this . pos . line < this . lines . length ) { this . savePos ( ) ; this . pos . line ++ ; const maxCol = this . endCol ( this . pos . line , { allowBesideEnd : true } ) ; const minCol = this . startCol ( this . pos . line ) ; this . pos . character = this . pos . character > maxCol ? maxCol : this . pos . character < minCol ? minCol : this . pos . character ; return true ; } return false ; } /**
     * Backspace. Returns true if the cursor could be moved, based on the current content.
     */ onBackspace ( ) { const success = this . onArrowLeft ( ) ; if ( success ) { this . onDelete ( ) ; return true ; } return false ; } /**
     * Delete. Returns true if the cursor could be moved, based on the current content.
     */ onDelete ( ) { const lineIndex = this . pos . line - 1 ; if ( lineIndex >= 0 && lineIndex < this . lines . length ) { if ( this . lines [ lineIndex ] . length === 0 ) { this . lines = this . lines . slice ( 0 , lineIndex ) . concat ( this . lines . slice ( lineIndex + 1 ) ) ; return true ; } if ( this . pos . character === this . lines [ lineIndex ] . length + 1 && ( lineIndex + 1 ) < this . lines . length ) { const merge = this . lines [ lineIndex ] + this . lines [ lineIndex + 1 ] ; this . lines = this . lines . slice ( 0 , lineIndex ) . concat ( this . lines . slice ( lineIndex + 1 ) ) ; this . lines [ lineIndex ] = merge ; return true ; } const deleted = this . deleteCharAt ( this . pos ) ; return true ; } return false ; } /**
     * Enter key.
     */ onEnter ( ) { const textBefore = this . textBefore ( this . pos ) ; const textAfter = this . textAfter ( this . pos ) ; const newLines = textBefore + "\n" + textAfter ; this . lines = newLines . split ( "\n" ) ; this . savePos ( ) ; this . pos . line = this . pos . line + 1 ; this . pos . character = this . startCol ( this . pos . line ) ; return true ; } /**
     * Generic handler for printable characters: inserts character at position index
     */ onChar ( c ) { if ( c . length > 1 ) { return false ; } return this . insertCharAt ( this . pos , c ) ; } /**
     * Moves the cursor to a given position
     */ cursorTo ( pos ) { const line = pos ?. line < this . base . line ? this . base . line : pos ?. line > this . lines . length ? this . lines . length : pos . line ; const maxCol = this . endCol ( line , { allowBesideEnd : true } ) ; const minCol = this . startCol ( line ) ; const character = pos ?. character < minCol ? minCol : pos ?. character > maxCol ? maxCol : pos . character ; if ( line !== this . pos . line || character !== this . pos . character ) { this . savePos ( ) ; this . pos = { line , character } ; return true ; } return false ; } /**
     * Cursor moves to the command line home position, i.e., after the command prompt.
     */ cursorToHome ( ) { if ( this . pos . line !== this . base . line || this . pos . character !== this . base . character ) { this . savePos ( ) ; const line = this . base . line ; const character = this . base . character ; return this . cursorTo ( { line , character } ) ; } return false ; } /**
     * Cursor moves to the end of the current input.
     */ cursorToEnd ( ) { const textAfter = this . textAfter ( this . pos ) ; if ( textAfter . length ) { this . savePos ( ) ; const line = this . endLine ( ) ; const character = this . endCol ( this . pos . line , { allowBesideEnd : true } ) ; return this . cursorTo ( { line , character } ) ; } return false ; } /**
     * Cursor moves to the beginning of the previous word in the command line input.
     */ cursorToPreviousWord ( ) { const textBefore = this . textBefore ( this . pos ) ; if ( textBefore . length ) { const blankPos = textBefore . trim ( ) . lastIndexOf ( " " ) + 1 ; if ( blankPos <= 0 ) { this . savePos ( ) ; return this . cursorToHome ( ) ; } const frag = textBefore . substring ( 0 , blankPos ) ; if ( frag ) { this . savePos ( ) ; const fragLines = frag . split ( "\n" ) ; const line = fragLines . length ; const character = fragLines [ line - 1 ] . length + 1 ; this . cursorTo ( { line , character } ) ; return true ; } } return false ; } /**
     * Cursor moves to the end of the nearest word in the command line input.
     */ cursorToNextWord ( ) { const textAfter = this . textAfter ( this . pos ) ; if ( textAfter . length ) { const leadingBlanks = textAfter . length - textAfter . trimLeft ( ) . length ; const blankPos = textAfter . trimLeft ( ) . indexOf ( " " ) ; if ( blankPos < 0 ) { this . savePos ( ) ; return this . cursorToEnd ( ) ; } const frag = this . textBefore ( this . pos ) + textAfter . substring ( 0 , blankPos + leadingBlanks ) ; if ( frag ) { this . savePos ( ) ; const fragLines = frag . split ( "\n" ) ; const line = fragLines . length ; const character = fragLines [ line - 1 ] . length + 1 ; this . cursorTo ( { line , character } ) ; return true ; } } return false ; } /**
     * Updates the content of the terminal based on key press events
     */ updateContent ( e ) { const ev = e . domEvent ; const key = e . key ; let keypressRegistered = false ; switch ( ev . key ) { case "Enter" : { keypressRegistered = this . onEnter ( ) ; break ; } case "Backspace" : { keypressRegistered = this . onBackspace ( ) ; break ; } case "Delete" : { keypressRegistered = this . onDelete ( ) ; break ; } case "Escape" : { keypressRegistered = true ; break ; } case "Tab" : { break ; } case "ArrowUp" : { keypressRegistered = this . onArrowUp ( ) ; break ; } case "ArrowDown" : { keypressRegistered = this . onArrowDown ( ) ; break ; } case "ArrowLeft" : { keypressRegistered = this . onArrowLeft ( ) ; break ; } case "ArrowRight" : { keypressRegistered = this . onArrowRight ( ) ; break ; } default : { keypressRegistered = this . onChar ( key ) ; break ; } } return keypressRegistered ; } /**
     * Match brackets
     */ matchBrackets ( bracket ? ) { const b1 = bracket || "(" ; const b2 = getB2 ( b1 ) ; const inputBeforeCursor = this . command ( { beforeCursor : true } ) ; if ( inputBeforeCursor ?. endsWith ( b2 ) ) { const pos2 = { character : this . pos . character - 1 , line : this . pos . line } ; const idx1 = this . findMatchingOpenBracketIndex ( inputBeforeCursor ) ; if ( idx1 >= 0 ) { const textBeforeIdx1 = inputBeforeCursor . substring ( 0 , idx1 ) ; const lineIndex = textBeforeIdx1 . split ( "\n" ) . length - 1 ; const padding = lineIndex > 0 ? textBeforeIdx1 . lastIndexOf ( "\n" ) : 0 ; const character = lineIndex === 0 ? idx1 + this . base . character : idx1 - padding ; const line = this . base . line + lineIndex ; const ans = { pos1 : { character , line } , pos2 } ; return ans ; } return { pos2 } ; } return null ; } /**
     * Internal function, finds matching bracket
     */ protected findMatchingOpenBracketIndex ( text ) { let par = 0 ; let quotes = 0 ; for ( let i = 0 ; i < text . length ; i ++ ) { const pos = text . length - 1 - i ; switch ( text [ pos ] ) { case "(" : { if ( quotes % 2 === 0 ) { par ++ ; } if ( par === 0 ) { return pos ; } break ; } case ")" : { if ( quotes % 2 === 0 ) { par -- ; } break ; } case '"' : { quotes ++ ; break ; } default : { break ; } } } return - 1 ; } } export type ModKeys = { alt : boolean ; ctrl : boolean ; meta : boolean ; } ; export type Bracket = "(" | ")" | "[" | "]" | "{" | "}" ; /**
 * Utility function, returns the character for the second bracket, based on the first bracket
 */ function getB2 ( b1 ) { return b1 === "(" ? ")" : b1 === "[" ? "]" : "}" ; } ; const tooltipTemplate = `<div>
{{#each hints}}
<div class="autocompletion-item p-0 m-0 {{#if @first}}selected highlighted{{/if}} index-{{@index}}">{{this}}</div>
{{/each}}
</div>` ; const tooltipStyle = `<style>
.tooltip.show {
    opacity:0.9 !important;
    left:10px !important;
}
.tooltip-inner {
    max-height: 20px; 
    max-width: 300px;
    font-size:12px;
    font-family:Menlo, Monaco, monospace;
    text-align:left;
    cursor:default;
    border: 1px solid;
    white-space: nowrap;
    padding-top: 0 !important;
    padding-bottom: 0 !important;
    overflow: overlay !important;
}
.tooltip-inner::-webkit-scrollbar {
    height: 1px;
    width: 2px;
}
.arrow::before {
    border-bottom-color: white !important;
    border-top-color: white !important;
    display: none !important;
}
.tooltip-arrow {
    display: none !important;
}
.selected {
    background: #004775 !important;
    color: white !important;
}
.highlighted {
    background: #292d2e;
    color: white;
}
.btn-help {
    font-size:11px;
}
</style>` ; const cursorStyle = `<style>
@keyframes pulser {
    0% { opacity: 1; }
    70% { opacity: 0.6; }
}
.xterm-cursor-layer {
    animation: pulser 2s linear infinite !important;
}
</style>` ; const terminalStyle = `<style>
.terminal-help {
    width:100%;
    background:transparent;
    white-space:nowrap;
    font-size:11px;
    font-family:Menlo, Monaco, monospace;
    text-align:left;
    margin-top:10px;
    padding-top:4px !important;
    border-top:1px solid gray;
    overflow-y:auto;
    overflow: overlay;
}
.terminal-help::-webkit-scrollbar {
    height: 6px;
}
body::-webkit-scrollbar {
    height: 6px;
}
body {
    overflow: overlay;
}
</style>` ; const terminalHelpTemplate = `
{{#if description}}
<style>
.terminal-help .cmd {
    color: #00b0ff;
}
.terminal-help .key {
    color: gold;
}
.hidden {
    color:transparent;
    user-select: none;
}
</style>
<div class="syntax">Syntax: {{syntax}}</div>
<div class="description">Description: {{description}}</div>
{{#each optionals}}
{{#if @first}}<div><span class="optionals">Optionals: </span><span class="key">{{@key}}</span> {{this}}</div>
{{else}}<div><span class="optionals hidden">Optionals: </span><span class="key">{{@key}}</span> {{this}}</div>{{/if}}
{{/each}}
{{#if note}}
<div class="optionals">Note: {{note}}</div>
{{/if}}
{{#if footnote}}
<div class="optionals">{{footnote}}</div>
{{/if}}
{{/if}}
` ; export interface AutocompleteData { substitution : string ; match : string ; } export enum AutocompleteEvent { didAutocomplete = "didAutocomplete" } ; export interface DidAutocompleteEvent extends AutocompleteData { currentInput : string ; } ; /**
 * Utility class for command line history
 */ export class History { protected sessionType : SessionType ; protected history : string [ ] = [ ] ; protected current : string = "" ; protected index : number = - 1 ; protected successHistory : string [ ] = [ ] ; /**
     * Constructor
     */ constructor ( sessionType ) { this . sessionType = sessionType ; } /**
     * Utility function, pushes the given command to the history, if the command is not present alreayd.
     * Additionally, the function clears the current command and resets the index
     */ push ( cmd , opt ? ) { if ( cmd ) { opt = opt || { } ; let elem = cmd . trim ( ) . replace ( commentRegexp , "" ) . replace ( /\n/g , " " ) . replace ( /\s\s+/g , " " ) ; if ( this . sessionType === "prover" && elem . startsWith ( "(" ) && elem . endsWith ( ")" ) ) { elem = elem . substring ( 1 , elem . length - 1 ) . trim ( ) ; } this . history = [ elem ] . concat ( this . history ) ; if ( opt . successHistory && ! this . successHistory . includes ( elem ) ) { this . successHistory = [ elem ] . concat ( this . successHistory ) ; } this . current = "" ; this . index = - 1 ; } } /**
     * Utility function, returns the size of the history
     */ size ( ) { return this . history . length ; } /**
     * clear the entire history and the current command
     */ clear ( ) { this . history = [ ] ; this . current = "" ; this . index = - 1 ; } /**
     * Updates the current command with the provided input
     */ updateCurrentCommand ( cmd ) { this . current = cmd ; } /**
     * Returns the previous command in the history
     */ prev ( ) { if ( this . history . length ) { this . index = ( this . index + 1 < this . history . length ) ? this . index + 1 : this . index ; return this . sessionType === "prover" ? `(${ this . history [ this . index ] })` : this . history [ this . index ] ; } return this . current ; } /**
     * Returns the next command in the history
     */ next ( ) { if ( this . index - 1 >= 0 && this . history . length ) { this . index -- ; return this . sessionType === "prover" ? `(${ this . history [ this . index ] })` : this . history [ this . index ] ; } this . index = - 1 ; return this . current ; } /**
     * Returns the history of commands
     */ getHistory ( opt ? ) { opt = opt || { } ; if ( opt . match !== undefined ) { return opt . match ? this . history . filter ( ( c ) => { return c . startsWith ( opt . match ) ; } ) : [ ] ; } return this . history ; } /**
     * Returns the history of commands successfully executed by the prover
     */ getSuccessHistory ( opt ? ) { opt = opt || { } ; if ( opt . match !== undefined ) { return opt . match ? this . successHistory . filter ( ( c ) => { return c . startsWith ( opt . match ) ; } ) : [ ] ; } return this . history ; } } /**
 * Utility function, returns a pointer to the cursor rendered in the terminal
 */ function getXtermCursor ( ) { return $ ( ".xterm-helper-textarea" ) ; } /**
 * Utility class for autocomplete
 */ export class Autocomplete extends Backbone . Model { protected content : Content ; protected sessionType : SessionType ; protected integratedHelpSize : number = 2 ; protected hintsObject : HintsObject = { } ; protected mathObjects : MathObjects = { } ; protected currentHints : string [ ] = [ ] ; protected mathSymbols : string [ ] = getMathSymbols ( ) ; protected frequentCommands : string [ ] = [ ] ; protected triggerMode : "standard" | "single-click" = "standard" ; protected currHelp : string = "" ; history : History ; /**
     * Constructor
     */ constructor ( content , sessionType , opt ? ) { super ( ) ; this . content = content ; this . sessionType = sessionType ; this . history = new History ( this . sessionType ) ; this . integratedHelpSize = opt ?. integratedHelpSize || 2 ; this . frequentCommands = opt ?. frequentCommands ?. split ( "," ) ?. map ( cmd => { return cmd . trim ( ) ; } ) . filter ( cmd => { return cmd ?. length ; } ) || [ ] ; console . log ( "[xterm-autocomplete] Frequent commands" , this . frequentCommands ) ; this . installHandlers ( ) ; } /**
     * Internal function, install relevant handlers for key presses
     */ protected installHandlers ( ) { $ ( document ) . on ( "keydown" , ( evt ) => { switch ( evt . key ) { case "ArrowUp" : case "ArrowDown" : evt . preventDefault ( ) ; case "ArrowLeft" : case "ArrowRight" : case "Enter" : case "Escape" : { this . autocompleteOnKeyPress ( evt ) ; break ; } default : { break ; } } } ) ; } /**
     * Returns math symbols used for autocomplete
     */ getMathSymbols ( ) { return this . mathSymbols ; } /**
     * Updates hints data for autocompletion
     */ updateHints ( hints ) { this . hintsObject = hints ; } /**
     * Updates mathObjects for autocompletion
     */ updateMathObjects ( mathObjects ) { this . mathObjects = mathObjects ; } /**
     * Utility function, returns true if the tooltip is visible
     */ tooltipVisible ( ) { return ! ( $ ( ".tooltip" ) [ 0 ] === null || $ ( ".tooltip" ) [ 0 ] === undefined ) ; } /**
     * Shows a tooltip with the provided hints
     */ showTooltip ( hints , opt ? ) { if ( ! this . sameHints ( hints , this . currentHints ) ) { this . deleteTooltips ( ) ; this . currentHints = hints || [ ] ; } this . renderTooltip ( this . currentHints , opt ) ; } /**
     * Updates the command history with the provided command, if the command is not one of the hints already known to autocomplete and history
     */ updateCommandHistory ( cmd , opt ? ) { if ( cmd ) { const cmdArray = this . sessionType === "prover" ? splitCommands ( cmd ) : [ cmd ] ; if ( cmdArray ?. length ) { for ( let i = 0 ; i < cmdArray . length ; i ++ ) { let elem = cmdArray [ i ] . trim ( ) ; if ( elem . startsWith ( "(" ) && elem . endsWith ( ")" ) ) { elem = elem . substring ( 1 , elem . length - 1 ) . trim ( ) ; } this . history . push ( elem , opt ) ; } } } } /**
     * Removes all tooltips
     */ deleteTooltips ( ) { $ ( ".xterm-helper-textarea" ) ?. tooltip ( 'dispose' ) ; } /**
     * Returns the input string used to compute autocompletion
     */ getCurrentInput ( opt ? ) { opt = opt || { } ; const currentInput = this . content ?. command ( { beforeCursor : true } ) ; if ( opt . regex && currentInput ) { const match = new RegExp ( opt . regex ) . exec ( currentInput ) ; if ( match && match . length && match [ 0 ] ) { return match [ 0 ] ; } return "" ; } if ( opt . removeLeadingBracket ) { const bless = currentInput . startsWith ( "(" ) ? currentInput . substring ( 1 ) : currentInput ; return bless ; } return currentInput ; } /**
     * Utility function, checks if a given symbol is known to the prover
     */ validSymbol ( sym ) { const symbols = this . hintsObject ?. symbols ; return symbols ?. includes ( sym ) ; } /**
     * Internal function, checks if the provided hints are identical
     */ protected sameHints ( t1 , t2 ) { if ( t1 ?. length === t2 ?. length ) { for ( let i = 0 ; i < t1 ?. length ; i ++ ) { if ( t1 [ i ] !== t2 [ i ] ) { return false ; } } return true ; } return false ; } /**
     * Internal function, shows tooltip at the cursor position
     */ protected renderTooltip ( hints , opt ? ) { if ( hints ?. length ) { opt = opt || { } ; const tooltip = Handlebars . compile ( tooltipTemplate , { noEscape : true } ) ( { hints } ) ; const cursor = getXtermCursor ( ) ; cursor . attr ( "data-toggle" , "tooltip" ) ; cursor . tooltip ( { trigger : "manual hover click" , title : tooltip , placement : "bottom-end" , html : true , boundary : "viewport" , rootBoundary : "document" , container : "body" , fallbackPlacements : [ 'right-end' , 'top-end' , 'bottom-end' ] , popperConfig : { placement : "bottom-end" } } ) . tooltip ( 'show' ) ; if ( this . sessionType === "prover" && opt . top !== undefined && opt . left !== undefined && $ ( ".tooltip-inner" ) [ 0 ] ) { const top = cursor . css ( "top" ) ; const left = cursor . css ( "left" ) ; const height = $ ( ".tooltip" ) . css ( "height" ) ; $ ( ".tooltip-inner" ) . css ( { "margin-left" : `${ opt . left - parseFloat ( left ) }px` , "margin-top" : `${ opt . top - parseFloat ( top ) - parseFloat ( height ) }px` } ) ; this . updateHelp ( { cmd : "expand" } ) ; this . triggerMode = "single-click" ; } else { this . triggerMode = "standard" ; } $ ( ".autocompletion-item" ) . on ( "mouseover" , ( evt ) => { const index = this . getIndex ( evt . target ) ; this . highlight ( index ) ; } ) . on ( "click" , ( evt ) => { const index = this . getIndex ( evt . target ) ; this . select ( index ) ; if ( this . triggerMode === "single-click" ) { this . triggerAutocomplete ( ) ; this . triggerMode = "standard" ; } } ) . on ( "dblclick" , ( evt ) => { const index = this . getIndex ( evt . target ) ; this . select ( index ) ; this . triggerAutocomplete ( ) ; } ) ; } else { this . deleteTooltips ( ) ; } } /**
     * Internal function, checks if a math symbol can be matched on the provided input string
     */ protected matchSymCode ( input ) { const info = input . includes ( "\\" ) ? input ?. split ( "\\" ) ?. slice ( - 1 ) : null ; return info ?. length ? { symbol : info [ 1 ] , code : "\\" + info [ 0 ] } : null ; } /**
     * Autocompletion logic for the prover
     */ autocompleteProverCommand ( currentInput , opt ? ) { if ( opt ?. fullSet ) { if ( opt ?. commandsOnly ) { return this . hintsObject ?. commands ? Object . keys ( this . hintsObject . commands ) : [ ] ; } const symbols = this . hintsObject ?. symbols ; const mathObjects = this . mathObjects ?. lemmas ; const commands = this . hintsObject ?. commands ? Object . keys ( this . hintsObject . commands ) : [ ] ; return symbols . concat ( mathObjects ) . concat ( commands ) ; } if ( currentInput ) { let hints = [ ] ; const symCode = this . matchSymCode ( currentInput ) ; const syms = symCode ?. code ? this . mathSymbols . filter ( ( sym ) => { return sym && sym . startsWith ( symCode . code ) ; } ) : null ; if ( syms ?. length ) { return syms ; } if ( currentInput . startsWith ( "expand" ) || currentInput . startsWith ( "expand*" ) || currentInput . startsWith ( "rewrite" ) || currentInput . startsWith ( "eval-expr" ) ) { const symbols = this . hintsObject ?. symbols ; const expandCommands = [ "expand" , "rewrite" , "eval-expr" , "expand*" ] ; for ( let i = 0 ; i < symbols ?. length ; i ++ ) { for ( let j = 0 ; j < expandCommands . length ; j ++ ) { const hint = `${ expandCommands [ j ] } "${ symbols [ i ] }"` ; if ( hint . startsWith ( currentInput ) ) { hints . push ( hint ) ; } } } } else if ( currentInput . startsWith ( "lemma" ) || currentInput . startsWith ( "apply-lemma" ) ) { if ( this . mathObjects ?. lemmas ?. length ) { const symbols = this . mathObjects ?. lemmas ; const lemmaCommands = [ "lemma" , "apply-lemma" ] ; for ( let i = 0 ; i < symbols ?. length ; i ++ ) { for ( let j = 0 ; j < lemmaCommands . length ; j ++ ) { const hint = `${ lemmaCommands [ j ] } "${ symbols [ i ] }"` ; if ( hint . startsWith ( currentInput ) ) { hints . push ( hint ) ; } } } } } else if ( currentInput . startsWith ( "help" ) ) { const cmds = this . sessionType === "prover" ? Object . keys ( { ... PROOF_COMMANDS , ... PROOF_TACTICS } ) : Object . keys ( EVALUATOR_COMMANDS ) ; for ( let i = 0 ; i < cmds ?. length ; i ++ ) { const hint = `help ${ cmds [ i ] }` ; if ( hint . startsWith ( currentInput ) ) { hints . push ( hint ) ; } } } else { hints = this . hintsObject ?. commands ? Object . keys ( this . hintsObject . commands ) ?. filter ( ( c ) => { return c . startsWith ( currentInput ) ; } ) : [ ] ; } return hints ; } return [ ] ; } /**
     * Autocompletion logic for the evaluator
     */ autocompleteEvaluatorCommand ( currentInput , opt ? ) { if ( opt ?. fullSet ) { if ( opt ?. commandsOnly ) { return this . hintsObject ?. commands ? Object . keys ( this . hintsObject . commands ) : [ ] ; } const symbols = this . hintsObject ?. symbols ; const commands = this . hintsObject ?. commands ? Object . keys ( this . hintsObject ?. commands ) : [ ] ; return symbols . concat ( commands ) ; } if ( currentInput ) { let hints = [ ] ; const symCode = this . matchSymCode ( currentInput ) ; const syms = symCode ?. code ? this . mathSymbols . filter ( ( sym ) => { return sym && sym . startsWith ( symCode . code ) ; } ) : null ; if ( syms ?. length ) { return syms ; } const symbols = this . hintsObject ?. symbols ; if ( symbols ?. length ) { hints = symbols ?. filter ( ( c ) => { return c . startsWith ( currentInput ) ; } ) ; } const cmds = this . hintsObject ?. commands ? Object . keys ( this . hintsObject . commands ) . filter ( ( c ) => { return c . startsWith ( currentInput ) ; } ) : [ ] ; hints = hints . concat ( cmds ) ; return hints ; } return [ ] ; } /**
     * Returns the hints, based on the current input entered by the user and the session type
     */ getHints ( opt ? ) { opt = opt || { } ; opt . includeHistory = ( opt . includeHistory === undefined ) ? true : ! ! opt . includeHistory ; const currentInput = this . getCurrentInput ( { removeLeadingBracket : true } ) ; let hints = this . sessionType === "evaluator" ? this . autocompleteEvaluatorCommand ( currentInput , opt ) : this . autocompleteProverCommand ( currentInput , opt ) ; if ( opt . includeHistory ) { let successHistory = opt ?. fullSet ? this . history . getSuccessHistory ( ) : this . history . getSuccessHistory ( { match : currentInput } ) ; successHistory = successHistory . filter ( ( elem ) => { return ! hints . includes ( elem ) ; } ) ; hints = hints . concat ( successHistory ) ; } return hints ?. sort ( ( a , b ) => { if ( this . sessionType === "prover" && this . frequentCommands ?. length ) { for ( let i = 0 ; i < this . frequentCommands . length ; i ++ ) { if ( a === this . frequentCommands [ i ] ) { return - 1 ; } if ( b === this . frequentCommands [ i ] ) { return 1 ; } } } return a < b ? - 1 : 1 ; } ) || [ ] ; } /**
     * Updates autocomplete information shown in the tooltip
     */ updateTooltip ( ) { const hints = this . getHints ( { includeHistory : true } ) ; this . showTooltip ( hints ) ; this . updateHelp ( ) ; } /**
     * Handler for arrow press events
     */ onArrow ( evt ) { switch ( evt . key ) { case "ArrowDown" : { this . selectNext ( ) ; break ; } case "ArrowUp" : { this . selectPrev ( ) ; break ; } default : { break ; } } } /**
     * Highlights the n-th hint shown in the tooltip
     */ highlight ( n ) { const $hints = $ ( ".autocompletion-item" ) ; this . clearHighlight ( ) ; $ ( $hints [ n ] ) . addClass ( "highlighted" ) ; } /**
     * Clears hints highlight
     */ clearHighlight ( ) { $ ( ".autocompletion-item" ) . removeClass ( "highlighted" ) ; } /**
     * Updates integrated help
     */ updateHelp ( opt ? ) { opt = opt || { } ; const currentInput = this . getCurrentInput ( { regex : /[\w\+\@\-\*\?\!]+/ } ) ; let cmd = opt . cmd || this . getSelectedHint ( ) || currentInput ; cmd = cmd ?. split ( " " ) [ 0 ] ; const desc = this . sessionType === "evaluator" ? evaluatorCommands [ cmd ] : proverCommands [ cmd ] ; const integratedHelp = Handlebars . compile ( terminalHelpTemplate , { noEscape : true } ) ( { cmd , ... desc , syntax : this . sessionType === "prover" ? `(${ desc ?. syntax })` : `${ desc ?. syntax };` , footnote : this . sessionType === "prover" && ! VSCODE_COMMANDS [ cmd ] ? `Use (help ${ cmd }) to display additional help information.` : "" } ) ; this . showHelp ( integratedHelp ) ; if ( ! currentInput && integratedHelp ) { this . showHelp ( welcomeMessage ( this . sessionType , this . integratedHelpSize ) ) ; } } /**
     * Returns the size of the integrated help (in number of lines)
     */ getIntegratedHelpSize ( ) { return this . integratedHelpSize ; } /**
     * Shows message in the integrated help
     */ showHelp ( msg ) { if ( this . currHelp !== msg ) { this . currHelp = msg ; $ ( ".terminal-help" ) . html ( this . currHelp ) ; } } /**
     * Clears the integrated help
     */ clearHelp ( ) { $ ( ".terminal-help" ) . empty ( ) ; } /**
     * Internal function, selects the n-th hint shown in the tooltip
     */ select ( index ) { if ( index >= 0 && index < this . currentHints ?. length ) { this . highlight ( index ) ; this . clearSelection ( ) ; this . highlight ( index ) ; $ ( $ ( ".autocompletion-item" ) [ index ] ) . addClass ( "selected" ) ; $ ( ".autocompletion-item" ) [ index ] . scrollIntoView ( { block : "nearest" } ) ; this . updateHelp ( ) ; } } /**
     * Selects next tooltip
     */ selectNext ( ) { const selected = $ ( ".autocompletion-item.selected" ) ; const index = this . getIndex ( selected [ 0 ] ) ; this . select ( index + 1 ) ; } /**
     * Selects previous tooltip
     */ selectPrev ( ) { const selected = $ ( ".autocompletion-item.selected" ) ; const index = this . getIndex ( selected [ 0 ] ) ; this . select ( index - 1 ) ; } /**
     * Clear selection
     */ clearSelection ( ) { $ ( ".autocompletion-item" ) . removeClass ( "selected" ) ; } /**
     * Internal function, returns the index of the selected item
     */ getIndex ( target ) { if ( target ) { const matchIndex = /\bindex-(\d+)/g . exec ( target ?. className ) ; if ( matchIndex && matchIndex . length > 1 ) { const index = + matchIndex [ 1 ] ; return index ; } } return NaN ; } /**
     * Returns the selected hint
     */ getSelectedHint ( ) { const selected = $ ( ".autocompletion-item.selected" ) ; if ( selected [ 0 ] ) { const matchIndex = /index-(\d+)/ . exec ( selected [ 0 ] . className ) ; if ( matchIndex ?. length > 1 && ! isNaN ( + matchIndex [ 1 ] ) ) { const index = + matchIndex [ 1 ] ; if ( index >= 0 && index < this . currentHints . length ) { const val = this . currentHints [ index ] ; return val ; } } console . warn ( "[xterm-pvs] Warning: incorrect index in tooltip, returning tooltip content as fallback" , { matchIndex , currentHints : this . currentHints } ) ; } return "" ; } /**
     * Internal function, triggers autocomplete
     */ protected triggerAutocomplete ( ) { let substitution = this . getSelectedHint ( ) ; let match = this . getCurrentInput ( { removeLeadingBracket : true } ) ; if ( substitution ?. startsWith ( "\\" ) && match . includes ( "\\" ) ) { const info = substitution ?. split ( " " ) ; const symCode = this . matchSymCode ( match ) ; if ( info ?. length > 1 && symCode ?. code ) { match = symCode . code ; substitution = info [ 1 ] ; } } const currentInput = this . getCurrentInput ( ) ; const evt = { substitution , currentInput , match } ; this . trigger ( AutocompleteEvent . didAutocomplete , evt ) ; this . deleteTooltips ( ) ; } /**
     * updates tooltips based on keypress events
     */ autocompleteOnKeyPress ( ev , opt ? ) { switch ( ev . key ) { case "Backspace" : { this . updateTooltip ( ) ; break ; } case "Delete" : { this . updateTooltip ( ) ; break ; } case "ArrowUp" : case "ArrowDown" : { this . onArrow ( ev ) ; break ; } case "ArrowLeft" : case "ArrowRight" : { this . updateTooltip ( ) ; break ; } case " " : { if ( opt ?. force ) { this . triggerAutocomplete ( ) ; } else { this . updateTooltip ( ) ; } break ; } case "Escape" : { this . deleteTooltips ( ) ; this . updateHelp ( ) ; break ; } case "Enter" : case "Tab" : { this . triggerAutocomplete ( ) ; break ; } default : { this . updateTooltip ( ) ; break ; } } } } const xtermjsColorThemes = { dark : { background : htmlColorCode . black , foreground : htmlColorCode . white , cursor : htmlColorCode . white , selection : htmlColorCode . blue } , light : { background : htmlColorCode . white , foreground : htmlColorCode . black , cursor : htmlColorCode . black , selection : htmlColorCode . darkblue } } ; /**
 * XTermPvs extends the functionalities of xterm.js by introducing:
 * - syntax highlighting for pvs
 * - virtual document for storing terminal content and command line
 * - highligh for matching brackets
 * ANSI sequences supported by xterm.js are at https://xtermjs.org/docs/api/vtfeatures/
 */ export class XTermPvs extends Backbone . Model { protected content : Content ; protected xterm : XTerm ; protected runningFlag : boolean = false ; protected autocomplete : Autocomplete ; protected sessionType : SessionType ; protected parent : string ; protected fontSize : number = 12 ; protected lineHeight : number = 1.2 ; protected paddingBottom : number = 0 ; protected modKeys : ModKeys = { alt : false , ctrl : false , meta : false } ; protected brackets : MatchBrackets ; protected timer : NodeJS . Timer = null ; readonly timerTimeout : number = 50 ; protected inputEnabled : boolean = true ; protected commands : CommandsMap = null ; protected TAB_SIZE : number = 4 ; protected prompt : string = "> " ; protected ntrims : number = 0 ; protected autocompleteWithEnterFlag : boolean = true ; protected colorTheme : XTermColorTheme = "dark" ; protected pos : Position = { line : MIN_POS . line , character : MIN_POS . character } ; /**
     * Constructor
     */ constructor ( opt ? ) { super ( ) ; opt = opt || { } ; this . content = new Content ( ) ; this . sessionType = opt ?. sessionType || "evaluator" ; this . autocomplete = new Autocomplete ( this . content , this . sessionType , { integratedHelpSize : opt ?. integratedHelpSize , frequentCommands : opt ?. frequentCommands } ) ; this . paddingBottom = opt ?. paddingBottom || 0 ; const cols = opt . cols || MIN_VIEWPORT_COLS ; LineWrapper . maxCols = cols ; const rows = opt . rows || Math . floor ( ( window . innerHeight - this . paddingBottom ) / ( this . fontSize * this . lineHeight ) ) || MIN_VIEWPORT_ROWS ; this . colorTheme = this . getColorTheme ( ) ; this . xterm = new XTerm ( { rendererType : "canvas" , cols , rows , fontSize : this . fontSize , fontFamily : "Menlo, Monaco, monospace" , scrollback : 2048 } ) ; this . updateColorTheme ( ) ; $ ( "#terminal" ) . append ( tooltipStyle ) ; $ ( "body" ) . append ( terminalStyle ) ; this . parent = opt ?. parent || "terminal" ; this . xterm . open ( document . getElementById ( this . parent ) ) ; this . installHandlers ( ) ; this . xterm . focus ( ) ; this . xterm . setOption ( "cursorBlink" , true ) ; console . log ( "[xterm-pvs] Init complete" , { colorTheme : this . colorTheme , xterm : this . xterm , jquery : $ ( `#${ this . parent }` ) , } ) ; } /**
     * Detects the color theme
     */ getColorTheme ( ) { const themeClass = $ ( "body" ) . attr ( "data-vscode-theme-kind" ) ; const theme = xTermDetectColorTheme ( themeClass ) ; return theme ; } /**
     * Sets dark color theme
     */ darkMode ( ) { this . xterm . setOption ( "theme" , xtermjsColorThemes . dark ) ; this . xterm . setOption ( "cursorStyle" , "block" ) ; $ ( "body" ) . css ( { color : xtermjsColorThemes . dark . foreground , background : xtermjsColorThemes . dark . background } ) ; $ ( ".terminal-help" ) . css ( { color : xtermjsColorThemes . dark . foreground } ) ; } /**
     * Sets light color theme
     */ lightMode ( ) { this . xterm . setOption ( "theme" , xtermjsColorThemes . light ) ; this . xterm . setOption ( "cursorStyle" , "bar" ) ; $ ( "body" ) . css ( { color : xtermjsColorThemes . light . foreground , background : xtermjsColorThemes . light . background } ) ; $ ( ".terminal-help" ) . css ( { color : xtermjsColorThemes . light . foreground } ) ; } param desc protected formatHelp ( cmd , desc ) { if ( desc ) { return `\n${ colorUtils . colorText ( `(${ cmd })` , colorUtils . PvsColor . green ) }
\t${ desc . description }
\tSyntax: (${ desc . syntax })\n` ; } return "" ; } /**
     * Shows all available commands and some brief info for each command
     */ helpStar ( ) { const cmds = this . sessionType === "evaluator" ? evaluatorCommands : proverCommands ; let ans = "" ; const keys = Object . keys ( cmds ) . sort ( ( a , b ) => { return a > b ? 1 : - 1 ; } ) ; for ( let i = 0 ; i < keys . length ; i ++ ) { if ( cmds [ keys [ i ] ] . description ) { ans += this . formatHelp ( keys [ i ] , cmds [ keys [ i ] ] ) ; } } this . write ( ans ) ; } /**
     * Shows all available commands and some brief info for each command
     */ helpVSCodePlot ( ) { const ans = this . formatHelp ( "vscode-plot" , proverCommands [ "vscode-plot" ] ) ; this . write ( ans ) ; } /**
     * Disables terminal input
     */ disableInput ( ) { this . inputEnabled = false ; } /**
     * Enables terminal input
     */ enableInput ( ) { this . inputEnabled = true ; } /**
     * Utility function, updates color theme
     */ updateColorTheme ( theme ? ) { this . colorTheme = theme || this . getColorTheme ( ) ; ( this . colorTheme === "dark" ) ? this . darkMode ( ) : this . lightMode ( ) ; } /**
     * Internal function, finds out which mod keys have been pressed
     */ protected getActiveModKeys ( ) { const active = [ ] ; for ( let i in this . modKeys ) { if ( this . modKeys [ i ] ) { active . push ( i ) ; } } return active . join ( " " ) ; } /**
     * Internal function, checks if a mod key is active
     */ protected modKeyIsActive ( ) { for ( let i in this . modKeys ) { if ( this . modKeys [ i ] ) { return true ; } } return false ; } /**
     * Updates hints data for autocompletion
     */ updateHints ( hints ) { this . autocomplete . updateHints ( hints ) ; if ( hints . commands && ! this . commands ) { this . commands = hints . commands ; } } /**
     * Updates mathObjects for autocompletion
     */ updateMathObjects ( mathObjects ) { this . autocomplete . updateMathObjects ( mathObjects ) ; } /**
     * Clears the content of the screen and resets the cursor position to its initial position (top-left corner)
     * see also http://ascii-table.com/ansi-escape-sequences.php
     * and https://xtermjs.org/docs/api/vtfeatures/
     * and https://gist.github.com/fnky/458719343aabd01cfb17a3a4f7296797
     */ clearScreen ( ) { this . content . deleteContent ( ) ; this . pos = { ... MIN_POS } ; this . xterm . clear ( ) ; this . xterm . write ( "\x1B[2J" ) ; this . xterm . write ( "\x1B[H" ) ; } /**
     * Internal function, clears text after position pos (character at pos excluded)
     * Use clearTextFrom if you want to clear also the character at the given position.
     */ protected clearTextAfter ( pos ) { this . clearTextFrom ( { line : pos . line , character : pos . character + 1 } ) ; } /**
     * Internal function, clears text from position pos.
     */ protected clearTextFrom ( pos ) { if ( pos ) { this . saveCursorPosition ( ) ; this . moveCursorTo ( { line : pos . line , character : pos . character } , { src : "clearTextFrom" , temp : true } ) ; this . xterm . write ( "\x1B[0J" ) ; this . restoreCursorPosition ( ) ; } } /**
     * Internal function, clears text at line n
     */ protected clearLine ( n ) { if ( n ) { this . saveCursorPosition ( ) ; this . moveCursorTo ( { line : n , character : MIN_POS . character } , { src : "clearLine" , temp : true } ) ; this . xterm . write ( "\x1B[2K" ) ; this . restoreCursorPosition ( ) ; } } /**
     * Internal function, refreshes the command line
     */ protected refreshCommandLine ( ) { const pos = this . content . cursorPosition ( ) ; const base = this . content . getHomePosition ( ) ; this . moveCursorTo ( base , { src : "refreshCommandLine " } ) ; this . clearTextFrom ( base ) ; const cmd = this . content . command ( ) . replace ( /\n/g , "\r\n" ) ; this . saveCursorPosition ( ) ; this . xterm . write ( this . applySyntaxHighlighting ( cmd , this . colorTheme ) ) ; this . restoreCursorPosition ( ) ; const nLines = cmd . split ( "\r\n" ) . length ; const atBufferEnd = this . xterm . buffer . active . cursorY + this . xterm . buffer . active . baseY >= this . xterm . buffer . active . length - 1 ; if ( atBufferEnd && nLines > 1 ) { this . cursorUp ( nLines - 1 ) ; } this . moveCursorTo ( pos , { src : "refreshCommandLine" } ) ; } /**
     * Internal function, refresh the terminal content after cursor
     */ protected refresh ( ) { const pos = this . content . cursorPosition ( ) ; this . clearTextAfter ( pos ) ; const text = this . content . textAfter ( pos ) ; this . xterm . write ( this . applySyntaxHighlighting ( text , this . colorTheme ) ) ; this . moveCursorTo ( pos , { src : "refresh" } ) ; } /**
     * Scroll the terminal content to the given position
     * A timeout is used to give time to the buffer to render the content
     * (if scrolling is performed without the timeout, the buffer has still the
     *  old content, and so it won't scroll to the intended final cursor position)
     */ scrollCursorIntoView ( ) { clearTimeout ( this . timer ) ; this . timer = setTimeout ( ( ) => { $ ( ".xterm-helper-textarea" ) [ 0 ] . scrollIntoView ( { block : "nearest" } ) ; } , this . timerTimeout ) ; } /**
     * Highlights matching brackets
     */ matchBrackets ( bracket ? ) { const b1 = bracket || "(" ; const match = this . content . matchBrackets ( b1 ) ; if ( match ?. pos1 !== this . brackets ?. pos1 || match ?. pos2 !== this . brackets ?. pos2 ) { if ( this . brackets ) { if ( this . brackets . pos1 ) { this . moveCursorTo ( this . brackets . pos1 , { src : "matchBrackets" } ) ; this . renderData ( this . content . charAt ( this . brackets . pos1 ) ) ; } if ( this . brackets . pos2 ) { this . moveCursorTo ( this . brackets . pos2 , { src : "matchBrackets" } ) ; this . renderData ( this . content . charAt ( this . brackets . pos2 ) ) ; } } if ( match ?. pos1 ) { this . moveCursorTo ( match . pos1 , { src : "matchBrackets" } ) ; const par = colorUtils . ansiColorText ( this . content . charAt ( match . pos1 ) , { background : colorUtils . PvsColor . gold , foreground : colorUtils . PvsColor . black , bold : true } ) ; this . renderData ( par ) ; } if ( match ?. pos2 ) { this . moveCursorTo ( match . pos2 , { src : "matchBrackets" } ) ; const opt = match . pos1 ? { background : colorUtils . PvsColor . gold , foreground : colorUtils . PvsColor . black , bold : true } : { background : colorUtils . PvsColor . red , foreground : colorUtils . PvsColor . white } ; const par = colorUtils . ansiColorText ( this . content . charAt ( match . pos2 ) , opt ) ; this . renderData ( par ) ; } this . brackets = match ; this . moveCursorTo ( this . content . cursorPosition ( ) , { src : "matchBrackets" } ) ; } } /**
     * Internal function, triggers event "sendText" when input is ready
     */ protected sendWhenReady ( ) { const cmd = this . content . command ( ) . trim ( ) ; if ( cmd ) { switch ( this . sessionType ) { case "evaluator" : { if ( this . readyToSend ( cmd ) ) { this . trigger ( XTermEvent . sendText , { data : cmd } ) ; this . autocomplete . updateCommandHistory ( cmd ) ; this . disableInput ( ) ; return true ; } break ; } case "prover" : { if ( this . readyToSend ( cmd ) ) { this . trigger ( XTermEvent . sendText , { data : cmd } ) ; this . autocomplete . updateCommandHistory ( cmd ) ; this . disableInput ( ) ; return true ; } break ; } default : { break ; } } } return false ; } /**
     * Internal function, checks if the input is ready to be sent
     */ protected readyToSend ( cmd ? ) { const cmdline = cmd !== undefined ? cmd : this . content . command ( ) . trim ( ) ; if ( cmdline ) { switch ( this . sessionType ) { case "evaluator" : { if ( cmdline . trim ( ) . endsWith ( ";" ) || cmdline . trim ( ) . endsWith ( "!" ) || cmdline ?. trim ( ) === "quit" ) { return true ; } break ; } case "prover" : { if ( checkPar ( cmdline ) ?. success || cmdline ?. trim ( ) === "quit" ) { return true ; } break ; } default : { break ; } } } return false ; } /**
     * Internal function, updates the terminal view based on the information given by this.content
     */ protected updateView ( keyEvent , opt ? ) { const domEvent = keyEvent . domEvent ; const key = keyEvent . key ; switch ( domEvent . key ) { case "Backspace" : { this . onRenderBackspace ( ) ; break ; } case "Delete" : { this . onRenderDelete ( ) ; break ; } case "Enter" : { this . onRenderEnter ( ) ; break ; } case "ArrowUp" : case "ArrowDown" : case "ArrowLeft" : case "ArrowRight" : { this . onRenderArrow ( ) ; break ; } case " " : { this . onRenderText ( key ) ; break ; } case "Escape" : case "Tab" : { break ; } default : { this . onRenderText ( key ) ; break ; } } const pos = this . cursorPosition ( ) ; const textLine = this . content . textLineAt ( pos ) ; this . moveCursorTo ( { line : pos . line , character : MIN_POS . character } , { src : "updateView" } ) ; this . saveCursorPosition ( ) ; this . xterm . write ( this . applySyntaxHighlighting ( textLine , this . colorTheme ) ) ; this . restoreCursorPosition ( ) ; if ( ! opt ?. disableParMatch ) { this . matchBrackets ( ) ; } this . moveCursorTo ( pos , { src : "updateView" } ) ; this . scrollCursorIntoView ( ) ; } /**
     * Updates success history
     */ updateCommandHistory ( data ) { if ( data . cmd ) { this . autocomplete . updateCommandHistory ( data . cmd , { successHistory : true } ) ; } } /**
     * Handler for command history search
     */ onHistorySearch ( evt ) { if ( this . autocomplete . history . size ( ) && this . content . cursorIsAtHomePosition ( ) && ! this . autocomplete . tooltipVisible ( ) && ( evt . domEvent . key === "ArrowUp" || evt . domEvent . key === "ArrowDown" ) ) { const cmd = evt . domEvent . key === "ArrowUp" ? this . autocomplete . history . prev ( ) : this . autocomplete . history . next ( ) ; this . content . setCommand ( cmd , { cursorToHome : true } ) ; return true ; } return false ; } /**
     * Moves the cursor to the end of the command line
     */ moveCursorToEnd ( ) { const success = this . content . cursorToEnd ( ) ; if ( success ) { const pos = this . content . cursorPosition ( ) ; this . moveCursorTo ( pos , { src : "attachCustomKeyEventHandler" } ) ; } } /**
     * Moves the cursor to the home position
     */ moveCursorToHome ( ) { const success = this . content . cursorToHome ( ) ; if ( success ) { const pos = this . content . cursorPosition ( ) ; this . moveCursorTo ( pos , { src : "attachCustomKeyEventHandler" } ) ; } } /**
     * Handler for key press events
     */ onKeyPress ( evt ) { const historySearch = this . onHistorySearch ( evt ) ; if ( ! historySearch && ! this . modKeyIsActive ( ) ) { const key = evt ?. domEvent ?. key ; const selectedHint = this . autocomplete ?. getSelectedHint ( ) ; const commandLine = this . content ?. command ( ) ?. trim ( ) ; if ( selectedHint ?. startsWith ( "\\" ) && ( key === "Enter" || key === " " ) ) { this . autocomplete . autocompleteOnKeyPress ( evt ?. domEvent , { force : true } ) ; return ; } if ( key === "Enter" && this . readyToSend ( ) && ( selectedHint === commandLine || ! selectedHint || ! this . autocompleteWithEnterFlag ) ) { this . brackets = null ; this . autocomplete . deleteTooltips ( ) ; this . moveCursorToEnd ( ) ; this . content . updateContent ( evt ) ; this . updateView ( evt , { disableParMatch : true } ) ; this . xterm . setOption ( "cursorBlink" , true ) ; this . sendWhenReady ( ) ; return ; } if ( key === "Enter" && selectedHint ) { this . autocomplete . autocompleteOnKeyPress ( evt ?. domEvent ) ; return ; } const selectingTooltip = ( key === "ArrowUp" || key === "ArrowDown" ) && this . autocomplete . tooltipVisible ( ) ; const contentHasChanged = selectingTooltip ? false : this . content . updateContent ( evt ) ; this . autocomplete . autocompleteOnKeyPress ( evt ?. domEvent ) ; if ( contentHasChanged ) { this . updateView ( evt ) ; } const hints = this . autocomplete . getHints ( ) ; if ( hints ?. length === 1 ) { const cmd = this . content . command ( ) ; if ( hints [ 0 ] === cmd ) { this . autocomplete . deleteTooltips ( ) ; } } } } /**
     * Shows a tooltip with the full list of commands
     */ showCommands ( ) { const hints = this . autocomplete . getHints ( { fullSet : true , includeHistory : false , commandsOnly : true } ) ; this . autocomplete . showTooltip ( hints ) ; this . autocomplete . updateHelp ( ) ; } /**
     * Updates autocompletion tooltip
     */ updateAutocomplete ( ) { this . autocomplete . updateTooltip ( ) ; } /**
     * Utility function, returns the current cursor position
     */ cursorPosition ( ) { return this . content . cursorPosition ( ) ; } /**
     * Handler for control sequences sent programmatically to the terminal,
     * e.g., following a mouse click event that repositions the mouse
     */ onControlSequence ( seq ) { let delta = 0 ; for ( let i = 0 ; i < seq . length ; i ++ ) { switch ( seq [ i ] ) { case "\x1B[C" : { delta ++ ; break ; } case "\x1B[D" : { delta -- ; break ; } default : { break ; } } } const pos = this . content . cursorPosition ( ) ; const relCol = this . xterm . buffer . active . cursorX + 1 + delta ; const deltaLine = Math . floor ( relCol / this . xterm . cols ) ; const col = relCol % this . xterm . cols ; const targetPos = { character : col < 0 ? col + this . xterm . cols : col , line : pos . line + deltaLine } ; const success = this . content . cursorTo ( targetPos ) ; if ( success ) { this . moveCursorTo ( this . content . cursorPosition ( ) , { src : "onControlSequence" } ) ; } } /**
     * Handler for data events (e.g., cut/paste in the terminal)
     */ onData ( data ) { if ( this . modKeyIsActive ( ) && data ) { if ( data . startsWith ( "\x1B[" ) ) { const seq = data . split ( "\x1B[" ) . map ( elem => { return "\x1B[" + elem ; } ) ; this . onControlSequence ( seq ) ; return ; } data = LineWrapper . wrapLines ( data ) ; this . content . writeData ( data ) ; const prevPos0 = { line : this . content . previousCursorPosition ( ) . line , character : 1 } ; const textAfter = this . content . textAfter ( prevPos0 ) ; this . clearTextAfter ( prevPos0 ) ; this . moveCursorTo ( prevPos0 , { src : "onData" } ) ; const colorText = this . applySyntaxHighlighting ( textAfter . replace ( /\n/g , "\r\n" ) , this . colorTheme ) ; this . renderData ( colorText ) ; const pos = this . content . cursorPosition ( ) ; this . moveCursorTo ( pos , { src : "onData" } ) ; this . scrollCursorIntoView ( ) ; } } /**
     * Internal function, install relevant event handlers
     */ protected installHandlers ( ) { this . xterm . onKey ( ( evt ) => { this . onKeyPress ( evt ) ; } ) ; this . xterm . onData ( ( data ) => { this . onData ( data ) ; } ) ; this . xterm . attachCustomKeyEventHandler ( ( evt ) : boolean => { this . modKeys = { alt : ! ! evt ?. altKey , ctrl : ! ! evt ?. ctrlKey , meta : ! ! evt ?. metaKey } ; if ( this . runningFlag && evt ?. ctrlKey && evt . key === "c" ) { this . trigger ( XTermEvent . sendText , { data : interruptCommand } ) ; return false ; } if ( this . inputEnabled && this . modKeyIsActive ( ) && evt . key === "c" ) { if ( evt . type === "keydown" ) { const sel = this . xterm . getSelection ( ) ; this . trigger ( XTermEvent . didCopyText , { data : sel } ) ; } return false ; } if ( this . inputEnabled && this . modKeyIsActive ( ) && evt . key === "x" ) { return false ; } if ( this . inputEnabled && this . modKeyIsActive ( ) && evt . key === "v" ) { this . autocomplete . deleteTooltips ( ) ; return false ; } if ( evt . key === "PageUp" ) { this . xterm . scrollLines ( - 4 ) ; return false ; } if ( evt . key === "PageDown" ) { this . xterm . scrollLines ( 4 ) ; return false ; } if ( this . inputEnabled && this . modKeyIsActive ( ) && ! evt ?. shiftKey ) { switch ( evt . key ) { case " " : { this . showCommands ( ) ; break ; } case "Home" : { this . moveCursorToHome ( ) ; break ; } case "End" : { this . moveCursorToEnd ( ) ; break ; } case "ArrowLeft" : { const success = this . content . cursorToPreviousWord ( ) ; if ( success ) { const pos = this . content . cursorPosition ( ) ; this . moveCursorTo ( pos , { src : "attachCustomKeyEventHandler" } ) ; this . inputEnabled = false ; setTimeout ( ( ) => { this . inputEnabled = true ; } , 100 ) ; } break ; } case "ArrowRight" : { const success = this . content . cursorToNextWord ( ) ; if ( success ) { const pos = this . content . cursorPosition ( ) ; this . moveCursorTo ( pos , { src : "attachCustomKeyEventHandler" } ) ; this . inputEnabled = false ; setTimeout ( ( ) => { this . inputEnabled = true ; } , 100 ) ; } break ; } case "Delete" : case "Backspace" : { this . clearCommandLine ( ) ; break ; } default : { break ; } } return false ; } if ( this . inputEnabled && evt . key === "F4" ) { return false ; } if ( this . inputEnabled && evt . key === "F5" ) { return false ; } if ( this . inputEnabled && evt . key === "F6" ) { return false ; } if ( this . inputEnabled && evt . key === "F2" ) { return false ; } return this . inputEnabled && ( ! this . modKeyIsActive ( ) || evt . key === "ArrowUp" || evt . key === "ArrowDown" ) ; } ) ; $ ( window ) . on ( "resize" , ( evt ) => { const rows = Math . floor ( ( window . innerHeight - this . paddingBottom ) / ( this . fontSize * this . lineHeight ) ) || MIN_VIEWPORT_ROWS ; this . resizeLines ( rows ) ; } ) ; $ ( document ) . on ( "dblclick" , ( evt ) => { const sel = this . xterm . getSelection ( ) ; if ( sel && this . autocomplete . validSymbol ( sel ) ) { this . autocomplete . showTooltip ( [ `(expand "${ sel }")` , `(expand "${ sel }" +)` , `(expand "${ sel }" -)` ] , { top : evt . pageY , left : evt . pageX } ) ; } else { this . autocomplete . deleteTooltips ( ) ; } } ) ; $ ( document ) . on ( "click" , ( evt ) => { this . autocomplete . deleteTooltips ( ) ; this . focus ( ) ; } ) ; this . content . on ( ContentEvent . rebase , ( evt ) => { this . onRebaseContent ( evt ) ; } ) ; this . content . on ( ContentEvent . didAutocompleteContent , ( ) => { this . refreshCommandLine ( ) ; this . focus ( ) ; } ) ; this . autocomplete . on ( AutocompleteEvent . didAutocomplete , ( evt ) => { this . onResolveAutocomplete ( evt ) ; this . focus ( ) ; this . xterm . clearSelection ( ) ; } ) ; } /**
     * Internal function, handles rebase events triggered by content
     */ protected onRebaseContent ( evt ) { if ( evt ?. pos ) { this . pos = { line : evt . pos . line , character : evt . pos . character } ; } } /**
     * Internal function, handles resolve events triggered by autocomplete
     */ protected onResolveAutocomplete ( evt ) { this . content . autocomplete ( evt ) ; } /**
     * Handles delete key presses
     */ protected onRenderDelete ( ) { const pos = this . content . cursorPosition ( ) ; const textAfter = this . content . textAfter ( pos ) ; this . xterm . write ( `\x1B[1P` ) ; if ( textAfter ) { this . clearTextFrom ( { line : pos . line + 1 , character : MIN_POS . character } ) ; this . saveCursorPosition ( ) ; this . xterm . write ( textAfter . replace ( /\n/g , "\r\n" ) ) ; this . restoreCursorPosition ( ) ; } } /**
     * Handles backspace key presses
     */ protected onRenderBackspace ( ) { const pos = this . content . cursorPosition ( ) ; this . moveCursorTo ( pos , { src : "onRenderBackspace" } ) ; this . onRenderDelete ( ) ; } /**
     * Handles renering for Enter key presses
     */ protected onRenderEnter ( ) { const pos = this . content . cursorPosition ( ) ; const prevPos = this . content . previousCursorPosition ( ) ; const textAfter = this . content . textAfter ( pos ) ; if ( textAfter ) { this . clearTextFrom ( prevPos ) ; } this . saveCursorPosition ( ) ; this . xterm . write ( "\r\n" + textAfter . replace ( /\n/g , "\r\n" ) ) ; this . restoreCursorPosition ( ) ; this . moveCursorTo ( pos , { src : "onRenderEnter" } ) ; } /**
     * Handles arrow key presses
     */ protected onRenderArrow ( ) { const pos = this . content . cursorPosition ( ) ; this . moveCursorTo ( pos , { src : "onRenderArrow" } ) ; } /**
     * Generic handler for printable characters
     */ protected onRenderText ( txt ) { const pos = this . content . cursorPosition ( ) ; this . renderData ( txt ) ; const textLineAfter = this . content . textLineAfter ( pos ) ; if ( textLineAfter ) { this . renderData ( textLineAfter ) ; } this . moveCursorTo ( pos , { src : "onRenderChar" } ) ; } /**
     * Write text in the terminal. The received data will become read-only
     */ write ( data ) { if ( data ) { this . saveCursorPosition ( ) ; data = data . replace ( /\t/g , " " . repeat ( this . TAB_SIZE ) ) ; data = LineWrapper . wrapLines ( data ) ; this . content . writeData ( data ) ; this . renderData ( data ) ; this . restoreCursorPosition ( ) ; this . moveCursorTo ( this . content . cursorPosition ( ) , { src : "write" } ) ; this . scrollCursorIntoView ( ) ; } } /**
     * Write text in the terminal. The received data will become read-only
     */ log ( data ) { if ( data ) { this . write ( data ) ; this . content . rebase ( ) ; } } /**
     * Internal function, renders data in the terminal
     */ protected renderData ( data , opt ? ) { if ( data ) { opt = opt || { } ; let content = data . replace ( /\n/g , "\r\n" ) ; if ( content ) { const renderLines = content . split ( "\n" ) ; const pos = opt . pos || this . content . cursorPosition ( ) ; let maxCol = this . xterm . cols ; for ( let i = 0 ; i < renderLines . length ; i ++ ) { const lineLen = pos . character + renderLines [ i ] . length ; if ( lineLen > maxCol ) { maxCol = lineLen ; } } this . resizeCol ( maxCol ) ; content = colorUtils . isPlainText ( content ) ? this . applySyntaxHighlighting ( content , this . colorTheme ) : content ; this . saveCursorPosition ( ) ; this . xterm . write ( content ) ; this . restoreCursorPosition ( ) ; } return content ; } return "" ; } /**
     * Resize the number of columns of the terminal.
     * The number of columns should only grow -- otherwise some lines may become wrapped.
     */ resizeCol ( nCols ) { const maxCols = nCols > this . xterm . cols ? nCols : this . xterm . cols ; if ( maxCols > this . xterm . cols ) { this . xterm . resize ( maxCols , this . xterm . rows ) ; } } /**
     * Resize the number of lines of the terminal
     */ resizeLines ( nLines ) { this . xterm . resize ( this . xterm . cols , nLines ) ; } /**
     * Resize the terminal
     */ /**
     * Resize the terminal if needed, so that the given position is visible
     */ /**
     * Select character at position pos
     */ selectCharacter ( pos ) { if ( pos ) { const col = pos . character ; const row = pos . line ; const len = 1 ; this . xterm . select ( col , row , len ) ; } } /**
     * Place focus on the terminal
     */ focus ( ) { this . xterm . focus ( ) ; } /**
     * Clears the command line
     */ clearCommandLine ( ) { this . content . setCommand ( "" ) ; this . refresh ( ) ; } /**
     * Updates integrated help
     */ updateHelp ( ) { this . autocomplete . updateHelp ( ) ; } /**
     * Move cursor up, see also http://ascii-table.com/ansi-escape-sequences.php
     * and https://xtermjs.org/docs/api/vtfeatures/
     * and https://gist.github.com/fnky/458719343aabd01cfb17a3a4f7296797
     */ protected cursorUp ( n ) { if ( n > 0 ) { this . xterm . write ( `\x1B[${ n }A` ) ; } } /**
     * Move cursor down, see also http://ascii-table.com/ansi-escape-sequences.php
     * and https://xtermjs.org/docs/api/vtfeatures/
     * and https://gist.github.com/fnky/458719343aabd01cfb17a3a4f7296797
     */ protected cursorDown ( n ) { if ( n > 0 ) { this . xterm . write ( `\x1B[${ n }B` ) ; } } /**
     * Move cursor right, see also http://ascii-table.com/ansi-escape-sequences.php
     * and https://xtermjs.org/docs/api/vtfeatures/
     * and https://gist.github.com/fnky/458719343aabd01cfb17a3a4f7296797
     */ protected cursorRight ( n ) { if ( n > 0 ) { this . xterm . write ( `\x1B[${ n }C` ) ; } } /**
     * Move cursor left, see also http://ascii-table.com/ansi-escape-sequences.php
     * and https://xtermjs.org/docs/api/vtfeatures/
     * and https://gist.github.com/fnky/458719343aabd01cfb17a3a4f7296797
     */ protected cursorLeft ( n ) { if ( n > 0 ) { this . xterm . write ( `\x1B[${ n }D` ) ; } } /**
     * Internal function, move cursor to given position,
     * see also http://ascii-table.com/ansi-escape-sequences.php
     * and https://xtermjs.org/docs/api/vtfeatures/
     * and https://gist.github.com/fnky/458719343aabd01cfb17a3a4f7296797
     */ protected moveCursorTo ( pos , opt ) { if ( pos && pos . character && pos . line ) { const deltaY = pos . line - this . pos . line ; if ( deltaY ) { ( deltaY > 0 ) ? this . cursorDown ( deltaY ) : this . cursorUp ( - deltaY ) ; if ( ! opt ?. temp ) { this . pos . line += deltaY ; } } const deltaX = pos . character - this . pos . character ; if ( deltaX ) { ( deltaX > 0 ) ? this . cursorRight ( deltaX ) : this . cursorLeft ( - deltaX ) ; if ( ! opt ?. temp ) { this . pos . character += deltaX ; } } } } param n /**
     * Internal function, saves cursor position
     */ protected saveCursorPosition ( ) { this . xterm . write ( `\x1B[s` ) ; } /**
     * Internal function, restores cursor position
     */ protected restoreCursorPosition ( ) { this . xterm . write ( `\x1B[u` ) ; } /**
     * Internal function, applies pvs syntax highlighting to the provided text
     */ protected applySyntaxHighlighting ( text , theme ? ) { theme = theme || "dark" ; if ( text ) { let htext = text ; for ( let i in pvsColorTheme ) { const color = pvsColorTheme [ i ] [ theme ] ; const regexp = new RegExp ( pvsColorTheme [ i ] . regex , pvsColorTheme [ i ] . flags ) ; htext = htext . replace ( regexp , ( txt ) => { return colorUtils . colorText ( txt , color ) ; } ) ; } const regexp = new RegExp ( `^${ this . prompt . trimEnd ( ) }\\s` ) ; htext = htext . replace ( regexp , ( txt ) => { return colorUtils . colorText ( txt , theme === "dark" ? colorUtils . PvsColor . blue : colorUtils . PvsColor . darkblue ) ; } ) ; return htext ; } return text ; } /**
     * Shows a welcome message in the integrated help panel
     */ showWelcomeMessage ( ) { this . xterm . setOption ( "cursorBlink" , false ) ; this . autocomplete . showHelp ( welcomeMessage ( this . sessionType , this . autocomplete . getIntegratedHelpSize ( ) ) ) ; } /**
     * Sets/Resets the running flag, which indicates that the prover is running a command
     */ running ( flag ) { this . runningFlag = ! ! flag ; this . xterm . setOption ( "cursorBlink" , true ) ; this . autocomplete . showHelp ( welcomeMessage ( this . sessionType , this . autocomplete . getIntegratedHelpSize ( ) ) ) ; } /**
     * Shows a message in the integrated help panel
     */ showHelpMessage ( msg ) { if ( msg ) { this . autocomplete . showHelp ( msg . trim ( ) . replace ( /\n/g , "<br>" ) ) ; if ( msg . includes ( "close-action" ) ) { $ ( ".close-action" ) . on ( "click" , ( evt ) => { this . trigger ( XTermEvent . closeConsole ) ; } ) ; } } } /**
     * Shows the prompt.
     */ showPrompt ( prompt ) { this . prompt = colorUtils . getPlainText ( prompt ) + " " ; const cprompt = "\n\n" + this . applySyntaxHighlighting ( this . prompt , this . colorTheme ) ; this . log ( cprompt ) ; this . content . rebase ( { prompt : this . prompt } ) ; this . enableInput ( ) ; this . xterm . setOption ( "cursorBlink" , false ) ; } /**
     * Set/Reset autocompleteWithEnter flag
     */ autocompleteWithEnter ( flag ) { this . autocompleteWithEnterFlag = ! ! flag ; } }