From b9d7777dd5e8b10028aee68d7f708e735054ab7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 29 Sep 2024 17:38:52 +0200 Subject: [PATCH] [fleche] New immediate request serving mode. In this mode, requests are served with whatever document state we have. This is very useful when we are not in continuous mode, and we don't have a good reference as to what to build, for example in `documentSymbols` (cc: #816) The mode actually works pretty well in practice as often language requests will come after goals requests, so the info that is needed is at hand. It could also be tried to set the build target for immediate requests to the view hint, but we should see some motivation for that. This commit switches `documentSymbols` to the immediate mode, when in lazy checking mode. --- CHANGES.md | 9 +++++++++ controller/lsp_core.ml | 11 ++++++++++- controller/request.ml | 8 ++++++++ controller/request.mli | 4 ++++ fleche/theory.ml | 3 +++ fleche/theory.mli | 1 + 6 files changed, 35 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index e8038419..de4884e1 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -25,6 +25,15 @@ @corwin-of-amber, #433) - [hover] Fix universe and level printing in hover (#839, fixes #835 , @ejgallego , @Alizter) + - [fleche] New immediate request serving mode. In this mode, requests + are served with whatever document state we have. This is very + useful when we are not in continuous mode, and we don't have a good + reference as to what to build, for example in + `documentSymbols`. The mode actually works pretty well in practice + as often language requests will come after goals requests, so the + info that is needed is at hand. It could also be tried to set the + build target for immediate requests to the view hint, but we should + see some motivation for that (@ejgallego, #841) # coq-lsp 0.2.0: From Green to Blue ----------------------------------- diff --git a/controller/lsp_core.ml b/controller/lsp_core.ml index 102afbf9..eb33483e 100644 --- a/controller/lsp_core.ml +++ b/controller/lsp_core.ml @@ -402,7 +402,16 @@ let do_document_request_maybe ~params ~handler = let postpone = not !Fleche.Config.v.check_only_on_request in do_document_request ~postpone ~params ~handler -let do_symbols = do_document_request_maybe ~handler:Rq_symbols.symbols +let do_immediate ~params ~handler = + let uri = Helpers.get_uri params in + Rq.Action.Data (Request.Data.Immediate { uri; handler }) + +(* new immediate mode, cc: #816 *) +let do_symbols ~params = + let handler = Rq_symbols.symbols in + if !Fleche.Config.v.check_only_on_request then do_immediate ~params ~handler + else do_document_request ~postpone:true ~params ~handler + let do_document = do_document_request_maybe ~handler:Rq_document.request let do_save_vo = do_document_request_maybe ~handler:Rq_save.request let do_lens = do_document_request_maybe ~handler:Rq_lens.request diff --git a/controller/request.ml b/controller/request.ml index f2acdb11..3ea2fac4 100644 --- a/controller/request.ml +++ b/controller/request.ml @@ -48,6 +48,10 @@ type position = (** Requests that require data access *) module Data = struct type t = + | Immediate of + { uri : Lang.LUri.File.t + ; handler : document + } | DocRequest of { uri : Lang.LUri.File.t ; postpone : bool @@ -63,6 +67,7 @@ module Data = struct (* Debug printing *) let data fmt = function + | Immediate { uri = _; handler = _ } -> Format.fprintf fmt "{k:imm }" | DocRequest { uri = _; postpone; handler = _ } -> Format.fprintf fmt "{k:doc | p: %B}" postpone | PosRequest { uri = _; point; version; postpone; handler = _ } -> @@ -73,6 +78,8 @@ module Data = struct let dm_request pr = match pr with + | Immediate { uri; handler = _ } -> + (uri, false, Fleche.Theory.Request.Immediate) | DocRequest { uri; postpone; handler = _ } -> (uri, postpone, Fleche.Theory.Request.FullDoc) | PosRequest { uri; point; version; postpone; handler = _ } -> @@ -80,6 +87,7 @@ module Data = struct let serve ~token ~doc pr = match pr with + | Immediate { uri = _; handler } -> handler ~token ~doc | DocRequest { uri = _; postpone = _; handler } -> handler ~token ~doc | PosRequest { uri = _; point; version = _; postpone = _; handler } -> handler ~token ~point ~doc diff --git a/controller/request.mli b/controller/request.mli index da4f5b41..d760381d 100644 --- a/controller/request.mli +++ b/controller/request.mli @@ -35,6 +35,10 @@ type position = (** Requests that require data access *) module Data : sig type t = + | Immediate of + { uri : Lang.LUri.File.t + ; handler : document + } | DocRequest of { uri : Lang.LUri.File.t ; postpone : bool diff --git a/fleche/theory.ml b/fleche/theory.ml index d4234974..9c4f710a 100644 --- a/fleche/theory.ml +++ b/fleche/theory.ml @@ -341,6 +341,7 @@ let close ~uri = module Request = struct type request = + | Immediate | FullDoc | PosInDoc of { point : int * int @@ -379,6 +380,7 @@ module Request = struct let default () = Cancel in (* should be Cancelled? *) match request with + | Immediate -> Handle.with_doc ~kind ~default ~uri ~f:(fun _ doc -> Now doc) | FullDoc -> Handle.with_doc ~kind ~default ~uri ~f:(fun _ doc -> match (Doc.Completion.is_completed doc.completed, postpone) with @@ -402,6 +404,7 @@ module Request = struct (** Removes the request from the list of things to wake up *) let remove { id; uri; postpone = _; request } = match request with + | Immediate -> () | FullDoc -> Handle.remove_cp_request ~uri ~id | PosInDoc { point; _ } -> Handle.remove_pt_request ~uri ~id ~point end diff --git a/fleche/theory.mli b/fleche/theory.mli index e20c2cf7..1703875f 100644 --- a/fleche/theory.mli +++ b/fleche/theory.mli @@ -49,6 +49,7 @@ val close : uri:Lang.LUri.File.t -> unit module Request : sig type request = + | Immediate | FullDoc | PosInDoc of { point : int * int