2

I want to prepend a line to a snippet already entered in the REPL. The screenshot shows the cursor at the point that the newline should be inserted.

enter image description here

I do not know how to do this since hitting return will try to execute the snippet. I also tried CMD-Ret and Alt-Ret: same behavior. Is there any way to do this without retyping the entire snippet?

2
  • Try Control-V, Control-J
    – Martin R
    Jun 29, 2020 at 17:14
  • @MartinR v nice! where did you learn that one (I'd like to see what other goodies are there) . Pls make an answer Jun 29, 2020 at 17:20

1 Answer 1

2

Control-V, Control-J does does the trick, similarly as in an interactive terminal. Control-V means "the next character should be treated literally" and Control-J generates a newline character.

1
  • That's a great answer: it is well more generally useful than what I was asking! One sometimes proves theorems more general than the specific condition. Jun 29, 2020 at 17:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.