Replies: 1 comment
-
Let me write a patch for this in my spare time. |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
Hi,
When I want to run a selected text in REPL, sometimes I cannot use "Evaluate Selection" because the text must be properly preprocessed somehow.
For example, in an application called HOL Light, I often want to evaluate some selected expression
expr
in a function callede
so that the actual sentence I want to run in REPL ise(expr);;
.Would it be a good idea if there is a new command, say "Evaluate Selection Using Custom Preprocessor", that runs a user-specified Javascript file on the input and runs its output (which is the preprocessed text) in REPL?
Beta Was this translation helpful? Give feedback.
All reactions