vscode-ocaml-platform

vscode-ocaml-platform copied to clipboard

This patch highlights the background of the statement that was sent to REPL.

To set the color, ocaml.repl.evalTextBackgroundColor is newly added as a configuration.

Modifying any character in the editor before or in the selected region will remove the highlighted background.

ping

Hi, thanks for your comments! I could not manage to find a time for addressing your comments today. I will reflect them tomorrow.

Hi, sorry for my delay. I reflected the comments so far.

Could you please add a change log entry?

Frankly, I'm not sure it's useful to color the background for the current behavior of the REPL since the text sent is based either on the selection which is already colored or the current line if selection is empty. The sent text is also visible in the REPL. Do you have cases when such background would be useful?

Yes, I felt this feature was necessary when I was evaluating the text in REPL which is taking a long time. While the text is evaluating, I cannot unselect the text and edit the .ml program because it makes me lose which text I was evaluating before. Evaluating the sent text typically prints lots of information to show the progress on REPL, hiding the latest sentence that was evaluated.

Specifically, I am using vscode-ocaml-platform to write an OCaml program that uses HOL Light (https://github.com/jrh13/hol-light/). OCaml programmer can use HOL Light to define a mathematical theorem and prove it step-by-step. An HOL Light program is supposed to run on OCaml REPL rather than compile it as a binary because the user needs to interact with the proof state after each step. This is computation intensive, and evaluating one sentence can easily take several minutes. Therefore evaluating a sentence and writing a code in parallel is important for saving time. It is also important to not lose which statement I had executed before.

An Emacs plugin called ProofGeneral has a similar feature. It is an editor for a language called Coq, which is similar to OCaml but for more mathematical purpose. https://www.youtube.com/watch?v=l6zqLJQCnzo shows how the evaluated text is colored as blue. A small difference between this plug in and our case is that it highlights the text up from the very beginning of the file, but this is because in ProofGeneral a program must be sequentially evaluated.

Since this mode isn't enabled by default, I feel there's not much risk in accepting this PR. It doesn't seem like it will add much maintenance overhead or bugs.

EDIT: I misread, only the color is configurable. Can you make this feature off by default and enabled via an option? That way we can merge it and continue the discussion about UX.