package vscoq-language-server
VSCoq language server
Install
Dune Dependency
Authors
Maintainers
Sources
vscoq-language-server-2.2.6.tar.gz
md5=f528c1760966ac10d48b5f1c5531411a
sha512=1f69538ae5f78854b34e3f1a9d408714843e899bb96d063c2bfac410339b6a13ee5f30d5e7b3cd2bbd673169bcfdb550153ba741092cdc3ee3a8ca6446cc2240
doc/src/vscoq-language-server.dm/documentManager.ml.html
Source file documentManager.ml
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002
(**************************************************************************) (* *) (* VSCoq *) (* *) (* Copyright INRIA and contributors *) (* (see version control and README file for authors & dates) *) (* *) (**************************************************************************) (* *) (* This file is distributed under the terms of the MIT License. *) (* See LICENSE file. *) (* *) (**************************************************************************) [%%import "vscoq_config.mlh"] open Lsp.Types open Protocol open Protocol.LspWrapper open Protocol.ExtProtocol open Protocol.Printing open Types let Log log = Log.mk_log "documentManager" type observe_id = Id of Types.sentence_id | Top type blocking_error = { last_range: Range.t; error_range: Range.t } let to_sentence_id = function | Top -> None | Id id -> Some id type document_state = | Parsing | Parsed (* | Executing of sentence_id TODO: ADD EXEDCUTING STATE | Executed of sentence_id *) type state = { uri : DocumentUri.t; init_vs : Vernacstate.t; opts : Coqargs.injection_command list; document : Document.document; execution_state : ExecutionManager.state; observe_id : observe_id; cancel_handle : Sel.Event.cancellation_handle option; document_state: document_state; } type event = | Execute of { (* we split the computation to help interruptibility *) id : Types.sentence_id; (* sentence of interest *) vst_for_next_todo : Vernacstate.t; (* the state to be used for the next todo, it is not necessarily the state of the last sentence, since it may have failed and this is a surrogate used for error resiliancy *) task : ExecutionManager.prepared_task; started : float; (* time *) } | ExecutionManagerEvent of ExecutionManager.event | ParseBegin | Observe of Types.sentence_id | SendProofView of (Types.sentence_id option) | DocumentEvent of Document.event | SendBlockOnError of Types.sentence_id | SendMoveCursor of Range.t type handled_event = { state : state option; events: event Sel.Event.t list; update_view: bool; notification: Notification.Server.t option; } let pp_event fmt = function | Execute { id; started; _ } -> let time = Unix.gettimeofday () -. started in Stdlib.Format.fprintf fmt "ExecuteToLoc %d (started %2.3f ago)" (Stateid.to_int id) time | ExecutionManagerEvent _ -> Stdlib.Format.fprintf fmt "ExecutionManagerEvent" | ParseBegin -> Stdlib.Format.fprintf fmt "ParseBegin" | Observe id -> Stdlib.Format.fprintf fmt "Observe %d" (Stateid.to_int id) | SendProofView id_opt -> Stdlib.Format.fprintf fmt "SendProofView %s" @@ (Option.cata Stateid.to_string "None" id_opt) | DocumentEvent event -> Stdlib.Format.fprintf fmt "DocumentEvent event: "; Document.pp_event fmt event | SendBlockOnError id -> Stdlib.Format.fprintf fmt "SendBlockOnError %d" @@ (Stateid.to_int id) | SendMoveCursor range -> Stdlib.Format.fprintf fmt "SendBlockOnError %s" @@ (Range.to_string range) let inject_em_event x = Sel.Event.map (fun e -> ExecutionManagerEvent e) x let inject_em_events events = List.map inject_em_event events let inject_doc_event x = Sel.Event.map (fun e -> DocumentEvent e) x let inject_doc_events events = List.map inject_doc_event events let mk_proof_view_event id = Sel.now ~priority:PriorityManager.proof_view (SendProofView (Some id)) let mk_proof_view_event_empty = Sel.now ~priority:PriorityManager.proof_view (SendProofView None) let mk_observe_event id = Sel.now ~priority:PriorityManager.execution (Observe id) let mk_move_cursor_event id = let priority = PriorityManager.move_cursor in Sel.now ~priority @@ SendMoveCursor id let mk_block_on_error_event last_range error_id background = let update_goal_view = [mk_proof_view_event error_id] in if background then update_goal_view else let red_flash = [Sel.now ~priority:PriorityManager.move_cursor @@ SendBlockOnError error_id] in let move_cursor = match last_range with | Some last_range -> [mk_move_cursor_event last_range] | None -> [] in red_flash @ move_cursor @ update_goal_view type events = event Sel.Event.t list let executed_ranges st mode = match st.observe_id, mode with | _, Settings.Mode.Continuous -> ExecutionManager.overview st.execution_state | Top, Settings.Mode.Manual -> empty_overview | Id id, Settings.Mode.Manual -> let range = Document.range_of_id st.document id in ExecutionManager.overview_until_range st.execution_state range let observe_id_range st = let doc = Document.raw_document st.document in match st.observe_id with | Top -> None | 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 Some range let is_parsing st = st.document_state = Parsing [%%if lsp < (1,19,0) ] let message_of_string x = x [%%else] let message_of_string x = `String x [%%endif] let make_diagnostic doc range oloc message severity code = let range = match oloc with | None -> range | Some loc -> RawDocument.range_of_loc (Document.raw_document doc) loc in let code, data = match code with | None -> None, None | Some (x,z) -> Some x, Some z in Diagnostic.create ?code ?data ~range ~message:(message_of_string message) ~severity () let mk_diag st (id,(lvl,oloc,qf,msg)) = let code = match qf with | [] -> None | qf -> let code : Jsonrpc.Id.t * Lsp.Import.Json.t = let open Lsp.Import.Json in (`String "quickfix-replace", qf |> yojson_of_list (fun qf -> let s = Pp.string_of_ppcmds @@ Quickfix.pp qf in let loc = Quickfix.loc qf in let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in QuickFixData.yojson_of_t (QuickFixData.{range; text = s}) )) in Some code in let lvl = DiagnosticSeverity.of_feedback_level lvl in make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code let mk_error_diag st (id,(oloc,msg,qf)) = (* mk_diag st (id,(Feedback.Error,oloc, msg)) *) let code = match qf with | None -> None | Some qf -> let code : Jsonrpc.Id.t * Lsp.Import.Json.t = let open Lsp.Import.Json in (`String "quickfix-replace", qf |> yojson_of_list (fun qf -> let s = Pp.string_of_ppcmds @@ Quickfix.pp qf in let loc = Quickfix.loc qf in let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in QuickFixData.yojson_of_t (QuickFixData.{range; text = s}) )) in Some code in let lvl = DiagnosticSeverity.of_feedback_level Feedback.Error in make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code let mk_parsing_error_diag st Document.{ msg = (oloc,msg); start; stop; qf } = let doc = Document.raw_document st.document in let severity = DiagnosticSeverity.Error in let start = RawDocument.position_of_loc doc start in let end_ = RawDocument.position_of_loc doc stop in let range = Range.{ start; end_ } in let code = match qf with | None -> None | Some qf -> let code : Jsonrpc.Id.t * Lsp.Import.Json.t = let open Lsp.Import.Json in (`String "quickfix-replace", qf |> yojson_of_list (fun qf -> let s = Pp.string_of_ppcmds @@ Quickfix.pp qf in let loc = Quickfix.loc qf in let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in QuickFixData.yojson_of_t (QuickFixData.{range; text = s}) )) in Some code in make_diagnostic st.document range oloc (Pp.string_of_ppcmds msg) severity code let all_diagnostics st = let parse_errors = Document.parse_errors st.document in let all_exec_errors = ExecutionManager.all_errors st.execution_state in let all_feedback = ExecutionManager.all_feedback st.execution_state in (* we are resilient to a state where invalidate was not called yet *) let exists (id,_) = Option.has_some (Document.get_sentence st.document id) in let not_info (_, (lvl, _, _, _)) = match lvl with | Feedback.Info -> false | _ -> true in let exec_errors = all_exec_errors |> List.filter exists in let feedback = all_feedback |> List.filter exists |> List.filter not_info in List.map (mk_parsing_error_diag st) parse_errors @ List.map (mk_error_diag st) exec_errors @ List.map (mk_diag st) feedback let id_of_pos st pos = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match Document.find_sentence_before st.document loc with | None -> None | Some { id } -> Some id let id_of_sentence_after_pos st pos = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in (* if the current loc falls squarely within a sentence *) match Document.find_sentence st.document loc with | Some { id } -> Some id | None -> (** otherwise the sentence start is after the loc, so we must be in the whitespace before the sentence and need to interpret to the sentence before instead *) match Document.find_sentence_before st.document loc with | None -> None | Some { id } -> Some id let id_of_pos_opt st = function | None -> begin match st.observe_id with Top -> None | Id id -> Some id end | Some pos -> id_of_pos st pos let get_messages st id = let error = ExecutionManager.error st.execution_state id in let feedback = ExecutionManager.feedback st.execution_state id in let feedback = List.map (fun (lvl,_oloc,_,msg) -> DiagnosticSeverity.of_feedback_level lvl, pp_of_coqpp msg) feedback in match error with | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback | None -> feedback let get_info_messages st pos = match id_of_pos_opt st pos with | None -> log (fun () -> "get_messages: Could not find id");[] | Some id -> log (fun () -> "get_messages: Found id"); let info (lvl, _, _, _) = match lvl with | Feedback.Info -> true | _ -> false in let feedback = ExecutionManager.feedback st.execution_state id in let feedback = feedback |> List.filter info in List.map (fun (lvl,_oloc,_,msg) -> DiagnosticSeverity.of_feedback_level lvl, pp_of_coqpp msg) feedback let create_execution_event background event = let priority = if background then None else Some PriorityManager.execution in Sel.now ?priority event let state_before_error state error_id loc = match Document.get_sentence state.document error_id with | None -> state, None | Some { start } -> let errored_sentence_range = Document.range_of_id_with_blank_space state.document error_id in let error_range = Option.cata (fun loc -> RawDocument.range_of_loc (Document.raw_document state.document) loc) errored_sentence_range loc in match Document.find_sentence_before state.document start with | None -> let observe_id = Top in {state with observe_id}, Some error_range | Some { id } -> let observe_id = (Id id) in {state with observe_id}, Some error_range let observe ~background state id ~should_block_on_error : (state * event Sel.Event.t list) = match Document.get_sentence state.document id with | None -> state, [] (* TODO error? *) | Some { id } -> Option.iter Sel.Event.cancel state.cancel_handle; let vst_for_next_todo, execution_state, task, error_id = ExecutionManager.build_tasks_for state.document (Document.schedule state.document) state.execution_state id should_block_on_error in match task with | Some task -> (* task will only be Some if there is no error *) let event = create_execution_event background (Execute {id; vst_for_next_todo; task; started = Unix.gettimeofday ()}) in let cancel_handle = Some (Sel.Event.get_cancellation_handle event) in {state with execution_state; cancel_handle}, [event] | None -> match error_id with | None -> {state with execution_state}, [] | Some (error_id, loc) -> let state, error_range = state_before_error state error_id loc in let events = mk_block_on_error_event error_range error_id background in {state with execution_state}, events let reset_to_top st = { st with observe_id = Top } let get_document_proofs st = let outline = Document.outline st.document in let is_theorem Document.{ type_ } = match type_ with | TheoremKind -> true | _ -> false in let mk_proof_block Document.{statement; proof; range } = let statement = ProofState.mk_proof_statement statement range in let last_step = List.hd proof in let proof = List.rev proof in let fst_step = List.hd proof in let range = Range.create ~start:fst_step.range.start ~end_:last_step.range.end_ in let steps = List.map (fun Document.{tactic; range} -> ProofState.mk_proof_step tactic range) proof in ProofState.mk_proof_block statement steps range in let proofs, _ = List.partition is_theorem outline in List.map mk_proof_block proofs let to_document_symbol elem = let Document.{name; statement; range; type_} = elem in let kind = begin match type_ with | TheoremKind -> SymbolKind.Function | DefinitionType -> SymbolKind.Variable | InductiveType -> SymbolKind.Struct | Other -> SymbolKind.Null | BeginSection | BeginModule -> SymbolKind.Class | End -> SymbolKind.Null end in DocumentSymbol.{name; detail=(Some statement); kind; range; selectionRange=range; children=None; deprecated=None; tags=None;} let rec get_document_symbols outline (sec_or_m: DocumentSymbol.t list) symbols = let add_child (s_father: DocumentSymbol.t) s_child = let children = match s_father.children with | None -> Some [s_child] | Some l -> Some (l @ [s_child]) in {s_father with children} in let record_in_outline outline symbol sec_or_m = match sec_or_m with | [] -> let symbols = symbols @ [symbol] in get_document_symbols outline sec_or_m symbols | s :: l -> let s = add_child s symbol in get_document_symbols outline (s::l) symbols in match outline with | [] -> symbols | e :: l -> let Document.{type_} = e in match type_ with | TheoremKind | DefinitionType | InductiveType | Other -> let symbol = to_document_symbol e in record_in_outline l symbol sec_or_m | BeginSection -> let symbol = to_document_symbol e in get_document_symbols l (symbol :: sec_or_m) symbols | BeginModule -> let symbol = to_document_symbol e in get_document_symbols l (symbol :: sec_or_m) symbols | End -> match sec_or_m with | [] -> log(fun () -> "Trying to end a module or section with no begin"); get_document_symbols l [] symbols | symbol :: s_l -> match s_l with | [] -> get_document_symbols l s_l (symbols @ [symbol]) | s_parent :: s_l -> let s = add_child s_parent symbol in get_document_symbols l (s :: s_l) symbols let get_document_symbols st = let outline = List.rev @@ Document.outline st.document in get_document_symbols outline [] [] let interpret_to st id check_mode = let observe_id = (Id id) in let st = { st with observe_id} in match check_mode with | Settings.Mode.Manual -> let event = mk_observe_event id in let pv_event = mk_proof_view_event id in st, [event] @ [pv_event] | Settings.Mode.Continuous -> match ExecutionManager.is_locally_executed st.execution_state id with | true -> st, [mk_proof_view_event id] | false -> st, [] let interpret_to_next_position st pos check_mode = match id_of_sentence_after_pos st pos with | None -> (st, []) (* document is empty *) | Some id -> let st, events = interpret_to st id check_mode in (st, events) let interpret_to_position st pos check_mode ~point_interp_mode = match point_interp_mode with | Settings.PointInterpretationMode.Cursor -> begin match id_of_pos st pos with | None -> (st, []) (* document is empty *) | Some id -> interpret_to st id check_mode end | Settings.PointInterpretationMode.NextCommand -> interpret_to_next_position st pos check_mode let get_next_range st pos = match id_of_pos st pos with | None -> None | Some id -> match Document.get_sentence st.document id with | None -> None | Some { stop } -> match Document.find_sentence_after st.document (stop+1) with | None -> Some (Document.range_of_id st.document id) | Some { id } -> Some (Document.range_of_id st.document id) let get_previous_range st pos = match id_of_pos st pos with | None -> None | Some id -> match Document.get_sentence st.document id with | None -> None | Some { start } -> match Document.find_sentence_before st.document (start) with | None -> Some (Document.range_of_id st.document id) | Some { id } -> Some (Document.range_of_id st.document id) let interpret_to_previous st check_mode = match st.observe_id with | Top -> (st, []) | (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; let range = Range.top () in { st with observe_id=Top }, [mk_move_cursor_event range; mk_proof_view_event_empty] | Some { id } -> let st, events = interpret_to st id check_mode in let range = Document.range_of_id st.document id in let mv_cursor = mk_move_cursor_event range in st, [mv_cursor] @ events let interpret_to_next st check_mode = match st.observe_id with | Top -> begin match Document.get_first_sentence st.document with | None -> st, [] (*The document is empty*) | Some { id } -> let st, events = interpret_to st id check_mode in let range = Document.range_of_id st.document id in let mv_cursor = mk_move_cursor_event range in st, [mv_cursor] @ events end | 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 } -> let st, events = interpret_to st id check_mode in let range = Document.range_of_id st.document id in let mv_cursor = mk_move_cursor_event range in st, [mv_cursor] @ events let interpret_to_end st check_mode = match Document.get_last_sentence st.document with | None -> (st, []) | Some {id} -> log (fun () -> "interpret_to_end id = " ^ Stateid.to_string id); interpret_to st id check_mode let interpret_in_background st ~should_block_on_error = match Document.get_last_sentence st.document with | None -> (st, []) | Some {id} -> log (fun () -> "interpret_to_end id = " ^ Stateid.to_string id); observe ~background:true st id ~should_block_on_error let is_above st id1 id2 = let range1 = Document.range_of_id st id1 in let range2 = Document.range_of_id st id2 in Position.compare range1.start range2.start < 0 let validate_document state (Document.{unchanged_id; invalid_ids; previous_document; parsed_document}) = let state = {state with document=parsed_document} in let observe_id = match unchanged_id, state.observe_id with | None, Id _ -> Top | _, Top -> Top | Some id, Id id' -> if is_above previous_document id id' then (Id id) else state.observe_id in let execution_state = List.fold_left (fun st id -> ExecutionManager.invalidate previous_document (Document.schedule previous_document) id st ) state.execution_state (Stateid.Set.elements invalid_ids) in let execution_state = ExecutionManager.reset_overview execution_state previous_document in { state with execution_state; observe_id; document_state = Parsed } [%%if coq = "8.18" || coq = "8.19"] let start_library top opts = Coqinit.start_library ~top opts [%%else] let start_library top opts = let intern = Vernacinterp.fs_intern in Coqinit.start_library ~intern ~top opts; [%%endif] [%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] let dirpath_of_top = Coqargs.dirpath_of_top [%%else] let dirpath_of_top = Coqinit.dirpath_of_top [%%endif] let init init_vs ~opts uri ~text = Vernacstate.unfreeze_full_state init_vs; let top = try (dirpath_of_top (TopPhysical (DocumentUri.to_path uri))) with e -> raise e in start_library top opts; 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 state = { uri; opts; init_vs; document; execution_state; observe_id=Top; cancel_handle = None; document_state = Parsing } in let priority = Some PriorityManager.launch_parsing in let event = Sel.now ?priority ParseBegin in state, [event] @ [inject_em_event feedback] let reset { uri; opts; init_vs; document; execution_state; } = 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 observe_id = Top in let state = { uri; opts; init_vs; document; execution_state; observe_id; cancel_handle = None ; document_state = Parsing } in let priority = Some PriorityManager.launch_parsing in let event = Sel.now ?priority ParseBegin in state, [event] @ [inject_em_event feedback] let apply_text_edits state edits = let apply_edit_and_shift_diagnostics_locs_and_overview state (range, new_text as edit) = let document = Document.apply_text_edit state.document edit in let exec_st = state.execution_state in let edit_start = RawDocument.loc_of_position (Document.raw_document state.document) range.Range.start in let edit_stop = RawDocument.loc_of_position (Document.raw_document state.document) range.Range.end_ in let edit_length = edit_stop - edit_start in let exec_st = ExecutionManager.shift_diagnostics_locs exec_st ~start:edit_stop ~offset:(String.length new_text - edit_length) in let execution_state = ExecutionManager.shift_overview exec_st ~before:(Document.raw_document state.document) ~after:(Document.raw_document document) ~start:edit_stop ~offset:(String.length new_text - edit_length) in {state with execution_state; document} in let state = List.fold_left apply_edit_and_shift_diagnostics_locs_and_overview state edits in let priority = Some PriorityManager.launch_parsing in let sel_event = Sel.now ?priority ParseBegin in state, [sel_event] let execution_finished st id started = let time = Unix.gettimeofday () -. started in log (fun () -> Printf.sprintf "ExecuteToLoc %d ends after %2.3f" (Stateid.to_int id) time); (* We update the state to trigger a publication of diagnostics *) let update_view = true in let state = Some st in {state; events=[]; update_view; notification=None} let execute st id vst_for_next_todo started task background block = let time = Unix.gettimeofday () -. started in let proof_view_event = (*When in continuous mode we always check if we should update the goal view *) if background then begin match st.observe_id with | Top -> [] | Id o_id -> let s_id = ExecutionManager.get_id_of_executed_task task in if o_id = s_id then [mk_proof_view_event s_id] else [] end else [] in match Document.get_sentence st.document id with | None -> log (fun () -> Printf.sprintf "ExecuteToLoc %d stops after %2.3f, sentences invalidated" (Stateid.to_int id) time); {state=Some st; events=[]; update_view=true; notification=None} (* Sentences have been invalidate, probably because the user edited while executing *) | Some _ -> log (fun () -> Printf.sprintf "ExecuteToLoc %d continues after %2.3f" (Stateid.to_int id) time); let (next, execution_state,vst_for_next_todo,events, exec_error) = ExecutionManager.execute st.execution_state st.document (vst_for_next_todo, [], false) task block in let st, block_events = match exec_error with | None -> st, [] | Some (error_id, loc) -> let st, error_range = state_before_error st error_id loc in let events = if block then mk_block_on_error_event error_range error_id background else [] in st, events in let event = Option.map (fun task -> create_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in match event, block_events with | None, [] -> execution_finished { st with execution_state } id started (* There is no new tasks, and no errors -> execution finished *) | _ -> let cancel_handle = Option.map Sel.Event.get_cancellation_handle event in let event = Option.cata (fun event -> [event]) [] event in let state = Some {st with execution_state; cancel_handle} in let update_view = true in let events = proof_view_event @ inject_em_events events @ block_events @ event in {state; events; update_view; notification=None} let get_proof st diff_mode id = let previous_st id = 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 observe_id = to_sentence_id st.observe_id in let oid = Option.append id observe_id 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) let handle_execution_manager_event st ev = let id, execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in let st = match (id, execution_state_update) with | Some id, Some exec_st -> let execution_state = ExecutionManager.update_processed id exec_st st.document in Some {st with execution_state} | Some id, None -> let execution_state = ExecutionManager.update_processed id st.execution_state st.document in Some {st with execution_state} | _, _ -> Option.map (fun execution_state -> {st with execution_state}) execution_state_update in let update_view = true in {state=st; events=(inject_em_events events); update_view; notification=None} let handle_event ev st ~block check_mode diff_mode = let background = check_mode = Settings.Mode.Continuous in match ev with | Execute { id; vst_for_next_todo; started; task } -> execute st id vst_for_next_todo started task background block | ExecutionManagerEvent ev -> handle_execution_manager_event st ev | Observe id -> let update_view = true in let st, events = observe st id ~should_block_on_error:block ~background in {state=Some st; events; update_view; notification=None} | ParseBegin -> let document, events = Document.validate_document st.document in let update_view = true in let state = Some {st with document} in let events = inject_doc_events events in {state; events; update_view; notification=None} | DocumentEvent ev -> let document, events, parsing_end_info = Document.handle_event st.document ev in begin match parsing_end_info with | None -> let update_view = false in let state = Some {st with document} in let events = inject_doc_events events in {state; events; update_view; notification=None} | Some parsing_end_info -> let st = validate_document st parsing_end_info in let update_view = true in if background then let (st, events) = interpret_in_background st ~should_block_on_error:block in {state=(Some st); events; update_view; notification=None} else {state=(Some st); events=[]; update_view; notification=None} end | SendProofView (Some id) -> let proof = get_proof st diff_mode (Some id) in let messages = get_messages st id in let params = Notification.Server.ProofViewParams.{ proof; messages} in let notification = Some (Notification.Server.ProofView params) in let update_view = true in {state=(Some st); events=[]; update_view; notification} | SendProofView None -> let params = Notification.Server.ProofViewParams.{ proof=None; messages=[] } in let notification = Some (Notification.Server.ProofView params) in let update_view = true in {state=(Some st); events=[]; update_view; notification} | SendBlockOnError id -> let {uri} = st in let range = Document.range_of_id st.document id in let notification = Some (Notification.Server.BlockOnError {uri; range}) in {state=(Some st); events=[]; update_view=false; notification} | SendMoveCursor range -> let {uri} = st in let notification = Some (Notification.Server.MoveCursor {uri; range}) in {state=(Some st); events=[]; update_view=false; notification} let context_of_id st = function | None -> Some (ExecutionManager.get_initial_context st.execution_state) | Some id -> ExecutionManager.get_context st.execution_state id (** Get context at the start of the sentence containing [pos] *) let get_context st pos = context_of_id st (id_of_pos st pos) let get_completions st pos = match id_of_pos st pos with | None -> log (fun () -> "Can't get completions, no sentence found before the cursor"); [] | Some id -> let ost = ExecutionManager.get_vernac_state st.execution_state id in let settings = ExecutionManager.get_options () in match Option.bind ost @@ CompletionSuggester.get_completions settings.completion_options with | None -> log (fun () -> "No completions available"); [] | Some lemmas -> lemmas [%%if coq = "8.18" || coq = "8.19"] [%%elif coq = "8.20"] let parsable_make = Pcoq.Parsable.make let unfreeze = Pcoq.unfreeze let entry_parse = Pcoq.Entry.parse [%%else] let parsable_make = Procq.Parsable.make let unfreeze = Procq.unfreeze let entry_parse = Procq.Entry.parse [%%endif] [%%if coq = "8.18" || coq = "8.19"] let parse_entry st pos entry pattern = let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string pattern) in let st = match Document.find_sentence_before st.document pos with | None -> st.init_vs.Vernacstate.synterp.parsing | Some { synterp_state } -> synterp_state.Vernacstate.Synterp.parsing in Vernacstate.Parser.parse st entry pa [%%else] let parse_entry st pos entry pattern = let pa = parsable_make (Gramlib.Stream.of_string pattern) in let st = match Document.find_sentence_before st.document pos with | None -> Vernacstate.(Synterp.parsing st.init_vs.synterp) | Some { synterp_state } -> Vernacstate.Synterp.parsing synterp_state in unfreeze st; entry_parse entry pa [%%endif] [%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] let smart_global = Pcoq.Prim.smart_global [%%else] let smart_global = Procq.Prim.smart_global [%%endif] let about st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with | None -> Error ({message="No context found"; code=None}) (*TODO execute *) | Some (sigma, env) -> try let ref_or_by_not = parse_entry st loc (smart_global) pattern in let udecl = None (* TODO? *) in Ok (pp_of_coqpp @@ Prettyp.print_about env sigma ref_or_by_not udecl) with e -> let e, info = Exninfo.capture e in let message = Pp.string_of_ppcmds @@ CErrors.iprint (e, info) in Error ({message; code=None}) let search st ~id pos pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with | None -> [] (* TODO execute? *) | Some (sigma, env) -> let query, r = parse_entry st loc (G_vernac.search_queries) pattern in SearchQuery.interp_search ~id env sigma query r (** Try to generate hover text from [pattern] the context of the given [sentence] *) let hover_of_sentence st loc pattern sentence = match context_of_id st (Option.map (fun ({ id; _ }: Document.sentence) -> id) sentence) with | None -> log (fun () -> "hover: no context found"); None | Some (sigma, env) -> try let ref_or_by_not = parse_entry st loc (smart_global) pattern in Language.Hover.get_hover_contents env sigma ref_or_by_not with e -> let e, info = Exninfo.capture e in log (fun () -> "Exception while handling hover: " ^ (Pp.string_of_ppcmds @@ CErrors.iprint (e, info))); None let hover st pos = (* Tries to get hover at three difference places: - At the start of the current sentence - At the start of the next sentence (for symbols defined in the current sentence) e.g. Definition, Inductive - At the next QED (for symbols defined after proof), if the next sentence is in proof mode e.g. Lemmas, Definition with tactics *) let opattern = RawDocument.word_at_position (Document.raw_document st.document) pos in match opattern with | None -> log (fun () -> "hover: no word found at cursor"); None | Some pattern -> log (fun () -> "hover: found word at cursor: \"" ^ pattern ^ "\""); let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in (* hover at previous sentence *) match hover_of_sentence st loc pattern (Document.find_sentence_before st.document loc) with | Some _ as x -> x | None -> match Document.find_sentence_after st.document loc with | None -> None (* Skip if no next sentence *) | Some sentence as opt -> (* hover at next sentence *) match hover_of_sentence st loc pattern opt with | Some _ as x -> x | None -> match sentence.ast with | Error _ -> None | Parsed ast -> match ast.classification with (* next sentence in proof mode, hover at qed *) | VtProofStep _ | VtStartProof _ -> hover_of_sentence st loc pattern (Document.find_next_qed st.document loc) | _ -> None [%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] let lconstr = Pcoq.Constr.lconstr [%%else] let lconstr = Procq.Constr.lconstr [%%endif] [%%if coq = "8.18" || coq = "8.19" || coq = "8.20"] let jump_to_definition _ _ = None [%%else] let jump_to_definition st pos = let raw_doc = Document.raw_document st.document in let loc = RawDocument.loc_of_position raw_doc pos in let opattern = RawDocument.word_at_position raw_doc pos in match opattern with | None -> log (fun () -> "jumpToDef: no word found at cursor"); None | Some pattern -> log (fun () -> "jumpToDef: found word at cursor: \"" ^ pattern ^ "\""); try let qid = parse_entry st loc (Procq.Prim.qualid) pattern in let ref = Nametab.locate_extended qid in match Nametab.cci_src_loc ref with | None -> None | Some loc -> begin match loc.Loc.fname with | Loc.ToplevelInput | InFile { dirpath = None } -> None | InFile { dirpath = Some dp } -> let f = Loadpath.locate_absolute_library @@ Libnames.dirpath_of_string dp in begin match f with | Ok f -> let f = Filename.remove_extension f ^ ".v" in (if Sys.file_exists f then let b_pos = Position.create ~character:(loc.bp - loc.bol_pos) ~line:(loc.line_nb - 1) in let e_pos = Position.create ~character:(loc.ep - loc.bol_pos) ~line:(loc.line_nb - 1) in let range = Range.create ~end_:b_pos ~start:e_pos in Some (range, f) else None ) | Error _ -> None end end with e -> let e, info = Exninfo.capture e in log (fun () -> Pp.string_of_ppcmds @@ CErrors.iprint (e, info)); None [%%endif] let check st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with | None -> Error ({message="No context found"; code=None}) (*TODO execute *) | Some (sigma,env) -> let rc = parse_entry st loc lconstr pattern in try let redexpr = None in Ok (pp_of_coqpp @@ Vernacentries.check_may_eval env sigma redexpr rc) with e -> let e, info = Exninfo.capture e in let message = Pp.string_of_ppcmds @@ CErrors.iprint (e, info) in Error ({message; code=None}) [%%if coq = "8.18" || coq = "8.19"] let print_located_qualid _ qid = Prettyp.print_located_qualid qid [%%else] let print_located_qualid = Prettyp.print_located_qualid [%%endif] let locate st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with | None -> Error ({message="No context found"; code=None}) (*TODO execute *) | Some (sigma, env) -> match parse_entry st loc (smart_global) pattern with | { v = AN qid } -> Ok (pp_of_coqpp @@ print_located_qualid env qid) | { v = ByNotation (ntn, sc)} -> Ok( pp_of_coqpp @@ Notation.locate_notation (Constrextern.without_symbols (Printer.pr_glob_constr_env env sigma)) ntn sc) [%%if coq = "8.18" || coq = "8.19"] let print_name = Prettyp.print_name [%%else] let print_name = let access = Library.indirect_accessor[@@warning "-3"] in Prettyp.print_name access [%%endif] let print st pos ~pattern = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in match get_context st pos with | None -> Error({message="No context found"; code=None}) | Some (sigma, env) -> let qid = parse_entry st loc (smart_global) pattern in let udecl = None in (*TODO*) Ok ( pp_of_coqpp @@ print_name env sigma qid udecl ) (* Ignore nested proofs option (lives in STM) instead of failing with anomaly when it is set in a .vo we Require. cf #1060 *) let warn_nested_proofs_opt = CWarnings.create ~name:"vscoq-nested-proofs-flag" Pp.(fun () -> str "Flag \"Nested Proofs Allowed\" is ignored by VsCoq.") let () = Goptions.declare_bool_option { optstage = Summary.Stage.Interp; optdepr = None; optkey = Vernac_classifier.stm_allow_nested_proofs_option_name; optread = (fun () -> false); optwrite = (fun b -> if b then warn_nested_proofs_opt ()) } module Internal = struct let document st = st.document let raw_document st = Document.raw_document st.document let execution_state st = st.execution_state let observe_id st = match st.observe_id with | Top -> None | (Id id) -> Some id let validate_document st parsing_end_info = validate_document st parsing_end_info let string_of_state st = let code_lines_by_id = Document.code_lines_sorted_by_loc st.document in let code_lines_by_end = Document.code_lines_by_end_sorted_by_loc st.document in let string_of_state id = if ExecutionManager.is_locally_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_item item = Document.Internal.string_of_item item ^ " " ^ match item with | Sentence { id } -> string_of_state id | ParsingError _ -> "(error)" | Comment _ -> "(comment)" in let string_by_id = String.concat "\n" @@ List.map string_of_item code_lines_by_id in let string_by_end = String.concat "\n" @@ List.map string_of_item code_lines_by_end in String.concat "\n" ["Document using sentences_by_id map\n"; string_by_id; "\nDocument using sentences_by_end map\n"; string_by_end] let inject_doc_events = inject_doc_events end
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>