Merge pull request #732 from coq-community/parse-errors

Fix parse errors and highlight zone

language-server/dm/document.ml

@@ -29,13 +29,20 @@ type 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;
 }
 
+(* Example:                        *)
+(* "  Check 3. "                   *)
+(* ^  ^       ^---- end            *)
+(* |  |------------ start          *)
+(* |---------------- parsing_start *)
 type sentence = {
+  parsing_start : int;
   start : int;
   stop : int;
   synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *)
@@ -70,22 +77,32 @@ let range_of_sentence raw (sentence : sentence) =
   let end_ = RawDocument.position_of_loc raw sentence.stop in
   Range.{ start; end_ }
 
+let range_of_sentence_with_blank_space raw (sentence : sentence) =
+  let start = RawDocument.position_of_loc raw sentence.parsing_start in
+  let end_ = RawDocument.position_of_loc raw sentence.stop in
+  Range.{ start; end_ }
+
 let range_of_id document id =
   match SM.find_opt id document.sentences_by_id with
   | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id)
   | Some sentence -> range_of_sentence document.raw_doc sentence
 
+let range_of_id_with_blank_space document id =
+  match SM.find_opt id document.sentences_by_id with
+  | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id)
+  | Some sentence -> range_of_sentence_with_blank_space document.raw_doc sentence
+
 let parse_errors parsed =
   List.map snd (LM.bindings parsed.parsing_errors_by_end)
 
-let add_sentence parsed start stop (ast: parsed_ast) synterp_state scheduler_state_before =
+let add_sentence parsed parsing_start start stop (ast: parsed_ast) 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
   in
   (* FIXME may invalidate scheduler_state_XXX for following sentences -> propagate? *)
-  let sentence = { start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in
+  let sentence = { parsing_start; start; stop; ast; id; synterp_state; scheduler_state_before; scheduler_state_after } in
   { parsed with sentences_by_end = LM.add stop sentence parsed.sentences_by_end;
     sentences_by_id = SM.add id sentence parsed.sentences_by_id;
     schedule
@@ -102,9 +119,36 @@ let remove_sentence parsed id =
 
 let sentences parsed =
   List.map snd @@ SM.bindings parsed.sentences_by_id
+
+type comment = {
+  start : int;
+  stop : int;
+}
+
+type code_line =
+  | Sentence of sentence
+  | ParsingError of parsing_error
+  | Comment of comment
+
+let start_of_code_line = function
+  | Sentence { start = x } -> x
+  | ParsingError  { start = x } -> x
+  | Comment { start = x } -> x
+
+let compare_code_line x y =
+  let s1 = start_of_code_line x in
+  let s2 = start_of_code_line y in
+  s1 - s2
+
+let code_lines_sorted_by_loc parsed =
+  List.sort compare_code_line @@ List.concat [
+    (List.map (fun (_,x) -> Sentence x) @@ SM.bindings parsed.sentences_by_id) ;
+    (List.map (fun (_,x) -> ParsingError x) @@ LM.bindings parsed.parsing_errors_by_end) ;
+    []  (* todo comments *)
+   ]
 
 let sentences_sorted_by_loc parsed =
-  List.sort (fun ({ start = s1 } : sentence) { start = s2 } -> s1 - s2) @@ List.map snd @@ SM.bindings parsed.sentences_by_id
+  List.sort (fun ({start = s1} : sentence) {start = s2} -> s1 - s2) @@ List.map snd @@ SM.bindings parsed.sentences_by_id
 
 let sentences_before parsed loc =
   let (before,ov,_after) = LM.split loc parsed.sentences_by_end in
@@ -178,14 +222,14 @@ let pos_at_end parsed =
   | Some (stop, _) -> stop
   | None -> -1
 
-let patch_sentence parsed scheduler_state_before id ({ ast; start; stop; synterp_state } : pre_sentence) =
+let patch_sentence parsed scheduler_state_before id ({ parsing_start; ast; start; stop; synterp_state } : pre_sentence) =
   log @@ "Patching sentence " ^ Stateid.to_string id;
   let old_sentence = SM.find id parsed.sentences_by_id in
   let scheduler_state_after, schedule =
     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; start; stop; scheduler_state_before; scheduler_state_after } 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
   let sentences_by_end = LM.remove old_sentence.stop parsed.sentences_by_end in
   let sentences_by_end = LM.add new_sentence.stop new_sentence sentences_by_end in
@@ -267,6 +311,7 @@ let rec parse_more synterp_state stream raw parsed errors =
     parse_more synterp_state stream raw parsed errors
   in
   let start = Stream.count stream in
+  log @@ "Start of parse is: " ^ (string_of_int start);
   begin
     (* FIXME should we save lexer state? *)
     match parse_one_sentence stream ~st:synterp_state with
@@ -288,7 +333,7 @@ let rec parse_more synterp_state stream raw parsed errors =
           let entry = Synterp.synterp_control ast in
           let classification = Vernac_classifier.classify_vernac ast in
           let synterp_state = Vernacstate.Synterp.freeze () in
-          let sentence = { ast = { ast = entry; classification; tokens }; start = begin_char; stop; synterp_state } in
+          let sentence = { parsing_start = start; ast = { ast = entry; classification; tokens }; start = begin_char; stop; synterp_state } in
           let parsed = sentence :: parsed in
           parse_more synterp_state stream raw parsed errors
         with exn ->
@@ -304,6 +349,11 @@ let rec parse_more synterp_state stream raw parsed errors =
       let loc = Loc.get_loc @@ Exninfo.info exn in
       junk_sentence_end stream;
       handle_parse_error start (loc,CLexer.Error.to_string e)
+    | exception exn ->
+      let e, info = Exninfo.capture exn in
+      let loc = Loc.get_loc @@ info in
+      junk_sentence_end stream;
+      handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info))
   end
 
 let parse_more synterp_state stream raw =
