Block on parse error

language-server/dm/document.ml

@@ -50,12 +50,29 @@ type parsed_ast = {
   tokens: Tok.t list
 }
 
+type comment = {
+  start: int;
+  stop: int;
+  content: string;
+}
+
+type parsing_error = {
+  start: int;
+  stop: int;
+  msg: Pp.t Loc.located;
+  qf: Quickfix.t list option;
+}
+
+type sentence_state =
+  | Error of parsing_error
+  | Parsed of parsed_ast
+
 type pre_sentence = {
   parsing_start : int;
   start : int;
   stop : int;
   synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *)
-  ast : parsed_ast;
+  ast : sentence_state;
 }
 
 (* Example:                        *)
@@ -70,23 +87,10 @@ type sentence = {
   synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *)
   scheduler_state_before : Scheduler.state;
   scheduler_state_after : Scheduler.state;
-  ast : parsed_ast;
+  ast : sentence_state;
   id : sentence_id;
 }
 
-type comment = {
-  start: int;
-  stop: int;
-  content: string;
-}
-
-type parsing_error = {
-  start: int;
-  stop: int;
-  msg: string Loc.located;
-  qf: Quickfix.t list option;
-}
-
 type document = {
   sentences_by_id : sentence SM.t;
   sentences_by_end : sentence LM.t;
@@ -223,8 +227,13 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out
     end
   | _ -> outline
 
+let record_outline document {id; ast} outline =
+  match ast with
+  | Error _ -> outline
+  | Parsed ast -> record_outline document id ast.ast ast.classification outline
+
 let compute_outline ({ sentences_by_end } as document) =
-    LM.fold (fun _ {id; ast} -> record_outline document id ast.ast ast.classification) sentences_by_end []
+    LM.fold (fun _ s -> record_outline document s) sentences_by_end []
 
 
 let schedule doc = doc.schedule
@@ -235,11 +244,15 @@ let outline doc = doc.outline
 let parse_errors parsed =
   List.map snd (LM.bindings parsed.parsing_errors_by_end)
 
-let add_sentence parsed parsing_start start stop (ast: parsed_ast) synterp_state scheduler_state_before =
+let add_sentence parsed parsing_start start stop (ast: sentence_state) synterp_state scheduler_state_before =
   let id = Stateid.fresh () in
-  let ast' = (ast.ast, ast.classification, synterp_state) in
-  let scheduler_state_after, schedule =
-    Scheduler.schedule_sentence (id, ast') scheduler_state_before parsed.schedule
+  let scheduler_state_after, schedule = 
+    match ast with
+    | 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
   in
   (* FIXME may invalidate scheduler_state_XXX for following sentences -> propagate? *)
   let sentence = { parsing_start; start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in
@@ -337,9 +350,12 @@ let find_next_qed parsed loc =
   let exception Found of sentence in
   let f k sentence =
     if loc <= k then
-    match sentence.ast.classification with
-    | VtQed _ -> raise (Found sentence)
-    | _ -> () in
+    match sentence.ast with
+    | Error _ -> ()
+    | Parsed ast ->
+    match ast.classification with
+      | VtQed _ -> raise (Found sentence)
+      | _ -> () in
   (* We can't use find_first since f isn't monotone *)
   match LM.iter f parsed.sentences_by_end with
   | () -> None
@@ -373,12 +389,20 @@ let string_of_parsed_ast { tokens } =
   (* TODO implement printer for vernac_entry *)
   "[" ^ String.concat "--" (List.map (Tok.extract_string false) tokens) ^ "]"
 
+let string_of_parsed_ast = function
+| Error _ -> "errored sentence"
+| Parsed ast -> string_of_parsed_ast ast
+
 let patch_sentence parsed scheduler_state_before id ({ parsing_start; ast; start; stop; synterp_state } : pre_sentence) =
   let old_sentence = SM.find id parsed.sentences_by_id in
   log @@ Format.sprintf "Patching sentence %s , %s" (Stateid.to_string id) (string_of_parsed_ast old_sentence.ast);
   let scheduler_state_after, schedule =
-    let ast = (ast.ast, ast.classification, synterp_state) in
-    Scheduler.schedule_sentence (id,ast) scheduler_state_before parsed.schedule
+    match ast with
+    | 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
   in
   let new_sentence = { old_sentence with ast; parsing_start; start; stop; scheduler_state_before; scheduler_state_after } in
   let sentences_by_id = SM.add id new_sentence parsed.sentences_by_id in
@@ -398,7 +422,11 @@ type diff =
 
 
 let same_tokens (s1 : sentence) (s2 : pre_sentence) =
-    CList.equal Tok.equal s1.ast.tokens s2.ast.tokens
+  match s1.ast, s2.ast with
+  | Error _, Error _ -> false
+  | Parsed ast1, Parsed ast2 ->
+    CList.equal Tok.equal ast1.tokens ast2.tokens
+  | _, _ -> false
 
 (* TODO improve diff strategy (insertions,etc) *)
 let rec diff old_sentences new_sentences =
@@ -505,12 +533,14 @@ let get_entry ast =
 [%%endif]
 
 
-let handle_parse_error start msg qf ({stream; errors;} 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 sentence = { parsing_start; ast = Error parsing_error; start; stop; synterp_state } in
+  let parsed = sentence :: parsed in
   let errors = parsing_error :: errors in
-  let parse_state = {parse_state with errors} in
+  let parse_state = {parse_state with errors; parsed} in
   (* TODO: we could count the \n between start and stop and increase Loc.line_nb *)
   create_parsing_event (ParseEvent parse_state)
 
@@ -538,7 +568,8 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
           let entry = get_entry ast in
           let classification = Vernac_classifier.classify_vernac ast in
           let synterp_state = Vernacstate.Synterp.freeze () in
-          let sentence = { parsing_start = start; ast = { ast = entry; classification; tokens }; start = begin_char; stop; synterp_state } in
+          let parsed_ast = Parsed { ast = entry; classification; tokens } in
+          let sentence = { parsing_start = start; ast = parsed_ast; start = begin_char; stop; synterp_state } in
           let parsed = sentence :: parsed in
           let comments = List.map (fun ((start, stop), content) -> {start; stop; content}) comments in
           let parsed_comments = List.append comments parsed_comments in
@@ -549,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 (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 (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 (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 (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
@@ -696,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;
 }
 
@@ -100,6 +100,10 @@ val apply_text_edits : document -> text_edit list -> document
 (** [apply_text_edits doc edits] updates the text of [doc] with [edits]. The new
     text is not parsed or executed. *)
 
+type sentence_state =
+  | Error of parsing_error
+  | Parsed of parsed_ast
+
 (* Example:                        *)
 (* "  Check 3. "                    *)
 (* ^  ^       ^---- end            *)
@@ -112,7 +116,7 @@ type sentence = {
   synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *)
   scheduler_state_before : Scheduler.state;
   scheduler_state_after : Scheduler.state;
-  ast : parsed_ast;
+  ast : sentence_state;
   id : sentence_id;
 }
 

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
@@ -770,11 +770,14 @@ let hover st pos =
     match hover_of_sentence st loc pattern opt with
     | Some _ as x -> x
     | None -> 
-    match sentence.ast.classification with
+    match sentence.ast with
+    | Error _ -> None
+    | Parsed ast -> 
+      match ast.classification with
     (* next sentence in proof mode, hover at qed *)
-    | VtProofStep _ | VtStartProof _ -> 
+      | VtProofStep _ | VtStartProof _ -> 
         hover_of_sentence st loc pattern (Document.find_next_qed st.document loc)
-    | _ -> None
+      | _ -> None
 
 [%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
   let lconstr = Pcoq.Constr.lconstr

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