Support block on first error mode #845
Conversation
| val build_tasks_for : Document.document -> Scheduler.schedule -> state -> sentence_id -> Vernacstate.t * prepared_task list * state | ||
| val execute : state -> Vernacstate.t * events * bool -> prepared_task -> (state * Vernacstate.t * events * bool) | ||
| val build_tasks_for : Document.document -> Scheduler.schedule -> state -> sentence_id -> bool -> Vernacstate.t * prepared_task list * state * sentence_id option | ||
| val execute : state -> Vernacstate.t * events * bool -> prepared_task -> (state * Vernacstate.t * events * bool * bool) |
There was a problem hiding this comment.
maybe it is time to name these booleans ;-)
|
If you give a name to the type range.t option, eg blocking_error, then the api update are are self explanatory |
rtetley
force-pushed
the
block-on-first-error
branch
from
e566624 to
d6682d1
Compare
| @@ -101,7 +103,7 @@ val get_proof : state -> Settings.Goals.Diff.Mode.t -> Position.t option -> Proo | |||
|
|
|||
| val get_completions : state -> Position.t -> (completion_item list, string) Result.t | |||
|
|
|||
| val handle_event : event -> state -> (state option * events) | |||
| val handle_event : event -> state -> bool -> (state option * events * Range.t option) | |||
There was a problem hiding this comment.
TODO: doc the bool and return type
| "vscoq.proof.block": { | ||
| "scope": "window", | ||
| "type": "boolean", | ||
| "default": true, |
There was a problem hiding this comment.
This is a behavior change, better be advertised in the changelog/news
There was a problem hiding this comment.
Should I change it to false by default maybe ?
There was a problem hiding this comment.
I really don't know. Probably the new default is less surprising.
One thing I'd like to change is that, even if it is off, going down 1 sentence blocks. But I got used to that from the CoqIDE days, so I don't know it it is just me. I mean: if I say go there, and there is far away, I really want to go there. If I want to execute the next sentence, and if it fails, I want to stay where I am. So to me ALT-down should have the ~should_block_on_error:true always, while ALT-right should read the value from the settings.
There was a problem hiding this comment.
I thought a bit more about my use case, and maybe also the one of Laurent. I think moving the caret in case of a failing step forward is bad, it really seems step fwd is special.
There was a problem hiding this comment.
Okay ! Just changed it
There was a problem hiding this comment.
Now I don't don't have the time to test it, but IIRC on block on error you both stop and move the caret back.
The last part should not happen when step forward fails.
Here I use | for the caret when I do a step fwd (ALT-down).
1) rewrite foo.| (* fails, damn, I move back to fix the rule *)
2) rewrite {2}|foo. (* fails again *)
3) rewrite {2 3|}foo. (* works *)
I'd like the caret to stay where it is when 2 fails, but move after the . when 3 works.
I think step fwd is special since you use it when you "refine" a command, and you may do it with the caret in the middle of it. So moving the caret elsewhere, like at the previous ., is just going to piss the user off.
There was a problem hiding this comment.
So if I understand correctly, the caret should not move at all on step forward when there is an error?
… blocking on error
rtetley
force-pushed
the
block-on-first-error
branch
from
3404078 to
4b04c29
Compare
rtetley
force-pushed
the
block-on-first-error
branch
from
d8a88fa to
a417bba
Compare
Closes #537