diff options
Diffstat (limited to 'parsing/location.mli')
| -rw-r--r-- | parsing/location.mli | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/parsing/location.mli b/parsing/location.mli index e6df9d1f6c..8287d1ec9a 100644 --- a/parsing/location.mli +++ b/parsing/location.mli @@ -69,6 +69,8 @@ val mkloc : 'a -> t -> 'a loc val print: formatter -> t -> unit val print_filename: formatter -> string -> unit +val absolute_path: string -> string + val show_filename: string -> string (** In -absname mode, return the absolute path for this filename. Otherwise, returns the filename unchanged. *) @@ -89,7 +91,8 @@ type error = val error: ?loc:t -> ?sub:error list -> ?if_highlight:string -> string -> error -val errorf: ?loc:t -> ?sub:error list -> ?if_highlight:string -> ('a, unit, string, error) format4 -> 'a +val errorf: ?loc:t -> ?sub:error list -> ?if_highlight:string + -> ('a, unit, string, error) format4 -> 'a val error_of_printer: t -> (formatter -> 'a -> unit) -> 'a -> error |