1#!/usr/bin/env python3 2 3# holwrap: it's like rlwrap but more colourful. 4# Featuring some StandardML syntax highlighting, history and multiline input. 5# Currently does print hol output until the next prompt (">") is read, 6# if you know how to fix this please make issue or PR on github. 7 8# You will need python3 to run holwrap 9# holwrap also depends on prompt_toolkit, pexpect and pygments, installable with pip, 10# e.g., pip3 install prompt_toolkit, pexpect 11# Usage: ./holwrap.py hol <hol flags> 12# or: python3 holwrap.py hol <hol flags> 13# you could also substitute hol.bare or something here if you wanted. 14# If hol is not in your path you will need to write the full path instead. 15# e.g., python3 holwrap.py /path/to/HOL/bin/hol 16 17# Due to the mutiline input, holwrap won't send input until it sees a semicolon, 18# 'QED' or 'End'. You can force it with Esc-Enter, but it could cause problems. 19 20import sys, pexpect, re 21from pygments.lexers.ml import SMLLexer 22from prompt_toolkit import PromptSession 23from prompt_toolkit.lexers import PygmentsLexer 24from prompt_toolkit.history import FileHistory 25from prompt_toolkit.auto_suggest import AutoSuggestFromHistory 26from prompt_toolkit.key_binding import KeyBindings 27from prompt_toolkit.filters import Condition 28from prompt_toolkit.patch_stdout import patch_stdout 29from prompt_toolkit.application import get_app 30 31@Condition 32def statement_ended(): 33 t = get_app().current_buffer.text 34 return re.search("(;|^)\s*$",t) or re.search("(^|\n)(QED|End)\s*$",t) 35 36bindings = KeyBindings() 37 38@bindings.add( 39 "enter", 40 filter=statement_ended, 41) 42def _(event): 43 event.current_buffer.validate_and_handle() 44 45def main(argv): 46 args =" ".join(argv[1:]) # this should be hol and flags for hol 47 repl = pexpect.spawn(args, encoding='utf-8', echo=False, timeout=None) 48 49 def find_prompt(): 50 # searches the output of hol for a prompt ">" 51 return repl.expect_list(map(re.compile,["(\s+|^)>\s*$"]))#,"#\s*$"])) 52 53 find_prompt() 54 print(repl.before) # prints everything read from stout until the prompt 55 repl.sendline("Parse.current_backend := PPBackEnd.vt100_terminal;") 56 # for coloured hol terms TODO: make config option 57 find_prompt() 58 59 session = PromptSession("> ", 60 lexer=PygmentsLexer(SMLLexer), 61 history=FileHistory('.holwrap_history'), 62 auto_suggest=AutoSuggestFromHistory(), 63 multiline=True, # TODO make config option 64 key_bindings=bindings # TODO add some useful keybindings? 65 ) 66 67 while True: 68 try: 69 with patch_stdout(): 70 # prompt for input 71 text = session.prompt() 72 if text and text != "\n": 73 repl.sendline(text.strip()) 74 # send input to hol 75 find_prompt() 76 print(repl.before) # print output after finding next prompt 77 except pexpect.EOF: 78 break # quit 79 except EOFError: 80 break # quit 81 except KeyboardInterrupt: 82 repl.sendcontrol('c') 83 find_prompt() 84 print(repl.before) 85 continue 86 except pexpect.TIMEOUT: 87 # Timeout currently not set, this shouldn't happen unless changed 88 repl.sendcontrol('c') 89 print("Timeout reached") 90 find_prompt() 91 print(repl.before) 92 continue 93 repl.close(True) # close hol before exit 94 95if __name__ == "__main__": 96 main(sys.argv) 97