[fleche] Consolidate test for position target reachability.

We had some code duplication coming from #179, time to consolidate it.

controller/coq_lsp.ml

@@ -231,9 +231,8 @@ let do_position_request ~postpone ~params ~handler =
   let in_range =
     match doc.completed with
     | Yes _ -> true
-    | Failed loc | Stopped loc ->
-      let proc_line = loc.end_.line in
-      line < proc_line || (line = proc_line && col < loc.end_.character)
+    | Failed range | Stopped range ->
+      Fleche.Doc.reached ~range (line,col)
   in
   let in_range =
     match version with

controller/doc_manager.ml

@@ -100,16 +100,12 @@ module Handle = struct
       let pt_request = None in
       let cp_requests = Int.Set.empty in
       ({ handle with cp_requests; pt_request }, wake_up)
-    | Stopped stop_loc ->
+    | Stopped range ->
       let handle, pt_id =
         match handle.pt_request with
         | None -> (handle, Int.Set.empty)
         | Some (id, (req_line, req_col)) ->
-          (* XXX: Same code than in doc.ml *)
-          let stop_line = stop_loc.end_.line in
-          let stop_col = stop_loc.end_.character in
-          if
-            stop_line > req_line || (stop_line = req_line && stop_col >= req_col)
+          if Fleche.Doc.reached ~range (req_line, req_col)
           then ({ handle with pt_request = None }, Int.Set.singleton id)
           else (handle, Int.Set.empty)
       in

controller/doc_manager.mli

@@ -49,3 +49,4 @@ val serve_on_completion : uri:string -> id:int -> unit
     now, we allow a single request like that. Maybe returns the id of the
     previous request which should now be cancelled. *)
 val serve_if_point : uri:string -> id:int -> point:int * int -> int option
+

fleche/doc.ml

@@ -562,17 +562,16 @@ module Target = struct
     | Position of int * int
 end
 
-let beyond_target (pos : Types.Range.t) target =
+let reached ~(range : Types.Range.t) (line, col) =
+  let reached_line = range.end_.line in
+  let reached_col = range.end_.character in
+  line < reached_line || (line = reached_line && col <= reached_col)
+
+let beyond_target (range : Types.Range.t) target =
   match target with
   | Target.End -> false
   | Position (cut_line, cut_col) ->
-    (* This needs careful thinking as to help with the show goals postponement
-       case. *)
-    (* let pos_line = pos.line_nb_last - 1 in *)
-    (* let pos_col = pos.ep - pos.bol_pos_last in *)
-    let pos_line = pos.end_.line in
-    let pos_col = pos.end_.character in
-    pos_line > cut_line || (pos_line = cut_line && pos_col > cut_col)
+    reached ~range (cut_line, cut_col)
 
 let pr_target = function
   | Target.End -> "end"

fleche/doc.mli

@@ -106,3 +106,6 @@ end
 (** [check ofmt ~fb_queue ?cutpoint ~doc] if set, [cutpoint] will have Flèche
     stop after the point specified there has been reached. *)
 val check : ofmt:Format.formatter -> target:Target.t -> doc:t -> unit -> t
+
+(** Helper used to determine wakeup / postponement condictions wrt targets *)
+val reached : range:Types.Range.t -> (int*int) -> bool