From 8e967dd27becad9a6fc9c6399fafa2f4441181a0 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 29 Aug 2023 18:36:11 +0200 Subject: [PATCH 1/4] Refactor observe_id. observe_id is only used in manual mode. In continuous mode it is now null. In manual mode we now introduce the Top type to indicate that observe id is currently at the top of the document. --- language-server/dm/document.ml | 1 + language-server/dm/documentManager.ml | 112 +++++++++++++++++-------- language-server/dm/documentManager.mli | 14 +++- language-server/vscoqtop/lspManager.ml | 72 ++++++++-------- 4 files changed, 123 insertions(+), 76 deletions(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 5bc35c561..9395e7b74 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -332,6 +332,7 @@ let validate_document ({ parsed_loc; raw_doc; } as document) = (* We take the state strictly before parsed_loc to cover the case when the end of the sentence is editted *) let (stop, synterp_state, _scheduler_state) = state_strictly_before document parsed_loc in + (* let top_id = find_sentence_strictly_before document parsed_loc with None -> Top | Some sentence -> Id sentence.id in *) let top_id = Option.map (fun sentence -> sentence.id) (find_sentence_strictly_before document parsed_loc) in let text = RawDocument.text raw_doc in let stream = Stream.of_string text in diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 5f99060b8..95f27ca50 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -20,13 +20,23 @@ open Types let Log log = Log.mk_log "documentManager" +type observe_id = Id of Types.sentence_id | Top + +let to_sentence_id = function +| Top -> None +| Id id -> Some id + +(* let observe_id_to_string = function +| Top -> "Top" +| Id id -> Stateid.to_string id *) + type state = { uri : DocumentUri.t; init_vs : Vernacstate.t; opts : Coqargs.injection_command list; document : Document.document; execution_state : ExecutionManager.state; - observe_id : Types.sentence_id option; + observe_id : observe_id option; } type event = @@ -87,17 +97,23 @@ let executed_ranges doc execution_state loc = } let executed_ranges st = - let loc = match Option.bind st.observe_id (Document.get_sentence st.document) with - | None -> 0 - | Some { stop } -> stop + let loc = match st.observe_id with + | None -> max_int + | Some Top -> 0 + | Some (Id id) -> match Document.get_sentence st.document id with + | None -> failwith "observe_id does not exist" + | Some { stop } -> stop in executed_ranges st.document st.execution_state loc let observe_id_range st = let doc = Document.raw_document st.document in - match Option.bind st.observe_id (Document.get_sentence st.document) with + match st.observe_id with | None -> None - | Some { start; stop} -> + | Some Top -> None + | Some (Id id) -> match Document.get_sentence st.document id with + | None -> failwith "observe_id does not exist" + | Some { start; stop } -> let start = RawDocument.position_of_loc doc start in let end_ = RawDocument.position_of_loc doc stop in let range = Range.{ start; end_ } in @@ -144,8 +160,12 @@ let id_of_pos st pos = | None -> None | Some { id } -> Some id +let id_of_pos_opt st = function + | None -> begin match st.observe_id with None | Some Top -> None | Some Id id -> Some id end + | Some pos -> id_of_pos st pos + let get_messages st pos = - match Option.cata (id_of_pos st) st.observe_id pos with + match id_of_pos_opt st pos with | None -> log "get_messages: Could not find id";[] | Some id -> log "get_messages: Found id"; let error = ExecutionManager.error st.execution_state id in @@ -155,11 +175,10 @@ let get_messages st pos = | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback | None -> feedback -let interpret_to ~stateful ~background state id : (state * event Sel.Event.t list) = +let observe ~background state id : (state * event Sel.Event.t list) = match Document.get_sentence state.document id with | None -> (state, []) (* TODO error? *) - | Some { id } -> - let state = if stateful then { state with observe_id = Some id } else state in + | Some {id } -> let vst_for_next_todo, todo = ExecutionManager.build_tasks_for (Document.schedule state.document) state.execution_state id in if CList.is_empty todo then (state, []) @@ -168,48 +187,61 @@ let interpret_to ~stateful ~background state id : (state * event Sel.Event.t lis let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started = Unix.gettimeofday (); background }) in (state, [ event ]) -let interpret_to_position ~stateful st pos = +let clear_observe_id st = + { st with observe_id = None } + +let reset_to_top st = + { st with observe_id = Some Top } + +let interpret_to st id = + let observe_id = if st.observe_id = None then None else (Some (Id id)) in + let st = { st with observe_id} in + observe ~background:false st id + +let interpret_to_position st pos = match id_of_pos st pos with | None -> (st, []) (* document is empty *) - | Some id -> interpret_to ~stateful ~background:false st id + | Some id -> interpret_to st id let interpret_to_previous st = match st.observe_id with - | None -> (st, []) - | Some oid -> - match Document.get_sentence st.document oid with + | None -> failwith "interpret to previous with no observe_id" + | Some Top -> (st, []) + | Some (Id id) -> + match Document.get_sentence st.document id with | None -> (st, []) (* TODO error? *) | Some { start } -> match Document.find_sentence_before st.document start with | None -> Vernacstate.unfreeze_full_state st.init_vs; - { st with observe_id=None}, [] - | Some { id } -> interpret_to ~stateful:true ~background:false st id + { st with observe_id=(Some Top)}, [] + | Some { id } -> interpret_to st id let interpret_to_next st = match st.observe_id with - | None -> + | None -> failwith "interpret to next with no observe_id" + | Some Top -> begin match Document.get_first_sentence st.document with | None -> (st, []) (*The document is empty*) - | Some {id} -> interpret_to ~stateful:true ~background:false st id + | Some {id} -> interpret_to st id end - | Some id -> + | Some (Id id) -> match Document.get_sentence st.document id with | None -> (st, []) (* TODO error? *) | Some { stop } -> match Document.find_sentence_after st.document (stop+1) with | None -> (st, []) - | Some {id } -> interpret_to ~stateful:true ~background:false st id + | Some {id } -> interpret_to st id let interpret_to_end st = - match Document.get_last_sentence st.document with + match Document.get_last_sentence st.document with | None -> (st, []) - | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~stateful:true ~background:false st id + | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to st id let interpret_in_background st = - match Document.get_last_sentence st.document with + match Document.get_last_sentence st.document with | None -> (st, []) - | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); interpret_to ~stateful:true ~background:true st id + | Some {id} -> log ("interpret_to_end id = " ^ Stateid.to_string id); observe ~background:true st id let is_above st id1 id2 = let range1 = Document.range_of_id st id1 in @@ -219,8 +251,10 @@ let is_above st id1 id2 = let validate_document state = let unchanged_id, invalid_roots, document = Document.validate_document state.document in let observe_id = match unchanged_id, state.observe_id with - | None, _ | _, None -> None - | Some id, Some id' -> if is_above state.document id id' then Some id else Some id' + | _, None -> None + | None, Some (Id _) -> None + | _, Some Top -> Some Top + | Some id, Some (Id id') -> if is_above state.document id id' then Some (Id id) else state.observe_id in let execution_state = List.fold_left (fun st id -> @@ -228,7 +262,7 @@ let validate_document state = ) state.execution_state (Stateid.Set.elements invalid_roots) in { state with document; execution_state; observe_id } -let init init_vs ~opts uri ~text = +let init init_vs ~opts uri ~text observe_id = Vernacstate.unfreeze_full_state init_vs; let top = try Coqargs.(dirpath_of_top (TopPhysical (DocumentUri.to_path uri))) with e -> raise e @@ -237,16 +271,17 @@ let init init_vs ~opts uri ~text = let init_vs = Vernacstate.freeze_full_state () in let document = Document.create_document init_vs.Vernacstate.synterp text in let execution_state, feedback = ExecutionManager.init init_vs in - let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in + let st = { uri; opts; init_vs; document; execution_state; observe_id } in validate_document st, [inject_em_event feedback] -let reset { uri; opts; init_vs; document; execution_state } = +let reset { uri; opts; init_vs; document; execution_state; observe_id } = let text = RawDocument.text @@ Document.raw_document document in Vernacstate.unfreeze_full_state init_vs; let document = Document.create_document init_vs.synterp text in ExecutionManager.destroy execution_state; let execution_state, feedback = ExecutionManager.init init_vs in - let st = { uri; opts; init_vs; document; execution_state; observe_id = None } in + let observe_id = if observe_id = None then None else (Some Top) in + let st = { uri; opts; init_vs; document; execution_state; observe_id} in validate_document st, [inject_em_event feedback] let apply_text_edits state edits = @@ -285,7 +320,12 @@ let get_proof st diff_mode pos = let oid = fst @@ Scheduler.task_for_sentence (Document.schedule st.document) id in Option.bind oid (ExecutionManager.get_vernac_state st.execution_state) in - let oid = Option.cata (id_of_pos st) st.observe_id pos in + let observe_id = + match st.observe_id with + | None -> None + | Some observe_id -> to_sentence_id observe_id + in + let oid = Option.cata (id_of_pos st) observe_id pos in let ost = Option.bind oid (ExecutionManager.get_vernac_state st.execution_state) in let previous = Option.bind oid previous_st in Option.bind ost (ProofState.get_proof ~previous diff_mode) @@ -315,7 +355,7 @@ let parse_entry st pos entry pattern = let about st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in - match get_context st pos with + match get_context st pos with | None -> Error ("No context found") (*TODO execute *) | Some (sigma, env) -> try @@ -341,7 +381,7 @@ let hover st pos = | Some pattern -> log ("hover: found word at cursor: " ^ pattern); let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in - match get_context st pos with + match get_context st pos with | None -> log "hover: no context found"; None | Some (sigma, env) -> try @@ -354,7 +394,7 @@ let hover st pos = let check st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in - match get_context st pos with + match get_context st pos with | None -> Error ("No context found") (*TODO execute *) | Some (sigma,env) -> let rc = parse_entry st loc Pcoq.Constr.lconstr pattern in @@ -378,7 +418,7 @@ let locate st pos ~pattern = let print st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in - match get_context st pos with + match get_context st pos with | None -> Error("No context found") | Some (sigma, env) -> let qid = parse_entry st loc (Pcoq.Prim.smart_global) pattern in diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 95a351f13..fd6ef064d 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -24,6 +24,8 @@ open CompletionItems and get feedback. Note that it does not require IDEs to parse vernacular sentences. *) +type observe_id = Id of Types.sentence_id | Top + type state type event @@ -31,7 +33,7 @@ val pp_event : Format.formatter -> event -> unit type events = event Sel.Event.t list -val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> state * events +val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> observe_id option -> state * events (** [init st opts uri text] initializes the document manager with initial vernac state [st] on which command line opts will be set. *) @@ -40,7 +42,13 @@ val apply_text_edits : state -> text_edit list -> state document is parsed, outdated executions states are invalidated, and the observe id is updated. *) -val interpret_to_position : stateful:bool -> state -> Position.t -> (state * events) +val clear_observe_id : state -> state +(** [clear_observe_id state] updates the state to make the observe_id None *) + +val reset_to_top : state -> state +(** [reset_to_top state] updates the state to make the observe_id Top *) + +val interpret_to_position : state -> Position.t -> (state * events) (** [interpret_to_position stateful doc pos] navigates to the last sentence ending before or at [pos] and returns the resulting state. The [stateful] flag determines if we record the resulting position in the state. *) @@ -111,7 +119,7 @@ module Internal : sig val raw_document : state -> RawDocument.t val execution_state : state -> ExecutionManager.state val string_of_state : state -> string - val observe_id : state -> Types.sentence_id option + val observe_id : state -> observe_id option val validate_document : state -> state (** [validate_document doc] reparses the text of [doc] and invalidates the diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 8f1354fdb..db211190b 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -212,7 +212,8 @@ let update_view uri st = ) let run_documents () = - let interpret_doc_in_bg path st events = + let interpret_doc_in_bg path (st : Dm.DocumentManager.state) events = + let st = Dm.DocumentManager.clear_observe_id st in let (st, events') = Dm.DocumentManager.interpret_in_background st in let uri = DocumentUri.of_path path in Hashtbl.replace states path st; @@ -222,10 +223,18 @@ let run_documents () = in Hashtbl.fold interpret_doc_in_bg states [] +let reset_observe_ids = + let reset_doc_observe_id path (st : Dm.DocumentManager.state) events = + let st = Dm.DocumentManager.reset_to_top st in + Hashtbl.replace states path st + in + Hashtbl.fold reset_doc_observe_id states + let textDocumentDidOpen params = let Lsp.Types.DidOpenTextDocumentParams.{ textDocument = { uri; text } } = params in let vst, opts = get_init_state () in - let st, events = try Dm.DocumentManager.init vst ~opts uri ~text with + let observe_id = if !check_mode = Settings.Mode.Continuous then None else Some Dm.DocumentManager.Top in + let st, events = try Dm.DocumentManager.init vst ~opts uri ~text observe_id with e -> raise e in let (st, events') = @@ -293,7 +302,7 @@ let coqtopInterpretToPoint params = match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "[interpretToPoint] ignoring event on non existant document"; [] | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_position ~stateful:(!check_mode = Settings.Mode.Manual) st position in + let (st, events) = Dm.DocumentManager.interpret_to_position st position in Hashtbl.replace states (DocumentUri.to_path uri) st; update_view uri st; let sel_events = inject_dm_events (uri, events) in @@ -301,39 +310,29 @@ let coqtopInterpretToPoint params = let coqtopStepBackward params = let Notification.Client.StepBackwardParams.{ textDocument = { uri } } = params in - match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "[stepBackward] ignoring event on non existant document"; [] - | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_previous st in - let range = Dm.DocumentManager.observe_id_range st in - Hashtbl.replace states (DocumentUri.to_path uri) st; - update_view uri st; - if !check_mode = Settings.Mode.Manual then - match range with - | None -> - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] (* how can this do anything? isn't observe_id None? *) - | Some range -> - [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] - else - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] (* isn't observe_id none in continuous mode? If so, how does this do anything? *) + let st = Hashtbl.find states (DocumentUri.to_path uri) in + let (st, events) = Dm.DocumentManager.interpret_to_previous st in + let range = Dm.DocumentManager.observe_id_range st in + Hashtbl.replace states (DocumentUri.to_path uri) st; + update_view uri st; + match range with + | None -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + | Some range -> + [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] let coqtopStepForward params = let Notification.Client.StepForwardParams.{ textDocument = { uri } } = params in - match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log @@ "ignoring event on non existant document"; [] - | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_next st in - let range = Dm.DocumentManager.observe_id_range st in - Hashtbl.replace states (DocumentUri.to_path uri) st; - update_view uri st; - if !check_mode = Settings.Mode.Manual then - match range with - | None -> - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] - | Some range -> - [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] - else - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + let st = Hashtbl.find states (DocumentUri.to_path uri) in + let (st, events) = Dm.DocumentManager.interpret_to_next st in + let range = Dm.DocumentManager.observe_id_range st in + Hashtbl.replace states (DocumentUri.to_path uri) st; + update_view uri st; + match range with + | None -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + | Some range -> + [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] let make_CompletionItem i item : CompletionItem.t = let (label, insertText, typ, path) = Dm.CompletionItems.pp_completion_item item in @@ -441,10 +440,9 @@ let workspaceDidChangeConfiguration params = let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in let settings = Settings.t_of_yojson settings in do_configuration settings; - if !check_mode = Settings.Mode.Continuous then - run_documents () - else - [] + match !check_mode with + | Continuous -> run_documents () + | Manual -> reset_observe_ids (); ([] : events) let dispatch_std_request : type a. Jsonrpc.Id.t -> a Lsp.Client_request.t -> (a,string) result * events = fun id req -> From 7a06d456d55ba3cf6feb25920129de799e00a0f0 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Fri, 24 Nov 2023 15:21:57 +0100 Subject: [PATCH 2/4] Correct unit tests. --- language-server/dm/documentManager.ml | 4 ++- language-server/dm/documentManager.mli | 2 +- language-server/tests/common.ml | 2 +- language-server/tests/dm_tests.ml | 44 -------------------------- 4 files changed, 5 insertions(+), 47 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 95f27ca50..3933b8bc6 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -437,7 +437,9 @@ module Internal = struct st.execution_state let observe_id st = - st.observe_id + match st.observe_id with + | None | Some Top -> None + | Some (Id id) -> Some id let validate_document st = validate_document st diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index fd6ef064d..9ccd92aa8 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -119,7 +119,7 @@ module Internal : sig val raw_document : state -> RawDocument.t val execution_state : state -> ExecutionManager.state val string_of_state : state -> string - val observe_id : state -> observe_id option + val observe_id : state -> sentence_id option val validate_document : state -> state (** [validate_document doc] reparses the text of [doc] and invalidates the diff --git a/language-server/tests/common.ml b/language-server/tests/common.ml index afb4f7552..6d668e55d 100644 --- a/language-server/tests/common.ml +++ b/language-server/tests/common.ml @@ -27,7 +27,7 @@ let injections = let init_state = Vernacstate.freeze_full_state () let openDoc uri ~text = - DocumentManager.init init_state ~opts:injections uri ~text + DocumentManager.init init_state ~opts:injections uri ~text (Some DocumentManager.Top) let run r = [%test_pred: (_,string) Result.t ] (function Error _ -> false | _ -> true) r; diff --git a/language-server/tests/dm_tests.ml b/language-server/tests/dm_tests.ml index 3351f5443..b8d15cac1 100644 --- a/language-server/tests/dm_tests.ml +++ b/language-server/tests/dm_tests.ml @@ -209,50 +209,6 @@ let%test_unit "step_backward.document_begin" = let st = handle_events todo st in [%test_eq: bool] (Option.is_none (DocumentManager.Internal.observe_id st)) true -(* With this test we can check that interpret_in_background has lower priority then interpret to *) -let%test_unit "interpret_in_background.interpret_to stateful" = - let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := false. Definition z := 0." in - let st, (s1, (s2, (s3, ()))) = dm_parse st (P (P (P O))) in - let todo = Sel.Todo.(add empty init_events) in - let st = handle_events todo st in - let st1, events = DocumentManager.interpret_in_background st in - let todo = Sel.Todo.(add empty events) in - let position = RawDocument.position_of_loc (DocumentManager.Internal.raw_document st) s2.stop in - let st2, events = DocumentManager.interpret_to_position ~stateful:true st1 position in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st1 in - [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s3.id)) (DocumentManager.Internal.observe_id st) - -(* With this test interpret_to_end and interpret_to have the same priority, and interpret to is stateful - so it will modify observe id, they will get executed in order of insertion, hence observe_id = s2.id *) -let%test_unit "interpret_to_end.interpret_to stateful" = - let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := false. Definition z := 0." in - let st, (s1, (s2, (s3, ()))) = dm_parse st (P (P (P O))) in - let todo = Sel.Todo.(add empty init_events) in - let st = handle_events todo st in - let st, events = DocumentManager.interpret_to_end st in - let todo = Sel.Todo.(add empty events) in - let position = RawDocument.position_of_loc (DocumentManager.Internal.raw_document st) s2.stop in - let st, events = DocumentManager.interpret_to_position ~stateful:true st position in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s2.id)) (DocumentManager.Internal.observe_id st) - -(* With this test interpret_to_end and interpret_to have the same priority, and interpret to is not stateful - so it will not modify observe id, they will get executed in order of insertion, hence observe_id = s3.id *) -let%test_unit "interpret_to_end.interpret_to not stateful" = - let st, init_events = init_test_doc ~text:"Definition x := true. Definition y := false. Definition z := 0." in - let st, (s1, (s2, (s3, ()))) = dm_parse st (P (P (P O))) in - let todo = Sel.Todo.(add empty init_events) in - let st = handle_events todo st in - let st, events = DocumentManager.interpret_to_end st in - let todo = Sel.Todo.(add empty events) in - let position = RawDocument.position_of_loc (DocumentManager.Internal.raw_document st) s2.stop in - let st, events = DocumentManager.interpret_to_position ~stateful:false st position in - let todo = Sel.Todo.(add todo events) in - let st = handle_events todo st in - [%test_pred: sentence_id option] (Option.equal Stateid.equal (Some s3.id)) (DocumentManager.Internal.observe_id st) - (* let%test_unit "exec.insert" = let st, events = init_test_doc ~text:"Definition x := true. Definition y := false." in From 22784f684df2186bec16f567100a0f07adbf993d Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Mon, 27 Nov 2023 10:04:58 +0100 Subject: [PATCH 3/4] Reset view when switching from continuous to manual. --- language-server/vscoqtop/lspManager.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index db211190b..b6d326b0a 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -226,7 +226,9 @@ let run_documents () = let reset_observe_ids = let reset_doc_observe_id path (st : Dm.DocumentManager.state) events = let st = Dm.DocumentManager.reset_to_top st in - Hashtbl.replace states path st + let uri = DocumentUri.of_path path in + Hashtbl.replace states path st; + update_view uri st in Hashtbl.fold reset_doc_observe_id states From d17a89c8e3d595d543e2255d66fe9226eaea71bd Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Thu, 30 Nov 2023 09:29:03 +0100 Subject: [PATCH 4/4] Fix Hashtbl.find_opt regression. --- language-server/vscoqtop/lspManager.ml | 44 ++++++++++++++------------ 1 file changed, 24 insertions(+), 20 deletions(-) diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index b6d326b0a..75a29eea1 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -312,29 +312,33 @@ let coqtopInterpretToPoint params = let coqtopStepBackward params = let Notification.Client.StepBackwardParams.{ textDocument = { uri } } = params in - let st = Hashtbl.find states (DocumentUri.to_path uri) in - let (st, events) = Dm.DocumentManager.interpret_to_previous st in - let range = Dm.DocumentManager.observe_id_range st in - Hashtbl.replace states (DocumentUri.to_path uri) st; - update_view uri st; - match range with - | None -> - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] - | Some range -> - [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + match Hashtbl.find_opt states (DocumentUri.to_path uri) with + | None -> log "[stepForward] ignoring event on non existant document"; [] + | Some st -> + let (st, events) = Dm.DocumentManager.interpret_to_previous st in + let range = Dm.DocumentManager.observe_id_range st in + Hashtbl.replace states (DocumentUri.to_path uri) st; + update_view uri st; + match range with + | None -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + | Some range -> + [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] let coqtopStepForward params = let Notification.Client.StepForwardParams.{ textDocument = { uri } } = params in - let st = Hashtbl.find states (DocumentUri.to_path uri) in - let (st, events) = Dm.DocumentManager.interpret_to_next st in - let range = Dm.DocumentManager.observe_id_range st in - Hashtbl.replace states (DocumentUri.to_path uri) st; - update_view uri st; - match range with - | None -> - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] - | Some range -> - [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + match Hashtbl.find_opt states (DocumentUri.to_path uri) with + | None -> log "[stepBackward] ignoring event on non existant document"; [] + | Some st -> + let (st, events) = Dm.DocumentManager.interpret_to_next st in + let range = Dm.DocumentManager.observe_id_range st in + Hashtbl.replace states (DocumentUri.to_path uri) st; + update_view uri st; + match range with + | None -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + | Some range -> + [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] let make_CompletionItem i item : CompletionItem.t = let (label, insertText, typ, path) = Dm.CompletionItems.pp_completion_item item in