[lsp] Only serve request when the document meta-data is up to date.

CHANGES.md

@@ -23,6 +23,8 @@
    goal list (@ejgallego, #115, fixes #109)
  - Resume checking from common prefix on document update (@ejgallego,
    #111, fixes #110)
+ - Cancel / reject requests that can be served due to document not
+   being processed sufficiently (@ejgallego, fixes #100)
 
 # coq-lsp 0.1.0: Memory
 -----------------------

controller/coq_lsp.ml

@@ -233,11 +233,16 @@ let do_close _ofmt params =
   let doc_file = string_field "uri" document in
   Hashtbl.remove doc_table doc_file
 
-let grab_doc params =
+let get_textDocument params =
   let document = dict_field "textDocument" params in
-  let doc_file = string_field "uri" document in
-  let doc = Hashtbl.(find doc_table doc_file) in
-  (doc_file, doc)
+  let uri = string_field "uri" document in
+  let doc = Hashtbl.find doc_table uri in
+  (uri, doc)
+
+let get_position params =
+  let pos = dict_field "position" params in
+  let line, character = (int_field "line" pos, int_field "character" pos) in
+  (line, character)
 
 let mk_syminfo file (name, _path, kind, pos) : J.t =
   `Assoc
@@ -258,57 +263,58 @@ let _kind_of_type _tm = 13
    *) | _ -> 12 (* Function *) *)
 
 let do_symbols ofmt ~id params =
-  let file, doc = grab_doc params in
-  let f loc id = mk_syminfo file (Names.Id.to_string id, "", 12, loc) in
-  let ast = asts_of_doc doc in
-  let slist = Coq.Ast.grab_definitions f ast in
-  let msg = LSP.mk_reply ~id ~result:(`List slist) in
-  LIO.send_json ofmt msg
-
-let get_docTextPosition params =
-  let document = dict_field "textDocument" params in
-  let file = string_field "uri" document in
-  let pos = dict_field "position" params in
-  let line, character = (int_field "line" pos, int_field "character" pos) in
-  (file, (line, character))
-
-(* XXX refactor *)
-let loc_info loc = Coq.Ast.pr_loc loc
-
-let do_hover ofmt ~id params =
+  let uri, doc = get_textDocument params in
+  match doc.completed with
+  | Yes _ ->
+    let f loc id = mk_syminfo uri (Names.Id.to_string id, "", 12, loc) in
+    let ast = asts_of_doc doc in
+    let slist = Coq.Ast.grab_definitions f ast in
+    let msg = LSP.mk_reply ~id ~result:(`List slist) in
+    LIO.send_json ofmt msg
+  | Stopped _ ->
+    let code = -32802 in
+    let message = "Document is not ready" in
+    LSP.mk_request_error ~id ~code ~message |> LIO.send_json ofmt
+
+let do_position_request ofmt ~id params ~handler =
+  let _uri, doc = get_textDocument params in
+  let point = get_position params in
+  let line, col = point in
+  let in_range =
+    match doc.completed with
+    | Yes _ -> true
+    | Stopped loc ->
+      line < loc.line_nb_last
+      || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last)
+  in
+  if in_range then
+    let result = handler ~doc ~point in
+    LSP.mk_reply ~id ~result |> LIO.send_json ofmt
+  else
+    (* -32802 = RequestFailed | -32803 = ServerCancelled ; *)
+    let code = -32802 in
+    let message = "Document is not ready" in
+    LSP.mk_request_error ~id ~code ~message |> LIO.send_json ofmt
+
+let hover_handler ~doc ~point =
   let show_loc_info = true in
-  let uri, point = get_docTextPosition params in
-  let doc = Hashtbl.find doc_table uri in
   let loc_string =
     Fleche.Info.LC.loc ~doc ~point Exact
-    |> Option.map loc_info |> Option.default "no ast"
+    |> Option.map Coq.Ast.pr_loc |> Option.default "no ast"
   in
   let info_string =
     Fleche.Info.LC.info ~doc ~point Exact |> Option.default "no info"
   in
   let hover_string =
     if show_loc_info then loc_string ^ "\n___\n" ^ info_string else info_string
   in
-  let result =
-    `Assoc
-      [ ( "contents"
-        , `Assoc
-            [ ("kind", `String "markdown"); ("value", `String hover_string) ] )
-      ]
-  in
-  let msg = LSP.mk_reply ~id ~result in
-  LIO.send_json ofmt msg
+  `Assoc
+    [ ( "contents"
+      , `Assoc [ ("kind", `String "markdown"); ("value", `String hover_string) ]
+      )
+    ]
 
-let do_completion ofmt ~id params =
-  let uri, _ = get_docTextPosition params in
-  let doc = Hashtbl.find doc_table uri in
-  let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in
-  let ast = asts_of_doc doc in
-  let clist = Coq.Ast.grab_definitions f ast in
-  let result = `List clist in
-  let msg = LSP.mk_reply ~id ~result in
-  LIO.send_json ofmt msg
-(* LIO.log_error "do_completion" (string_of_int line ^"-"^ string_of_int pos) *)
+let do_hover ofmt = do_position_request ofmt ~handler:hover_handler
 
 (* Replace by ppx when we can print goals properly in the client *)
 let mk_hyp { Coq.Goals.names; def = _; ty } : Yojson.Safe.t =
@@ -327,23 +333,26 @@ let goals_mode =
   if !Fleche.Config.v.goal_after_tactic then Fleche.Info.PrevIfEmpty
   else Fleche.Info.Prev
 
-let do_goals ofmt ~id params =
-  let uri, point = get_docTextPosition params in
-  let doc = Hashtbl.find doc_table uri in
+let goals_handler ~doc ~point =
   let goals = Fleche.Info.LC.goals ~doc ~point goals_mode in
-  let result =
-    `Assoc
-      [ ( "textDocument"
-        , `Assoc [ ("uri", `String uri); ("version", `Int doc.version) ] )
-      ; ( "position"
-        , `Assoc [ ("line", `Int (fst point)); ("character", `Int (snd point)) ]
-        )
-      ; ("goals", `List (mk_goals goals))
-      ]
-  in
-  let msg = LSP.mk_reply ~id ~result in
-  LIO.send_json ofmt msg
+  `Assoc
+    [ ( "textDocument"
+      , `Assoc [ ("uri", `String doc.uri); ("version", `Int doc.version) ] )
+    ; ( "position"
+      , `Assoc [ ("line", `Int (fst point)); ("character", `Int (snd point)) ]
+      )
+    ; ("goals", `List (mk_goals goals))
+    ]
+
+let do_goals ofmt = do_position_request ofmt ~handler:goals_handler
+
+let completion_handler ~doc ~point:_ =
+  let f _loc id = `Assoc [ ("label", `String Names.Id.(to_string id)) ] in
+  let ast = asts_of_doc doc in
+  let clist = Coq.Ast.grab_definitions f ast in
+  `List clist
 
+let do_completion ofmt = do_position_request ofmt ~handler:completion_handler
 let memo_cache_file = ".coq-lsp.cache"
 
 let memo_save_to_disk () =

fleche/info.ml

@@ -113,6 +113,7 @@ module type S = sig
 
   type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option
 
+  val node : (approx, Doc.node) query
   val loc : (approx, Loc.t) query
   val ast : (approx, Coq.Ast.t) query
   val goals : (approx, Coq.Goals.reified_pp) query
@@ -142,6 +143,8 @@ module Make (P : Point) : S with module P := P = struct
     in
     find None doc.Doc.nodes
 
+  let node = find
+
   let if_not_empty (pp : Pp.t) =
     if Pp.(repr pp = Ppcmd_empty) then None else Some pp
 

fleche/info.mli

@@ -44,6 +44,7 @@ module type S = sig
 
   type ('a, 'r) query = doc:Doc.t -> point:P.t -> 'a -> 'r option
 
+  val node : (approx, Doc.node) query
   val loc : (approx, Loc.t) query
   val ast : (approx, Coq.Ast.t) query
   val goals : (approx, Coq.Goals.reified_pp) query

lsp/base.ml

@@ -34,6 +34,13 @@ let _parse_uri str =
 let mk_reply ~id ~result =
   `Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ]
 
+let mk_request_error ~id ~code ~message =
+  `Assoc
+    [ ("jsonrpc", `String "2.0")
+    ; ("id", `Int id)
+    ; ("error", `Assoc [ ("code", `Int code); ("message", `String message) ])
+    ]
+
 let mk_notification ~method_ ~params =
   `Assoc
     [ ("jsonrpc", `String "2.0")

lsp/base.mli

@@ -24,6 +24,9 @@ val mk_notification :
 (** Answer to a request *)
 val mk_reply : id:int -> result:Yojson.Safe.t -> Yojson.Safe.t
 
+(** Fail a request *)
+val mk_request_error : id:int -> code:int -> message:string -> Yojson.Safe.t
+
 (* val mk_diagnostic : Range.t * int * string * unit option -> Yojson.Basic.t *)
 val mk_diagnostics :
      uri:string