-
Notifications
You must be signed in to change notification settings - Fork 31
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[lsp] Abstract URI type, improve URI validation.
This should help preventing many issues that can happen due to bad URIs; still quite a bit of work to do here, but the code overall, while a bit uglier, seems safer. Fixes #187
- Loading branch information
Showing
25 changed files
with
185 additions
and
59 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,4 @@ | ||
(library | ||
(name lang) | ||
(public_name coq-lsp.lang) | ||
(libraries coq-core.library)) | ||
(libraries uri coq-core.library)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
(************************************************************************) | ||
(* Flèche => document manager: Language Support *) | ||
(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) | ||
(* Written by: Emilio J. Gallego Arias *) | ||
(************************************************************************) | ||
|
||
type t = Uri.t | ||
|
||
let of_string = Uri.of_string | ||
let is_file_path _ = true | ||
|
||
module File = struct | ||
type uri = t | ||
|
||
type t = | ||
{ uri : uri | ||
; file : string | ||
} | ||
|
||
let of_uri uri = Result.Ok { uri; file = Uri.pct_decode (Uri.path uri) } | ||
let to_string_uri { uri; _ } = Uri.to_string uri | ||
let to_string_file { file; _ } = file | ||
let extension { file; _ } = Filename.extension file | ||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
(************************************************************************) | ||
(* Flèche => document manager: Language Support *) | ||
(* Copyright 2019-2023 Inria -- Dual License LGPL 2.1 / GPL3+ *) | ||
(* Written by: Emilio J. Gallego Arias *) | ||
(************************************************************************) | ||
|
||
type t | ||
|
||
(** Builds and URI from a string, like the ones present in the LSP protocol wire *) | ||
val of_string : string -> t | ||
|
||
(** Checks if a URI points to a (local) file *) | ||
val is_file_path : t -> bool | ||
|
||
(** Uris that are filesystem paths *) | ||
module File : sig | ||
type uri = t | ||
type t | ||
|
||
val of_uri : uri -> (t, string) Result.t | ||
|
||
(** Extension, with the dot included *) | ||
val extension : t -> string | ||
|
||
(** Percent-enconded URI as string *) | ||
val to_string_uri : t -> string | ||
|
||
(** Filename version, fit for OS functions *) | ||
val to_string_file : t -> string | ||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.