indexing: use String.remove_prefix (#1455)

- error.ml: fix comment
- Indexing.parse_file: test prefix "file://" instead of "file:///", and use Lplib.String.remove_prefix
- Library.path_of_file error message: put filename between double quotes

Author: fblanqui

src/common/error.ml

@@ -40,7 +40,7 @@ let no_wrn : ('a -> 'b) -> 'a -> 'b = fun f x ->
     description of the error, displayed differently from the error itself. *)
 exception Fatal of Pos.popt option * string * string
 
-(** [fatal_str fmt] may be called an arbitrary number of times to build up the
+(** [fatal_msg fmt] may be called an arbitrary number of times to build up the
     error message of the [fatal] or [fatal_no_pos] functions prior to  calling
     them. Note that the messages are stored in a buffer that is flushed by the
     [fatal] or [fatal_no_pos] function. Hence, they must be called. *)
@@ -50,8 +50,7 @@ let fatal_msg : 'a outfmt -> 'a =
 (** [fatal popt fmt] raises the [Fatal(popt,msg,err_desc)] exception, in which
     [msg] is built from the format [fmt] (provided the necessary arguments).
     [err_desc] continues the error message and is printed in normal format
-    instead of red color*)
-
+    instead of red color. *)
 let fatal : Pos.popt -> ?err_desc:string -> ('a,'b) koutfmt -> 'a =
   fun pos ?(err_desc="") fmt ->
   let err_desc _ =
@@ -89,4 +88,4 @@ let handle_exceptions : (unit -> unit) -> unit = fun f ->
   | e ->
       exit_with "" "Uncaught [%s].\n%s"
         (Printexc.to_string e)
-        (Printexc.get_backtrace())
+        (Printexc.get_backtrace())

src/common/library.ml

@@ -220,7 +220,7 @@ let path_of_file : (string -> string) -> string -> Path.t =
     match !mapping with
     | Some(mp, fp) -> (mp, fp)
     | None ->
-        fatal_msg "%s cannot be mapped under the library root.@." fname;
+        fatal_msg "\"%s\" cannot be mapped under the library root.@." fname;
         fatal_msg "Consider adding a package file under your source tree, ";
         fatal_no_pos "or use the [--map-dir] option."
   in

src/tool/indexing.ml

@@ -450,7 +450,7 @@ module DB = struct
  (* given a filename/URI it returns the stream of lines
     and a function to close the resources *)
  let parse_file fname =
-  if String.starts_with ~prefix:"file:///" fname then
+  if String.starts_with ~prefix:"file://" fname then
    (assert (fst Stdlib.(!lsp_input) = fname) ;
    let text = snd Stdlib.(!lsp_input) in
    let lines = ref (String.split_on_char '\n' text) in
@@ -742,12 +742,7 @@ let index_rule sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) =
  let rhs = rule.rhs in
  let get_relation = function | DB.Conclusion r -> r | _ -> assert false in
  let filename = Option.get rule_pos.fname in
- let filename =
-   if String.starts_with ~prefix:"file:///" filename then
-    let n = String.length "file://" in
-    String.sub filename n (String.length filename - n)
-   else
-    filename in
+ let filename = Lplib.String.remove_prefix "file://" filename in
  let path = Library.path_of_file Parsing.LpLexer.escape filename in
  let rule_name = (path,Common.Pos.to_string ~print_fname:false rule_pos) in
  index_term_and_subterms ~is_spine:false lhs