@@ -331,8 +381,8 @@ let invalidate top_edit top_id parsed_doc new_sentences =
       invalidate_diff parsed_doc scheduler_state invalid_ids diffs
     | Added new_sentences :: diffs ->
     (* FIXME could have side effect on the following, unchanged sentences *)
-      let add_sentence (parsed_doc,scheduler_state) ({ start; stop; ast; synterp_state } : pre_sentence) =
-        add_sentence parsed_doc start stop ast synterp_state scheduler_state
+      let add_sentence (parsed_doc,scheduler_state) ({ parsing_start; start; stop; ast; synterp_state } : pre_sentence) =
+        add_sentence parsed_doc parsing_start start stop ast synterp_state scheduler_state
       in
       let parsed_doc, scheduler_state = List.fold_left add_sentence (parsed_doc,scheduler_state) new_sentences in
       invalidate_diff parsed_doc scheduler_state invalid_ids diffs
@@ -361,7 +411,7 @@ let validate_document ({ parsed_loc; raw_doc; } as document) =
   log @@ Format.sprintf "%i new sentences" (List.length new_sentences);
   let unchanged_id, invalid_ids, document = invalidate (stop+1) top_id document new_sentences in
   let parsing_errors_by_end =
-    List.fold_left (fun acc error -> LM.add error.stop error acc) errors new_errors
+    List.fold_left (fun acc (error : parsing_error) -> LM.add error.stop error acc) errors new_errors
   in
   let parsed_loc = pos_at_end document in
   unchanged_id, invalid_ids, { document with parsed_loc; parsing_errors_by_end }
@@ -394,4 +444,16 @@ module Internal = struct
     sentence.start
     sentence.stop
 
+  let string_of_error error =
+    let (_, str) = error.msg in
+    Format.sprintf "[parsing error] [%s] (%i -> %i)"
+    str
+    error.start
+    error.stop
+
+  let string_of_item = function
+    | Sentence sentence -> string_of_sentence sentence
+    | Comment _ -> "(* comment *)"
+    | ParsingError error -> string_of_error error
+
 end

language-server/dm/document.mli

@@ -53,7 +53,13 @@ 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. *)
 
