diff options
| -rw-r--r-- | Biz/Repl.py | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/Biz/Repl.py b/Biz/Repl.py index cb9dfe7..2f71c33 100644 --- a/Biz/Repl.py +++ b/Biz/Repl.py @@ -18,6 +18,7 @@ import importlib import importlib.util import logging import os +import subprocess import sys import mypy.api @@ -59,13 +60,31 @@ def typecheck(path: str) -> None: sys.stderr.flush() +def edit_file(ns: str, path: str, editor: str) -> None: + """ + Edit and reload the given namespace and path. + + It is assumed ns and path go together. If `editor` returns something other + than 0, this function will not reload the ns. + """ + try: + proc = subprocess.run([editor, path], check=False) + except FileNotFoundError: + Log.fail("editor '%s' not found", editor) + if proc.returncode == 0: + use(ns, path) + typecheck(path) + + if __name__ == "__main__": Log.setup() NS = sys.argv[1] PATH = sys.argv[2] + EDITOR = os.environ.get("EDITOR", "$EDITOR") use(NS, PATH) typecheck(PATH) + logging.info("use edit() to open %s in %s", NS, EDITOR) logging.info("use reload() after making changes") sys.ps1 = f"{NS}> " sys.ps2 = f"{NS}| " @@ -74,3 +93,7 @@ if __name__ == "__main__": """Reload the namespace.""" use(NS, PATH) typecheck(PATH) + + def edit() -> None: + """Edit the current namespace.""" + edit_file(NS, PATH, EDITOR) |