From 2c886bfc461e20910a84f77c6a9205fb57e2f64f Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Thu, 25 Apr 2024 13:22:55 +0200
Subject: [PATCH] Adding optcomp

---
 language-server/dm/document.ml | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
index 22e9dd3e4..dfbe6c6d6 100644
--- a/language-server/dm/document.ml
+++ b/language-server/dm/document.ml
@@ -288,14 +288,24 @@ let parse_one_sentence stream ~st =
   (* FIXME: handle proof mode correctly *)
   *)
 
+
+[%%if coq = "8.18" || coq = "8.19"]
+let parse_one_sentence stream ~st =
+  Vernacstate.Synterp.unfreeze st;
+  let entry = Pvernac.main_entry (Some (Synterp.get_default_proof_mode ())) in
+  let pa = Pcoq.Parsable.make stream in
+  let sentence = Pcoq.Entry.parse entry pa in
+  (sentence, [])
+[%%else]
 let parse_one_sentence stream ~st =
   Vernacstate.Synterp.unfreeze st;
   Flags.record_comments := true;
   let entry = Pvernac.main_entry (Some (Synterp.get_default_proof_mode ())) in
   let pa = Pcoq.Parsable.make stream in
-    let sentence = Pcoq.Entry.parse entry pa in
-    let comments = Pcoq.Parsable.comments pa in
-    (sentence, comments)
+  let sentence = Pcoq.Entry.parse entry pa in
+  let comments = Pcoq.Parsable.comments pa in
+  (sentence, comments)
+[%%endif]
 
 let rec junk_sentence_end stream =
   match Stream.npeek () 2 stream with
@@ -438,9 +448,6 @@ let validate_document ({ parsed_loc; raw_doc; } as document) =
   let parsing_errors_by_end =
     List.fold_left (fun acc (error : parsing_error) -> LM.add error.stop error acc) errors new_errors
   in
-  log @@ "PARSED NEW COMMENTS: ";
-  List.iter (fun (comment: comment) -> log @@ Format.sprintf "[start: %i, stop: %i, comment %s]" comment.start comment.stop comment.content) new_comments;
-  log @@ "------------------";
   let comments_by_end =
     List.fold_left (fun acc (comment : comment) -> LM.add comment.stop comment acc) comments new_comments
   in