+(* Example:                        *)
+(* "  Check 3. "                    *)
+(* ^  ^       ^---- end            *)
+(* |  |------------ start          *)
+(* |---------------- parsing_start *)
 type sentence = {
+  parsing_start : int;
   start : int;
   stop : int;
   synterp_state : Vernacstate.Synterp.t; (* synterp state after this sentence's synterp phase *)
@@ -63,7 +69,18 @@ type sentence = {
   id : sentence_id;
 }
 
+type comment = {
+  start : int;
+  stop : int;
+}
+
+type code_line =
+  | Sentence of sentence
+  | ParsingError of parsing_error
+  | Comment of comment
+
 val sentences : document -> sentence list
+val code_lines_sorted_by_loc : document -> code_line list
 val sentences_sorted_by_loc : document -> sentence list
 
 val get_sentence : document -> sentence_id -> sentence option
@@ -90,9 +107,14 @@ val get_last_sentence : document  -> sentence option
 val schedule : document -> Scheduler.schedule
 
 val range_of_id : document -> Stateid.t -> Range.t
+(** [range_of_id doc id] returns a Range object coressponding to the sentence id given in argument *)
+
+val range_of_id_with_blank_space : document -> Stateid.t -> Range.t
+(** [range_of_id_with_blank_space doc id] returns a Range object coressponding to the sentence id given in argument but with the white spaces before (until the previous sentence) *)
 
 module Internal : sig
 
   val string_of_sentence : sentence -> string
+  val string_of_item : code_line -> string
 
 end

language-server/dm/documentManager.ml

@@ -66,27 +66,25 @@ type exec_overview = {
   processed : Range.t list;
 }
 
-let merge_ranges doc (r1,l) r2 =
-  let loc1 = RawDocument.loc_of_position doc r1.Range.end_ in
-  let loc2 = RawDocument.loc_of_position doc r2.Range.start in
-  if RawDocument.only_whitespace_between doc (loc1+1) (loc2-1) then
+let merge_adjacent_ranges (r1,l) r2 =
+  if Position.compare r1.Range.end_ r2.Range.start == 0 then
     Range.{ start = r1.Range.start; end_ = r2.Range.end_ }, l
   else
     r2, r1 :: l
 
-let compress_sorted_ranges doc = function
+let compress_sorted_ranges = function
   | [] -> []
   | range :: tl ->
-    let r, l = List.fold_left (merge_ranges doc) (range,[]) tl in
+    let r, l = List.fold_left merge_adjacent_ranges (range,[]) tl in
     r :: l
 
-let compress_ranges doc ranges =
+let compress_ranges ranges =
   let ranges = List.sort (fun { Range.start = s1 } { Range.start = s2 } -> Position.compare s1 s2) ranges in
-  compress_sorted_ranges doc ranges
+  compress_sorted_ranges ranges
 
 let executed_ranges doc execution_state loc =
   let ranges_of l =
-    compress_ranges (Document.raw_document doc) @@ List.map (Document.range_of_id doc) l
+    compress_ranges @@ List.map (Document.range_of_id_with_blank_space doc) l
   in
   let ids_before_loc = List.map (fun s -> s.Document.id) @@ Document.sentences_before doc loc in
   let processed_ids = List.filter (fun x -> ExecutionManager.is_executed execution_state x || ExecutionManager.is_remotely_executed execution_state x) ids_before_loc in
@@ -472,15 +470,19 @@ module Internal = struct
     validate_document st
 
   let string_of_state st =
-    let sentences = Document.sentences_sorted_by_loc st.document in
+    let code_lines = Document.code_lines_sorted_by_loc st.document in
     let string_of_state id =
       if ExecutionManager.is_executed st.execution_state id then "(executed)"
       else if ExecutionManager.is_remotely_executed st.execution_state id then "(executed in worker)"
       else "(not executed)"
     in
-    let string_of_sentence sentence =
-      Document.Internal.string_of_sentence sentence ^ " " ^ string_of_state sentence.id
+    let string_of_item item =
+      Document.Internal.string_of_item item ^ " " ^
+        match item with
+        | Sentence { id } -> string_of_state id
+        | ParsingError _ -> "(error)"
+        | Comment _ -> "(comment)"
     in
-    String.concat "\n" @@ List.map string_of_sentence sentences
+    String.concat "\n" @@ List.map string_of_item code_lines
 
 end

language-server/dm/rawDocument.ml

@@ -104,12 +104,3 @@ let apply_text_edit raw (Range.{start; end_}, editText) =
   let new_text = before ^ editText ^ after in (* FIXME avoid concatenation *)
   let new_lines = compute_lines new_text in (* FIXME compute this incrementally *)
   { text = new_text; lines = new_lines }, start
-
-let only_whitespace_between raw loc1 loc2 =
-  let res = ref true in
-  for i = loc1 to loc2 do
-    let code = Char.code raw.text.[i] in
-    if code <> 0x20 && code <> 0xD && code <> 0xA && code <> 0x9
-      then res := false
-  done;
-  !res

language-server/dm/rawDocument.mli

@@ -29,7 +29,3 @@ val word_at_position: t -> Position.t -> string option
 
 (** Applies a text edit, and returns start location *)
 val apply_text_edit : t -> text_edit -> t * int
-
-(** Tests if document text contains only whitespace between the two provided
-    locations, included *)
-val only_whitespace_between : t -> int -> int -> bool

language-server/tests/common.ml

@@ -65,7 +65,7 @@ let rec parse : type a. int -> int -> Document.sentence list -> Document.parsing
       Error ("fewer sentences than expected, only " ^ Int.to_string m ^ " list of errors:\n" ^ errors)
     | E _, _, [] -> Error ("fewer errors than expected, only " ^ Int.to_string n)
 
-let d_sentences doc spec = 
+let d_sentences doc spec =
   let sentences = Document.sentences_sorted_by_loc doc in
   let errors = Document.parse_errors doc in
   let r = run (parse 0 0 sentences errors spec) in

language-server/tests/dm_tests.ml

@@ -33,15 +33,15 @@ let%test_unit "parse.init" =
   let doc = Document.raw_document @@ DocumentManager.Internal.document st in
   [%test_eq: int] (RawDocument.end_loc doc) 44;
   let sentences = Document.sentences @@ DocumentManager.Internal.document st in
-  let positions = Stdlib.List.map (fun s -> s.Document.start) sentences in
+  let positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in
   [%test_eq: int list] positions [ 0; 22 ];
   check_no_diag st
 
 let%test_unit "parse.insert" =
   let st, events = init_test_doc ~text:"Definition x := true. Definition y := false." in
   let st = insert_text st ~loc:0 ~text:"Definition z := 0. " in
   let sentences = Document.sentences @@ DocumentManager.Internal.document st in
-  let positions = Stdlib.List.map (fun s -> s.Document.start) sentences in
+  let positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in
   [%test_eq: int list] positions [ 0; 19; 41 ];
   check_no_diag st
 
@@ -50,8 +50,8 @@ let%test_unit "parse.squash" =
   let st = edit_text st ~start:20 ~stop:21 ~text:"" in
   let doc = DocumentManager.Internal.document st in
   let sentences = Document.sentences doc in
-  let start_positions = Stdlib.List.map (fun s -> s.Document.start) sentences in
-  let stop_positions = Stdlib.List.map (fun s -> s.Document.stop) sentences in
+  let start_positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in
+  let stop_positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.stop) sentences in
   [%test_eq: int list] start_positions [ 44 ];
   [%test_eq: int list] stop_positions [ 62 ];
   [%test_eq: int] (List.length (Document.parse_errors doc)) 1
@@ -60,14 +60,14 @@ let%test_unit "parse.error_recovery" =
   let st, events = init_test_doc ~text:"## . Definition x := true. !! . Definition y := false." in
   let doc = DocumentManager.Internal.document st in
   let sentences = Document.sentences doc in
-  let start_positions = Stdlib.List.map (fun s -> s.Document.start) sentences in
+  let start_positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in
   [%test_eq: int list] start_positions [ 5; 32 ];
   [%test_eq: int] (List.length (Document.parse_errors doc)) 2
 
 let%test_unit "parse.extensions" =
   let st, events = init_test_doc ~text:"Notation \"## x\" := x (at level 0). Definition f (x : nat) := ##xx." in
   let sentences = Document.sentences @@ DocumentManager.Internal.document st in
-  let start_positions = Stdlib.List.map (fun s -> s.Document.start) sentences in
+  let start_positions = Stdlib.List.map (fun (s : Document.sentence) -> s.Document.start) sentences in
   [%test_eq: int list] start_positions [ 0; 35 ];
   check_no_diag st
 
@@ -117,7 +117,7 @@ let%test_unit "exec.require_error" =
   let st = handle_events todo st in
   let ranges = (DocumentManager.executed_ranges st).processed in
   let positions = Stdlib.List.map (fun s -> s.Lsp.Types.Range.start.character) ranges in
-  [%test_eq: int list] positions [ 19 ]
+  [%test_eq: int list] positions [ 18 ]
 
 let%test_unit "step_forward.delete_observe_id" =
   let st, init_events = init_test_doc ~text:"Definition x := 3. Lemma foo : x = 3." in