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