Locations on parse errors

src/ide/why3ide.ml

@@ -1394,18 +1394,23 @@ let open_session: GMenu.menu_item =
 
 let treat_message_notification msg = match msg with
   (* TODO: do something ! *)
-  | Proof_error (_id, s)   -> print_message "%s" s
-  | Transf_error (_id, s)  -> print_message "%s" s
-  | Strat_error (_id, s)   -> print_message "%s" s
-  | Replay_Info s          -> print_message "%s" s
-  | Query_Info (_id, s)    -> print_message "%s" s
-  | Query_Error (_id, s)   -> print_message "%s" s
-  | Help s                 -> print_message "%s" s
-  | Information s          -> print_message "%s" s
-  | Task_Monitor (t, s, r) -> update_monitor t s r
-  | Open_File_Error s      -> print_message "%s" s
-  | Parse_Or_Type_Error s  -> print_message "%s" s
-  | File_Saved f           ->
+  | Proof_error (_id, s)         -> print_message "%s" s
+  | Transf_error (_id, s)        -> print_message "%s" s
+  | Strat_error (_id, s)         -> print_message "%s" s
+  | Replay_Info s                -> print_message "%s" s
+  | Query_Info (_id, s)          -> print_message "%s" s
+  | Query_Error (_id, s)         -> print_message "%s" s
+  | Help s                       -> print_message "%s" s
+  | Information s                -> print_message "%s" s
+  | Task_Monitor (t, s, r)       -> update_monitor t s r
+  | Open_File_Error s            -> print_message "%s" s
+  | Parse_Or_Type_Error (loc, s) ->
+    begin
+      (* TODO find a new color *)
+      color_loc ~color:Goal_color loc;
+      print_message "%s" s
+    end
+  | File_Saved f                 ->
     begin
       try
         let (_source_page, _source_view, b, l) = Hstr.find source_view_table f in
@@ -1413,10 +1418,10 @@ let treat_message_notification msg = match msg with
         update_label_saved l;
         print_message "%s was saved" f
       with
-      | Not_found ->
+      | Not_found                ->
           print_message "Please report: %s was not found in ide but was saved in session" f
     end
-  | Error s                ->
+  | Error s                      ->
       if Debug.test_flag debug then
         print_message "%s" s
       else

src/session/itp_communication.ml

@@ -32,7 +32,7 @@ type message_notification =
   | Help                  of string
   | Information           of string
   | Task_Monitor          of int * int * int
-  | Parse_Or_Type_Error   of string
+  | Parse_Or_Type_Error   of Loc.position * string
   | File_Saved            of string
   | Error                 of string
   | Open_File_Error       of string

src/session/itp_communication.mli

@@ -33,13 +33,13 @@ type message_notification =
   | Help                  of string
   (* General information *)
   | Information           of string
-  (* Number               of task scheduled, running, etc *)
+  (* Number of task scheduled, running, etc *)
   | Task_Monitor          of int * int * int
   (* A file was read or reloaded and now contains a parsing or typing error *)
-  | Parse_Or_Type_Error   of string
-  (* An error happened that could not be identified in server *)
-  | File_Saved            of string
+  | Parse_Or_Type_Error   of Loc.position * string
   (* [File_Saved f] f was saved *)
+  | File_Saved            of string
+  (* An error happened that could not be identified in server *)
   | Error                 of string
   | Open_File_Error       of string
 

src/session/itp_server.ml

@@ -273,19 +273,19 @@ let print_request fmt r =
 
 let print_msg fmt m =
   match m with
-  | Proof_error (_ids, s)  -> fprintf fmt "proof error %s" s
-  | Transf_error (_ids, s) -> fprintf fmt "transf error %s" s
-  | Strat_error (_ids, s)  -> fprintf fmt "start error %s" s
-  | Replay_Info s          -> fprintf fmt "replay info %s" s
-  | Query_Info (_ids, s)   -> fprintf fmt "query info %s" s
-  | Query_Error (_ids, s)  -> fprintf fmt "query error %s" s
-  | Help _s                -> fprintf fmt "help"
-  | Information s          -> fprintf fmt "info %s" s
-  | Task_Monitor _         -> fprintf fmt "task montor"
-  | Parse_Or_Type_Error s  -> fprintf fmt "parse_or_type_error:\n %s" s
-  | File_Saved s           -> fprintf fmt "file saved %s" s
-  | Error s                -> fprintf fmt "%s" s
-  | Open_File_Error s      -> fprintf fmt "%s" s
+  | Proof_error (_ids, s)      -> fprintf fmt "proof error %s" s
+  | Transf_error (_ids, s)     -> fprintf fmt "transf error %s" s
+  | Strat_error (_ids, s)      -> fprintf fmt "start error %s" s
+  | Replay_Info s              -> fprintf fmt "replay info %s" s
+  | Query_Info (_ids, s)       -> fprintf fmt "query info %s" s
+  | Query_Error (_ids, s)      -> fprintf fmt "query error %s" s
+  | Help _s                    -> fprintf fmt "help"
+  | Information s              -> fprintf fmt "info %s" s
+  | Task_Monitor _             -> fprintf fmt "task montor"
+  | Parse_Or_Type_Error (_, s) -> fprintf fmt "parse_or_type_error:\n %s" s
+  | File_Saved s               -> fprintf fmt "file saved %s" s
+  | Error s                    -> fprintf fmt "%s" s
+  | Open_File_Error s          -> fprintf fmt "%s" s
 
 (* TODO ad hoc printing. Should reuse print_loc. *)
 let print_loc fmt (loc: Loc.position) =
