LSP

dune-project

@@ -19,7 +19,10 @@
   dune
   dune-build-info
   dune-site
+  logs
+  logs-fmt
   markdown
+  lsp
   (pcre2 (>= 8))
   (why3 (and (>= 1.8.0) (< 1.9)))
   yojson

easycrypt.opam

@@ -7,7 +7,10 @@ depends: [
   "dune" {>= "3.13"}
   "dune-build-info"
   "dune-site"
+  "logs"
+  "logs-fmt"
   "markdown"
+  "lsp"
   "pcre2" {>= "8"}
   "why3" {>= "1.8.0" & < "1.9"}
   "yojson"

src/dune

@@ -16,15 +16,15 @@
  (public_name easycrypt.ecLib)
  (foreign_stubs (language c) (names eunix))
  (modules :standard \ ec)
- (libraries batteries camlp-streams dune-build-info dune-site inifiles markdown markdown.html pcre2 tyxml why3 yojson zarith)
+ (libraries batteries camlp-streams dune-build-info dune-site inifiles logs logs.fmt lsp markdown markdown.html pcre2 tyxml why3 yojson zarith)
 )
 
 (executable
  (public_name easycrypt)
  (name ec)
  (modules ec)
  (promote (until-clean))
- (libraries batteries camlp-streams dune-build-info dune-site inifiles pcre2 why3 yojson zarith ecLib))
+(libraries batteries camlp-streams dune-build-info dune-site inifiles logs logs.fmt lsp pcre2 why3 yojson zarith ecLib))
 
 (ocamllex ecLexer)
 

src/ec.ml

@@ -214,6 +214,9 @@ let main () =
   (* Execution of eager commands *)
   begin
     match options.o_command with
+    | `Lsp ->
+        EcLsp.run ();
+        exit 0
     | `Runtest input -> begin
         let root =
           match EcRelocate.sourceroot with
@@ -535,6 +538,9 @@ let main () =
     | `Runtest _ ->
         (* Eagerly executed *)
         assert false
+    | `Lsp ->
+        (* Eagerly executed *)
+        assert false
 
     | `DocGen docopts -> begin
         let name = docopts.doco_input in

src/ecIo.ml

@@ -96,14 +96,15 @@ let from_string data =
 let finalize (ecreader : ecreader) =
   Disposable.dispose ecreader
 
+(* -------------------------------------------------------------------- *)
+let isfinal_token = function
+  | EcParser.FINAL _ -> true
+  | _ -> false
+
 (* -------------------------------------------------------------------- *)
 let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
   let lexbuf = ecreader.ecr_lexbuf in
 
-  let isfinal = function
-    | EcParser.FINAL _ -> true
-    | _ -> false in
-
   if ecreader.ecr_atstart then
     ecreader.ecr_trim <- ecreader.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum;
 
@@ -134,7 +135,7 @@ let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
 
   ecreader.ecr_tokens  <- prequeue @ queue;
 
-  if isfinal token then
+  if isfinal_token token then
     ecreader.ecr_atstart <- true
   else
     ecreader.ecr_atstart <- ecreader.ecr_atstart && (
@@ -177,6 +178,28 @@ let parse (ecreader : ecreader) : EcParsetree.prog =
 
   in parse (EcParser.Incremental.prog ecreader.ecr_lexbuf.lex_curr_p)
 
+(* -------------------------------------------------------------------- *)
+let next_sentence_from (text : string) (start : int) : (string * int * int) option =
+  let len = String.length text in
+  if start < 0 || start >= len then
+    None
+  else
+    let sub = String.sub text start (len - start) in
+    let reader = from_string sub in
+    let ecr = Disposable.get reader in
+    Fun.protect
+      ~finally:(fun () -> finalize reader)
+      (fun () ->
+        try
+          while not (isfinal_token (proj3_1 (lexer ecr))) do () done;
+
+          let p = ecr.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum - 1 in
+          let s = String.sub sub 0 p in
+
+          Some (s, start, start + p)
+        with
+        | EcLexer.LexicalError _ -> None)
+
 (* -------------------------------------------------------------------- *)
 let xparse (ecreader : ecreader) : string * EcParsetree.prog =
   let ecr = Disposable.get ecreader in

src/ecIo.mli

@@ -13,6 +13,7 @@ val parse    : ecreader -> EcParsetree.prog
 val parseall : ecreader -> EcParsetree.global list
 val drain    : ecreader -> unit
 val lexbuf   : ecreader -> Lexing.lexbuf
+val next_sentence_from : string -> int -> (string * int * int) option
 
 (* -------------------------------------------------------------------- *)
 val lex_single_token : string -> EcParser.token option