diff --git a/petanque/agent.ml b/petanque/agent.ml index d531396e..aa77dca9 100644 --- a/petanque/agent.ml +++ b/petanque/agent.ml @@ -41,6 +41,9 @@ module Error = struct | Anomaly _ -> -32004 | System _ -> -32005 | Theorem_not_found _ -> -32006 + + let coq e = Coq e + let system e = System e end module R = struct diff --git a/petanque/agent.mli b/petanque/agent.mli index d0a908e3..8ba9c2ed 100644 --- a/petanque/agent.mli +++ b/petanque/agent.mli @@ -27,6 +27,8 @@ module Error : sig val to_string : t -> string val to_code : t -> int + val coq : string -> t + val system : string -> t end (** Petanque results *) diff --git a/petanque/shell.ml b/petanque/shell.ml index 524e2ed5..85ee1343 100644 --- a/petanque/shell.ml +++ b/petanque/shell.ml @@ -19,7 +19,7 @@ let setup_workspace ~token ~init ~debug ~root = let+ workspace = Coq.Workspace.guess ~token ~debug ~cmdline ~dir in let files = Coq.Files.make () in Fleche.Doc.Env.make ~init ~workspace ~files) - |> Result.map_error (fun msg -> Agent.Error.Coq msg) + |> Result.map_error Agent.Error.coq let trace_stderr hdr ?extra:_ msg = Format.eprintf "@[[trace] %s | %s @]@\n%!" hdr msg @@ -68,7 +68,7 @@ let print_diags (doc : Fleche.Doc.t) = let read_raw ~uri = let file = Lang.LUri.File.to_string_file uri in try Ok Coq.Compat.Ocaml_414.In_channel.(with_open_text file input_all) - with Sys_error err -> Error (Agent.Error.Coq err) + with Sys_error err -> Error (Agent.Error.system err) let setup_doc ~token env uri = match read_raw ~uri with @@ -82,15 +82,21 @@ let setup_doc ~token env uri = let build_doc ~token ~uri = setup_doc ~token (Option.get !env) uri (* Flèche LSP backend handles the conversion at the protocol level *) -let to_uri uri = Lang.LUri.of_string uri |> Lang.LUri.File.of_uri +let to_uri uri = + Lang.LUri.of_string uri |> Lang.LUri.File.of_uri + |> Result.map_error Agent.Error.system + +let uri_of_path path = Format.asprintf "file:///%s" path |> to_uri let set_roots ~token ~debug ~roots = - match roots with - | [] -> Ok () - | root :: _ -> ( - match to_uri root with - | Error err -> Error (Agent.Error.System err) - | Ok root -> set_workspace ~token ~debug ~root) + let root = + match roots with + | [] -> Sys.getcwd () + | root :: _ -> root + in + let open Coq.Compat.Result.O in + let* root = uri_of_path root in + set_workspace ~token ~debug ~root let init_agent ~token ~debug ~roots = init_st := Some (init_coq ~debug);