[petanque] Allow clients to set file contents

controller/lsp_core.ml

@@ -442,7 +442,7 @@ let petanque_handle ~token =
   let open Petanque_json in
   function
   | Interp.Action.Now handler -> Rq.Action.now (handler ~token)
-  | Interp.Action.Doc { uri; handler } ->
+  | Interp.Action.Doc { uri; contents = _; handler } ->
     (* Request document execution if not ready *)
     let postpone = true in
     Rq.Action.(Data (DocRequest { uri; postpone; handler }))

petanque/json/interp.ml

@@ -16,6 +16,7 @@ module Action = struct
     | Now of (token:Coq.Limits.Token.t -> Yojson.Safe.t r)
     | Doc of
         { uri : Lang.LUri.File.t
+        ; contents : string option
         ; handler :
             token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> Yojson.Safe.t r
         }
@@ -38,9 +39,9 @@ let do_request (module R : Protocol.Request.S) ~params =
     | Immediate handler ->
       Action.Now (fun ~token -> handler ~token params |> of_pet)
     | FullDoc { uri_fn; handler } ->
-      let uri = uri_fn params in
+      let uri, contents = uri_fn params in
       let handler ~token ~doc = handler ~token ~doc params |> of_pet in
-      Action.Doc { uri; handler }
+      Action.Doc { uri; contents; handler }
   in
   match R.Handler.Params.of_yojson (`Assoc params) with
   | Ok params -> handler params

petanque/json/interp.mli

@@ -13,6 +13,7 @@ module Action : sig
     | Now of (token:Coq.Limits.Token.t -> Yojson.Safe.t r)
     | Doc of
         { uri : Lang.LUri.File.t
+        ; contents : string option
         ; handler :
             token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> Yojson.Safe.t r
         }

petanque/json/protocol.ml

@@ -10,7 +10,7 @@ module HType = struct
   type ('p, 'r) t =
     | Immediate of (token:Coq.Limits.Token.t -> 'p -> 'r R.t)
     | FullDoc of
-        { uri_fn : 'p -> LUri.File.t
+        { uri_fn : 'p -> LUri.File.t * string option
         ; handler : token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> 'p -> 'r R.t
         }
 end
@@ -56,6 +56,7 @@ module Start = struct
     type t =
       { uri : Lsp.JLang.LUri.File.t
       ; opts : Run_opts.t option [@default None]
+      ; contents : string option [@default None]
       ; pre_commands : string option [@default None]
       ; thm : string
       }
@@ -75,9 +76,10 @@ module Start = struct
 
     let handler =
       HType.FullDoc
-        { uri_fn = (fun { Params.uri; _ } -> uri)
+        { uri_fn = (fun { Params.uri; contents; _ } -> (uri, contents))
         ; handler =
-            (fun ~token ~doc { Params.uri = _; opts; pre_commands; thm } ->
+            (fun ~token ~doc
+                 { Params.uri = _; opts; contents = _; pre_commands; thm } ->
               Agent.start ~token ~doc ?opts ?pre_commands ~thm ())
         }
   end

petanque/json_shell/interp_shell.ml

@@ -10,9 +10,9 @@ open Protocol_shell
 let do_handle ~fn ~token action =
   match action with
   | Action.Now handler -> handler ~token
-  | Action.Doc { uri; handler } ->
+  | Action.Doc { uri; contents; handler } ->
     let open Coq.Compat.Result.O in
-    let* doc = fn ~token ~uri |> of_pet_err in
+    let* doc = fn ~token ~uri ~contents |> of_pet_err in
     handler ~token ~doc
 
 let request ~fn ~token ~id ~method_ ~params =
@@ -36,6 +36,7 @@ let request ~fn ~token ~id ~method_ ~params =
 type doc_handler =
      token:Coq.Limits.Token.t
   -> uri:Lang.LUri.File.t
+  -> contents:string option
   -> (Fleche.Doc.t, Petanque.Agent.Error.t) Result.t
 
 let interp ~fn ~token (r : Lsp.Base.Message.t) : Lsp.Base.Message.t option =

petanque/json_shell/interp_shell.mli

@@ -8,6 +8,7 @@
 type doc_handler =
      token:Coq.Limits.Token.t
   -> uri:Lang.LUri.File.t
+  -> contents:string option
   -> (Fleche.Doc.t, Petanque.Agent.Error.t) Result.t
 
 val interp :

petanque/json_shell/protocol_shell.ml

@@ -56,7 +56,7 @@ module TableOfContents = struct
 
     let handler =
       Protocol.HType.FullDoc
-        { uri_fn = (fun { Params.uri } -> uri)
+        { uri_fn = (fun { Params.uri } -> (uri, None))
         ; handler = (fun ~token ~doc _ -> Shell.get_toc ~token ~doc)
         }
   end

petanque/json_shell/shell.ml

@@ -72,16 +72,22 @@ let read_raw ~uri =
   try Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all)
   with Sys_error err -> Error (Petanque.Agent.Error.system err)
 
-let setup_doc ~token env uri =
-  match read_raw ~uri with
+let setup_doc ~token env uri contents =
+  let contents =
+    match contents with
+    | Some contents -> Ok contents
+    | None -> read_raw ~uri
+  in
+  match contents with
   | Ok raw ->
     let doc = Fleche.Doc.create ~token ~env ~uri ~version:0 ~raw in
     print_diags doc;
     let target = Fleche.Doc.Target.End in
     Ok (Fleche.Doc.check ~io ~token ~target ~doc ())
   | Error err -> Error err
 
-let build_doc ~token ~uri = setup_doc ~token (Option.get !env) uri
+let build_doc ~token ~uri ~contents =
+  setup_doc ~token (Option.get !env) uri contents
 
 (* Flèche LSP backend handles the conversion at the protocol level *)
 let to_uri uri =

petanque/json_shell/shell.mli

@@ -24,6 +24,7 @@ val set_workspace :
 val build_doc :
      token:Coq.Limits.Token.t
   -> uri:Lang.LUri.File.t
+  -> contents:string option
   -> (Fleche.Doc.t, Agent.Error.t) Result.t
 
 val get_toc :

petanque/test/basic_api.ml

@@ -30,7 +30,7 @@ let start ~token =
   let* () = Shell.set_workspace ~token ~debug ~root in
   (* Careful to call [build_doc] before we have set an environment! [pet] and
      [pet-server] are careful to always set a default one *)
-  let* doc = Shell.build_doc ~token ~uri in
+  let* doc = Shell.build_doc ~token ~uri ~contents:None in
   Agent.start ~token ~doc ~thm:"rev_snoc_cons" ()
 
 let extract_st { Agent.Run_result.st; _ } = st

petanque/test/json_api.ml

@@ -51,6 +51,7 @@ let print_toc = false
 let run (ic, oc) =
   let open Coq.Compat.Result.O in
   let debug = false in
+  let contents = None in
   let module S = Client.S (struct
     let ic = ic
     let oc = oc
@@ -66,7 +67,8 @@ let run (ic, oc) =
   let root, uri = prepare_paths () in
   let* () = S.set_workspace { debug; root } in
   let* { st; _ } =
-    S.start { uri; opts = None; pre_commands = None; thm = "rev_snoc_cons" }
+    S.start
+      { uri; opts = None; contents; pre_commands = None; thm = "rev_snoc_cons" }
   in
   let* premises = S.premises { st } in
   (if print_premises then

petanque/test/json_api_failure.ml

@@ -18,6 +18,7 @@ let extract_st { JAgent.Run_result.st; _ } = st
 let run (ic, oc) =
   let open Coq.Compat.Result.O in
   let debug = false in
+  let contents = None in
   let module S = Client.S (struct
     let ic = ic
     let oc = oc
@@ -34,7 +35,7 @@ let run (ic, oc) =
   let opts = None in
   let* _env = S.set_workspace { debug; root } in
   let* { st; _ } =
-    S.start { uri; opts; pre_commands = None; thm = "rev_snoc_cons" }
+    S.start { uri; opts; contents; pre_commands = None; thm = "rev_snoc_cons" }
   in
   let* _premises = S.premises { st } in
   let* st = S.run { opts; st; tac = "induction l." } in