fix: block on parse error

We create a Block type in the scheduler (and its corresponding PBlock
in execution manager) which will send an exec_error if one tries to execute
through a parse error. If the user has set block_on_error mode then the behaviour
is now identical with parsing errors and execution errors.

Author: rtetley

language-server/dm/document.ml

@@ -59,7 +59,7 @@ type comment = {
 type parsing_error = {
   start: int;
   stop: int;
-  msg: string Loc.located;
+  msg: Pp.t Loc.located;
   qf: Quickfix.t list option;
 }
 
@@ -248,7 +248,8 @@ let add_sentence parsed parsing_start start stop (ast: sentence_state) synterp_s
   let id = Stateid.fresh () in
   let scheduler_state_after, schedule = 
     match ast with
-    | Error _ -> scheduler_state_before, parsed.schedule (* If the sentence has a parsing error we do not schedule it *)
+    | Error {msg} ->
+      scheduler_state_before, Scheduler.schedule_errored_sentence id msg parsed.schedule
     | Parsed ast ->
       let ast' = (ast.ast, ast.classification, synterp_state) in
       Scheduler.schedule_sentence (id, ast') scheduler_state_before parsed.schedule
@@ -397,7 +398,8 @@ let patch_sentence parsed scheduler_state_before id ({ parsing_start; ast; start
   log @@ Format.sprintf "Patching sentence %s , %s" (Stateid.to_string id) (string_of_parsed_ast old_sentence.ast);
   let scheduler_state_after, schedule =
     match ast with
-    | Error _ -> scheduler_state_before, parsed.schedule
+    | Error {msg} ->
+      scheduler_state_before, Scheduler.schedule_errored_sentence id msg parsed.schedule
     | Parsed ast ->
       let ast = (ast.ast, ast.classification, synterp_state) in
       Scheduler.schedule_sentence (id,ast) scheduler_state_before parsed.schedule
@@ -531,11 +533,10 @@ let get_entry ast =
 [%%endif]
 
 
-let handle_parse_error start parsing_start msg qf ({stream; errors; parsed} as parse_state) =
+let handle_parse_error start parsing_start msg qf ({stream; errors; parsed;} as parse_state) synterp_state =
   log @@ "handling parse error at " ^ string_of_int start;
   let stop = Stream.count stream in
   let parsing_error = { msg; start; stop; qf} in
-  let synterp_state = Vernacstate.Synterp.freeze () in
   let sentence = { parsing_start; ast = Error parsing_error; start; stop; synterp_state } in
   let parsed = sentence :: parsed in
   let errors = parsing_error :: errors in
@@ -579,24 +580,26 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
           let e, info = Exninfo.capture exn in
           let loc = get_loc_from_info_or_exn e info in
           let qf = Result.value ~default:[] @@ Quickfix.from_exception e in
-          handle_parse_error start begin_char (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) parse_state
+          handle_parse_error start begin_char (loc, CErrors.iprint_no_report (e,info)) (Some qf) parse_state synterp_state
         end
-    | exception (E msg as exn) ->
-      let loc = Loc.get_loc @@ Exninfo.info exn in
-      let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
+    | exception (E _ as exn) ->
+      let e, info = Exninfo.capture exn in
+      let loc = get_loc_from_info_or_exn e info in
+      let qf = Result.value ~default:[] @@ Quickfix.from_exception e in
       junk_sentence_end stream;
-      handle_parse_error start start (loc,msg) (Some qf) {parse_state with stream}
-    | exception (CLexer.Error.E e as exn) -> (* May be more problematic to handle for the diff *)
-      let loc = Loc.get_loc @@ Exninfo.info exn in
+      handle_parse_error start start (loc, CErrors.iprint_no_report (e, info)) (Some qf) {parse_state with stream} synterp_state
+    | exception (CLexer.Error.E _ as exn) -> (* May be more problematic to handle for the diff *)
+      let e, info = Exninfo.capture exn in
+      let loc = get_loc_from_info_or_exn e info in
       let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
       junk_sentence_end stream;
-      handle_parse_error start start (loc,CLexer.Error.to_string e) (Some qf) {parse_state with stream}
+      handle_parse_error start start (loc,CErrors.iprint_no_report (e, info)) (Some qf) {parse_state with stream} synterp_state
     | exception exn ->
       let e, info = Exninfo.capture exn in
       let loc = Loc.get_loc @@ info in
       let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in
       junk_sentence_end stream;
-      handle_parse_error start start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) {parse_state with stream}
+      handle_parse_error start start (loc, CErrors.iprint_no_report (e,info)) (Some qf) {parse_state with stream} synterp_state
   end
 
 let rec unchanged_id id = function
@@ -726,9 +729,9 @@ module Internal = struct
     sentence.stop
 
   let string_of_error error =
-    let (_, str) = error.msg in
+    let (_, pp) = error.msg in
     Format.sprintf "[parsing error] [%s] (%i -> %i)"
-    str
+    (Pp.string_of_ppcmds pp)
     error.start
     error.stop
 

language-server/dm/document.mli

@@ -84,7 +84,7 @@ type parsed_ast = {
 type parsing_error = {
   start: int; 
   stop: int; 
-  msg: string Loc.located;
+  msg: Pp.t Loc.located;
   qf: Quickfix.t list option;
 }
 

language-server/dm/documentManager.ml

@@ -226,7 +226,7 @@ let mk_parsing_error_diag st Document.{ msg = (oloc,msg); start; stop; qf } =
         in
       Some code
   in
-  make_diagnostic st.document range oloc msg severity code
+  make_diagnostic st.document range oloc (Pp.string_of_ppcmds msg) severity code
 
 let all_diagnostics st =
   let parse_errors = Document.parse_errors st.document in

language-server/dm/executionManager.ml

@@ -78,6 +78,7 @@ type delegated_task = {
 
 type prepared_task =
   | PSkip of { id: sentence_id; error: Pp.t option }
+  | PBlock of { id: sentence_id; error: Pp.t Loc.located }
   | PExec of executable_sentence
   | PQuery of executable_sentence
   | PDelegate of delegated_task
@@ -268,7 +269,7 @@ let interp_qed_delayed ~proof_using ~state_id ~st =
 let cut_overview task state document =
   let range = match task with
   | PDelegate { terminator_id } -> Document.range_of_id_with_blank_space document terminator_id
-  | PSkip { id } | PExec { id } | PQuery { id } ->
+  | PSkip { id } | PExec { id } | PQuery { id } | PBlock { id } ->
     Document.range_of_id_with_blank_space document id
   in
   let {prepared; processing; processed} = state.overview in
@@ -325,7 +326,7 @@ let update_processing task state document =
     let prepared = RangeList.remove_or_truncate_range range prepared in
     let overview = {state.overview with prepared; processing} in
     {state with overview}
-  | PSkip { id } | PExec { id } | PQuery { id } ->
+  | PSkip { id } | PExec { id } | PQuery { id } | PBlock { id } ->
     let range = Document.range_of_id_with_blank_space document id in
     let processing = RangeList.insert_or_merge_range range processing in
     let prepared = RangeList.remove_or_truncate_range range prepared in
@@ -345,7 +346,7 @@ let update_prepared task document state =
     let prepared = List.append prepared [ range ] in
     let overview = {state.overview with prepared} in
     {state with overview}
-  | PSkip { id } | PExec { id } | PQuery { id } ->
+  | PSkip { id } | PExec { id } | PQuery { id } | PBlock { id } ->
     let range = Document.range_of_id_with_blank_space document id in
     let prepared = RangeList.insert_or_merge_range range prepared in
     let overview = {state.overview with prepared} in
@@ -361,7 +362,7 @@ let update_overview task state document =
     let overview = update_processed_as_Done (Success None) range state.overview in
     let overview = {overview with prepared} in
     {state with overview}
-  | PSkip { id } | PExec { id } | PQuery { id } ->
+  | PSkip { id } | PExec { id } | PQuery { id } | PBlock { id } ->
     update_processed id state document
   in
   match state.todo with
@@ -507,6 +508,7 @@ let last_opt l = try Some (CList.last l).id with Failure _ -> None
 let prepare_task task : prepared_task list =
   match task with
   | Skip { id; error } -> [PSkip { id; error }]
+  | Block { id; error } -> [PBlock {id; error}]
   | Exec e -> [PExec e]
   | Query e -> [PQuery e]
   | OpaqueProof { terminator; opener_id; tasks; proof_using} ->
@@ -524,6 +526,7 @@ let prepare_task task : prepared_task list =
 
 let id_of_prepared_task = function
   | PSkip { id } -> id
+  | PBlock { id } -> id
   | PExec ex -> ex.id
   | PQuery ex -> ex.id
   | PDelegate { terminator_id } -> terminator_id
@@ -582,6 +585,12 @@ let execute_task st (vs, events, interrupted) task =
   end else
     try
       match task with
+      | PBlock { id; error = err} ->
+        let (loc, pp) = err in
+        let v = error None None pp vs in
+        let parse_error = Some (id, loc) in
+        let st = update st id v in
+        (st, vs, events, false, parse_error)
       | PSkip { id; error = err } ->
           let v = match err with
             | None -> success vs
@@ -804,7 +813,7 @@ let invalidate1 of_sentence id =
 
 let cancel1 todo invalid_id =
   let task_of_id = function
-    | PSkip { id } | PExec { id } | PQuery { id } -> Stateid.equal id invalid_id
+    | PSkip { id } | PExec { id } | PQuery { id } | PBlock { id } -> Stateid.equal id invalid_id
     | PDelegate _ -> false
   in
   List.filter task_of_id todo

language-server/dm/scheduler.ml

@@ -32,6 +32,7 @@ type executable_sentence = {
 
 type task =
   | Skip of { id: sentence_id; error: Pp.t option }
+  | Block of { id: sentence_id; error: Pp.t Loc.located }
   | Exec of executable_sentence
   | OpaqueProof of { terminator: executable_sentence;
                      opener_id: sentence_id;
@@ -214,13 +215,19 @@ let string_of_task (task_id,(base_id,task)) =
   | Exec { id } -> Format.sprintf "Exec %s" (Stateid.to_string id)
   | OpaqueProof { terminator; tasks } -> Format.sprintf "OpaqueProof [%s | %s]" (Stateid.to_string terminator.id) (String.concat "," (List.map (fun task -> Stateid.to_string task.id) tasks))
   | Query { id } -> Format.sprintf "Query %s" (Stateid.to_string id)
+  | Block { id } -> Format.sprintf "Block %s" (Stateid.to_string id)
   in
   Format.sprintf "[%s] : [%s] -> %s" (Stateid.to_string task_id) (Option.cata Stateid.to_string "init" base_id) s
 
 let _string_of_state st =
   let scopes = (List.map (fun b -> List.map (fun x -> x.id) b.proof_sentences) st.proof_blocks) @ [st.document_scope] in
   String.concat "|" (List.map (fun l -> String.concat " " (List.map Stateid.to_string l)) scopes)
 
+let schedule_errored_sentence id error schedule =
+  let task = Block {id; error} in
+  let tasks = SM.add id (None, task) schedule.tasks in
+  {schedule with tasks}
+
 let schedule_sentence (id, (ast, classif, synterp_st)) st schedule =
   let base, st, task = 
       let open Vernacexpr in

language-server/dm/scheduler.mli

@@ -37,6 +37,7 @@ type executable_sentence = {
 
 type task =
   | Skip of { id: sentence_id; error: Pp.t option }
+  | Block of { id: sentence_id; error: Pp.t Loc.located }
   | Exec of executable_sentence
   | OpaqueProof of { terminator: executable_sentence;
                      opener_id: sentence_id;
@@ -51,6 +52,8 @@ type schedule
 
 val initial_schedule : schedule
 
+val schedule_errored_sentence : sentence_id -> Pp.t Loc.located -> schedule -> schedule
+
 val schedule_sentence : sentence_id * (Synterp.vernac_control_entry * Vernacextend.vernac_classification * Vernacstate.Synterp.t) -> state -> schedule -> state * schedule
 (** Identifies the structure of the document and dependencies between sentences
     in order to easily compute the tasks to interpret the a sentence.