new parser for lp files

src/common/pos.ml

@@ -88,13 +88,11 @@ let to_string : ?print_dirname:bool -> ?print_fname:bool -> pos -> string =
   fun ?(print_dirname=true) ?(print_fname=true)
     {fname; start_line; start_col; end_line; end_col} ->
   let fname =
-    if not print_fname then "" else
-    match fname with
-    | None    -> ""
-    | Some(n) ->
-        if print_dirname then n ^ ":"
-        else
-          Filename.basename n ^ ":"
+    if print_fname then
+      match fname with
+      | None -> ""
+      | Some n -> (if print_dirname then n else Filename.basename n) ^ ":"
+    else ""
   in
   if start_line <> end_line then
     Printf.sprintf "%s%d:%d-%d:%d" fname start_line start_col end_line end_col
@@ -107,8 +105,8 @@ let popt_to_string :
   ?print_dirname:bool -> ?print_fname:bool -> popt -> string =
   fun ?(print_dirname=true) ?(print_fname=true) pop ->
   match pop with
-    | None -> "Unknown location "
-    | Some (p) -> to_string ~print_dirname ~print_fname p ^ " "
+    | None -> "Unknown location"
+    | Some (p) -> to_string ~print_dirname ~print_fname p
 
 (** [pp ppf pos] prints the optional position [pos] on [ppf]. *)
 let pp : popt Lplib.Base.pp = fun ppf p ->

src/handle/command.ml

@@ -575,8 +575,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   with
   | Timeout                as e -> raise e
   | Fatal(Some(Some(_)),_) as e -> raise e
-  | Fatal(None         ,m)      -> fatal pos "Error on command.@.%s" m
-  | Fatal(Some(None)   ,m)      -> fatal pos "Error on command.@.%s" m
+  | Fatal(None         ,m)      -> fatal pos "%s" m
+  | Fatal(Some(None)   ,m)      -> fatal pos "%s" m
   | e                           ->
       fatal pos "Uncaught exception: %s." (Printexc.to_string e)
 

src/handle/query.ml

@@ -160,9 +160,9 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result =
   let ctxt = Env.to_ctxt env in
   let p = new_problem() in
   match elt with
-  | P_query_search s ->
+  | P_query_search q ->
       let dbpath = Path.default_dbpath in
-      return string (Tool.Indexing.search_cmd_txt ss s ~dbpath)
+      return string (Tool.Indexing.search_cmd_txt_query ss q ~dbpath)
   | P_query_debug(_,_)
   | P_query_verbose(_)
   | P_query_flag(_,_)