@@ -610,20 +610,38 @@ end
                       Format.eprintf "File : %s@." f.file_name;
                       read_and_send f.file_name) files
 
+  let relativize_location s loc =
+    let f, l, b, e = Loc.get loc in
+    let f = Sysutil.relativize_filename (Session_itp.get_dir s) f in
+    Loc.user_position f l b e
+
   (* Reload_files that is used even if the controller is not correct. It can
      be incorrect and end up in a correct state. *)
   let reload_files cont ~use_shapes =
     try reload_files cont ~use_shapes; true with
+    | Loc.Located (loc, e) ->
+      let loc = relativize_location cont.controller_session loc in
+      let s = Format.asprintf "%a at %a@."
+          Exn_printer.exn_printer e Pretty.print_loc loc in
+      P.notify (Message (Parse_Or_Type_Error (loc, s)));
+      false
     | e ->
       let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
-      P.notify (Message (Parse_Or_Type_Error s));
+      P.notify (Message (Parse_Or_Type_Error (Loc.dummy_position, s)));
       false
 
-  let add_file c ?format fname =
-    try add_file c ?format fname; true with
+  let add_file cont ?format fname =
+    try add_file cont ?format fname; true with
+    | Loc.Located (loc, e) ->
+      let loc = relativize_location cont.controller_session loc in
+      let s = Format.asprintf "%a at %a@."
+          Exn_printer.exn_printer e Pretty.print_loc loc in
+      P.notify (Message (Parse_Or_Type_Error (loc, s)));
+      false
     | e ->
-        let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
-        P.notify (Message (Parse_Or_Type_Error s)); false
+      let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
+      P.notify (Message (Parse_Or_Type_Error (Loc.dummy_position, s)));
+      false
 
   let task_driver config env =
     try

src/session/json_util.ml

@@ -247,6 +247,13 @@ let convert_constructor_message (m: message_notification) =
   | Open_File_Error _     -> String "Open_File_Error"
   | File_Saved _          -> String "File_Saved"
 
+let convert_loc (loc: Loc.position) : Json_base.json =
+  let (file, line, col1, col2) = Loc.get loc in
+  Record (convert_record ["file", Json_base.String file;
+                          "line", Json_base.Int line;
+                          "col1", Json_base.Int col1;
+                          "col2", Json_base.Int col2])
+
 let convert_message (m: message_notification) =
   let cc = convert_constructor_message in
   Record (match m with
@@ -282,9 +289,10 @@ let convert_message (m: message_notification) =
   | Task_Monitor (n, k, p) ->
       convert_record ["mess_notif", cc m;
            "monitor", List [Int n; Int k; Int p]]
-  | Parse_Or_Type_Error s ->
+  | Parse_Or_Type_Error (loc, s) ->
       convert_record ["mess_notif", cc m;
-           "error", String s]
+                      "loc", convert_loc loc;
+                      "error", String s]
   | Error s ->
       convert_record ["mess_notif", cc m;
            "error", String s]
@@ -302,13 +310,6 @@ let convert_color (color: color) : Json_base.json =
     | Premise_color -> "Premise_color"
     | Goal_color -> "Goal_color")
 
-let convert_loc (loc: Loc.position) : Json_base.json =
-  let (file, line, col1, col2) = Loc.get loc in
-  Record (convert_record ["file", Json_base.String file;
-                          "line", Json_base.Int line;
-                          "col1", Json_base.Int col1;
-                          "col2", Json_base.Int col2])
-
 let convert_loc_color (loc,color: Loc.position * color) : Json_base.json =
   let loc = convert_loc loc in
   let color = convert_color color in
@@ -686,6 +687,11 @@ let parse_message constr j =
     let s = get_string (get_field j "open_error") in
     Open_File_Error s
 
+  | "Parse_Or_Type_Error" ->
+    let loc = parse_loc (get_field j "loc") in
+    let error = get_string (get_field j "error") in
+    Parse_Or_Type_Error (loc, error)
+
   | _ -> raise NotMessage
 
 

src/tools/why3shell.ml

@@ -108,7 +108,7 @@ g -> print the current task\n\
 p -> print the session@." s
   | Information s          -> fprintf fmt "%s@." s
   | Task_Monitor (_t, _s, _r) -> () (* TODO do we want to print something for this? *)
-  | Parse_Or_Type_Error s  -> fprintf fmt "%s@." s
+  | Parse_Or_Type_Error (_, s)  -> fprintf fmt "%s@." s
   | Error s                ->
       fprintf fmt "%s@." s
   | Open_File_Error s -> fprintf fmt "%s@." s