Cleaned up commands and styling
parent
d11c9a5a7e
commit
0ef0e8e585
GPG Key ID:
AD62BB059C2AAEE4
|
|
@ -7,6 +7,7 @@
|
|||
- Prettyprint functions (combine args, rename bound variables)
|
||||
- Write a nice README
|
||||
- Handle or avoid recursion errors
|
||||
- Fix colors
|
||||
|
||||
## Todo:
|
||||
- live syntax check
|
||||
|
|
|
|||
|
|
@ -22,8 +22,9 @@ def _(event):
|
|||
|
||||
session = PromptSession(
|
||||
message = FormattedText([
|
||||
("#00FFFF", "~~> ")
|
||||
("class:prompt", "~~> ")
|
||||
]),
|
||||
style = utils.style,
|
||||
key_bindings = bindings
|
||||
)
|
||||
|
||||
|
|
@ -74,44 +75,42 @@ while True:
|
|||
except ppx.ParseException as e:
|
||||
l = len(to_plain_text(session.message))
|
||||
printf(FormattedText([
|
||||
("#FF0000", " "*(e.loc + l) + "^\n"),
|
||||
("#FF0000", f"Syntax error at char {e.loc}."),
|
||||
("#FFFFFF", "\n")
|
||||
("class:err", " "*(e.loc + l) + "^\n"),
|
||||
("class:err", f"Syntax error at char {e.loc}."),
|
||||
("class:text", "\n")
|
||||
]))
|
||||
continue
|
||||
except tokens.ReductionError as e:
|
||||
printf(FormattedText([
|
||||
("#FF0000", f"{e.msg}"),
|
||||
("#FFFFFF", "\n")
|
||||
]))
|
||||
("class:err", f"{e.msg}\n")
|
||||
]), style = utils.style)
|
||||
continue
|
||||
|
||||
# If this line defined a macro, print nothing.
|
||||
if isinstance(x, rs.MacroStatus):
|
||||
printf(FormattedText([
|
||||
("#FFFFFF", "Set "),
|
||||
("#FF00FF", x.macro_label),
|
||||
("#FFFFFF", " to "),
|
||||
("#FFFFFF", str(x.macro_expr))
|
||||
]))
|
||||
("class:text", "Set "),
|
||||
("class:syn_macro", x.macro_label),
|
||||
("class:text", " to "),
|
||||
("class:text", str(x.macro_expr))
|
||||
]), style = utils.style)
|
||||
|
||||
|
||||
if isinstance(x, rs.CommandStatus):
|
||||
printf(x.formatted_text)
|
||||
printf(x.formatted_text, style = utils.style)
|
||||
|
||||
# If this line was an expression, print reduction status
|
||||
elif isinstance(x, rs.ReduceStatus):
|
||||
printf(FormattedText([
|
||||
|
||||
("#00FF00 bold", f"\nExit reason: "),
|
||||
("class:result_header", f"\nExit reason: "),
|
||||
x.stop_reason.value,
|
||||
|
||||
("#00FF00 bold", f"\nReduction count: "),
|
||||
("#FFFFFF", str(x.reduction_count)),
|
||||
("class:result_header", f"\nReduction count: "),
|
||||
("class:text", str(x.reduction_count)),
|
||||
|
||||
|
||||
("#00FF00 bold", "\n\n => "),
|
||||
("#FFFFFF", str(x.result)),
|
||||
]))
|
||||
("class:result_header", "\n\n => "),
|
||||
("class:text", str(x.result)),
|
||||
]), style = utils.style)
|
||||
|
||||
printf("")
|
||||
|
|
|
|||
|
|
@ -17,6 +17,13 @@ def lamb_command(*, help_text: str):
|
|||
return inner
|
||||
|
||||
def run(command, runner):
|
||||
if command.name not in commands:
|
||||
return CommandStatus(
|
||||
formatted_text = FormattedText([
|
||||
("class:warn", f"Unknown command \"{command.name}\"")
|
||||
])
|
||||
)
|
||||
else:
|
||||
return commands[command.name](command, runner)
|
||||
|
||||
@lamb_command(help_text = "Delete a macro")
|
||||
|
|
@ -24,7 +31,7 @@ def mdel(command, runner):
|
|||
if len(command.args) != 1:
|
||||
return CommandStatus(
|
||||
formatted_text = HTML(
|
||||
"<red>Command <grey>:mdel</grey> takes exactly one argument.</red>"
|
||||
"<warn>Command <cmd_code>:mdel</cmd_code> takes exactly one argument.</warn>"
|
||||
)
|
||||
)
|
||||
|
||||
|
|
@ -32,7 +39,7 @@ def mdel(command, runner):
|
|||
if target not in runner.macro_table:
|
||||
return CommandStatus(
|
||||
formatted_text = HTML(
|
||||
f"<red>Macro \"{target}\" is not defined</red>"
|
||||
f"<warn>Macro \"{target}\" is not defined</warn>"
|
||||
)
|
||||
)
|
||||
|
||||
|
|
@ -41,11 +48,13 @@ def mdel(command, runner):
|
|||
@lamb_command(help_text = "Show macros")
|
||||
def macros(command, runner):
|
||||
return CommandStatus(
|
||||
|
||||
# Can't use HTML here, certain characters might break it.
|
||||
formatted_text = FormattedText([
|
||||
("#FF6600 bold", "\nDefined Macros:\n"),
|
||||
("class:cmd_h", "\nDefined Macros:\n"),
|
||||
] +
|
||||
[
|
||||
("#FFFFFF", f"\t{name} \t {exp}\n")
|
||||
("class:cmd_text", f"\t{name} \t {exp}\n")
|
||||
for name, exp in runner.macro_table.items()
|
||||
]
|
||||
)
|
||||
|
|
@ -60,56 +69,22 @@ def clear(command, runner):
|
|||
@lamb_command(help_text = "Print this help")
|
||||
def help(command, runner):
|
||||
return CommandStatus(
|
||||
formatted_text = FormattedText([
|
||||
("#FF6600 bold", "\nUsage:\n"),
|
||||
(
|
||||
"#FFFFFF",
|
||||
"\tWrite lambda expressions using your "
|
||||
),
|
||||
(
|
||||
"#00FF00",
|
||||
"\\"
|
||||
),
|
||||
(
|
||||
"#FFFFFF",
|
||||
" key.\n" +
|
||||
"\tMacros can be defined using "
|
||||
),
|
||||
|
||||
|
||||
("#00FF00", "="),
|
||||
(
|
||||
"#FFFFFF",
|
||||
", as in "
|
||||
),
|
||||
(
|
||||
"#AAAAAA bold",
|
||||
"T = λab.a\n"
|
||||
),
|
||||
|
||||
|
||||
(
|
||||
"#FFFFFF",
|
||||
"\tRun commands using "
|
||||
),
|
||||
(
|
||||
"#00FF00",
|
||||
":"
|
||||
),
|
||||
(
|
||||
"#FFFFFF",
|
||||
", for example "
|
||||
),
|
||||
(
|
||||
"#AAAAAA bold",
|
||||
":help"
|
||||
),
|
||||
|
||||
("#FF6600 bold", "\n\nCommands:\n")
|
||||
] +
|
||||
[
|
||||
("#FFFFFF", f"\t{name} \t {text}\n")
|
||||
formatted_text = HTML(
|
||||
"\n<cmd_text>" +
|
||||
"<cmd_h>Usage:</cmd_h>" +
|
||||
"\n" +
|
||||
"\tWrite lambda expressions using your <cmd_key>\\</cmd_key> key." +
|
||||
"\n" +
|
||||
"\tMacros can be defined using <cmd_key>=</cmd_key>, as in <cmd_code>T = λab.a</cmd_code>" +
|
||||
"\n" +
|
||||
"\tRun commands using <cmd_key>:</cmd_key>, for example <cmd_code>:help</cmd_code>" +
|
||||
"\n\n" +
|
||||
"<cmd_h>Commands:</cmd_h>"+
|
||||
"\n" +
|
||||
"\n".join([
|
||||
f"\t{name} \t {text}"
|
||||
for name, text in help_texts.items()
|
||||
]
|
||||
]) +
|
||||
"</cmd_text>"
|
||||
)
|
||||
)
|
||||
|
|
@ -16,18 +16,6 @@ class Runner:
|
|||
# If None, no maximum is enforced.
|
||||
self.reduction_limit: int | None = 300
|
||||
|
||||
def exec_command(self, command: tokens.command) -> rs.CommandStatus:
|
||||
if command.name in commands.commands:
|
||||
return commands.run(command, self)
|
||||
|
||||
# Handle unknown commands
|
||||
else:
|
||||
return rs.CommandStatus(
|
||||
formatted_text = FormattedText([
|
||||
("#FFFF00", f"Unknown command \"{command}\"")
|
||||
])
|
||||
)
|
||||
|
||||
|
||||
def reduce_expression(self, expr: tokens.LambdaToken) -> rs.ReduceStatus:
|
||||
|
||||
|
|
@ -81,7 +69,7 @@ class Runner:
|
|||
|
||||
# If this line is a command, do the command.
|
||||
elif isinstance(e, tokens.command):
|
||||
return self.exec_command(e)
|
||||
return commands.run(e, self)
|
||||
|
||||
# If this line is a plain expression, reduce it.
|
||||
elif isinstance(e, tokens.LambdaToken):
|
||||
|
|
|
|||
|
|
@ -1,4 +1,5 @@
|
|||
from prompt_toolkit.formatted_text import FormattedText
|
||||
from prompt_toolkit.formatted_text import HTML
|
||||
import enum
|
||||
|
||||
import lamb.tokens as tokens
|
||||
|
|
@ -33,10 +34,10 @@ class MacroStatus(RunStatus):
|
|||
|
||||
|
||||
class StopReason(enum.Enum):
|
||||
BETA_NORMAL = ("#FFFFFF", "β-normal form")
|
||||
LOOP_DETECTED = ("#FFFF00", "loop detected")
|
||||
MAX_EXCEEDED = ("#FFFF00", "too many reductions")
|
||||
INTERRUPT = ("#FF0000", "user interrupt")
|
||||
BETA_NORMAL = ("class:text", "β-normal form")
|
||||
LOOP_DETECTED = ("class:warn", "loop detected")
|
||||
MAX_EXCEEDED = ("class:err", "too many reductions")
|
||||
INTERRUPT = ("class:warn", "user interrupt")
|
||||
|
||||
|
||||
class ReduceStatus(RunStatus):
|
||||
|
|
@ -71,6 +72,6 @@ class CommandStatus(RunStatus):
|
|||
def __init__(
|
||||
self,
|
||||
*,
|
||||
formatted_text: FormattedText
|
||||
formatted_text: FormattedText | HTML
|
||||
):
|
||||
self.formatted_text = formatted_text
|
||||
|
|
@ -30,6 +30,38 @@ def autochurch(results):
|
|||
)
|
||||
|
||||
|
||||
style = Style.from_dict({
|
||||
# Basic formatting
|
||||
"text": "#FFFFFF",
|
||||
"warn": "#FFFF00",
|
||||
"err": "#FF0000",
|
||||
"prompt": "#00FFFF",
|
||||
|
||||
# Syntax
|
||||
"syn_macro": "#FF00FF",
|
||||
"syn_lambda": "#FF00FF",
|
||||
"syn_bound": "#FF00FF",
|
||||
|
||||
# Titles for reduction results
|
||||
"result_header": "#B4EC85 bold",
|
||||
|
||||
# Command formatting
|
||||
# cmd_h: section titles
|
||||
# cmd_code: example snippets
|
||||
# cmd_text: regular text
|
||||
# cmd_key: keyboard keys, usually one character
|
||||
"cmd_h": "#FF6600 bold",
|
||||
"cmd_code": "#AAAAAA italic",
|
||||
"cmd_text": "#FFFFFF",
|
||||
"cmd_key": "#B4EC85 bold",
|
||||
|
||||
# Only used in greeting
|
||||
"_v": "#B4EC85 bold",
|
||||
"_l": "#FF6600 bold",
|
||||
"_s": "#B4EC85 bold",
|
||||
"_p": "#AAAAAA"
|
||||
})
|
||||
|
||||
|
||||
def show_greeting():
|
||||
# | _.._ _.|_
|
||||
|
|
@ -62,19 +94,4 @@ def show_greeting():
|
|||
"<_s> A λ calculus engine</_s>",
|
||||
"<_p> Type :help for help</_p>",
|
||||
""
|
||||
])), style = Style.from_dict({
|
||||
# Heading
|
||||
"_h": "#FFFFFF bold",
|
||||
|
||||
# Version
|
||||
"_v": "#B4EC85 bold",
|
||||
|
||||
# Lambda
|
||||
"_l": "#FF6600 bold",
|
||||
|
||||
# Subtitle
|
||||
"_s": "#B4EC85 bold",
|
||||
|
||||
# :help message
|
||||
"_p": "#AAAAAA"
|
||||
}))
|
||||
])), style = style)
|
||||
Reference in New Issue