Merge pull request #775 from ejgallego/skip_vofile

[coq] Adapt to coq/coq#17393

language-server/dm/document.ml

@@ -332,6 +332,13 @@ let get_loc_from_info_or_exn exn =
   Loc.get_loc @@ info
 [%%endif]
 
+[%%if coq = "8.18" || coq = "8.19"]
+let get_entry ast = Synterp.synterp_control ast
+[%%else]
+let get_entry ast =
+  let intern = Vernacinterp.fs_intern in
+  Synterp.synterp_control ~intern ast
+[%%endif]
 
 let rec parse_more synterp_state stream raw parsed parsed_comments errors =
   let handle_parse_error start msg =
@@ -361,7 +368,7 @@ let rec parse_more synterp_state stream raw parsed parsed_comments errors =
       let tokens = stream_tok 0 [] lex begin_line begin_char in
       begin
         try
-          let entry = Synterp.synterp_control ast in
+          let entry = get_entry ast in
           let classification = Vernac_classifier.classify_vernac ast in
           let synterp_state = Vernacstate.Synterp.freeze () in
           let sentence = { parsing_start = start; ast = { ast = entry; classification; tokens }; start = begin_char; stop; synterp_state } in

language-server/dm/documentManager.ml

@@ -312,12 +312,20 @@ let validate_document state =
       ) state.execution_state (Stateid.Set.elements invalid_roots) in
   { state with document; execution_state; observe_id }
 
+[%%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]
+
 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
   in
-  Coqinit.start_library ~top opts;
+  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