Commit 778feeab authored by Sylvain Dailler's avatar Sylvain Dailler

ide: In node names, avoid interpreting '.' of explanations as a separator

for goal ancestry because it can be interpreted as part of a filename.
parent e193469f
...@@ -2031,8 +2031,21 @@ let treat_notification n = ...@@ -2031,8 +2031,21 @@ let treat_notification n =
| New_node (id, parent_id, typ, name, detached) -> | New_node (id, parent_id, typ, name, detached) ->
begin begin
let name = let name =
(* Reduce the name of the goals to the minimum: "0" instead of
"WP_Parameter.0" for example.
In cases where we want the explanation to be printed, and the
explanation contains filename (with '.'), this does not work. So, we
additionally check that the first part of the name is a number.
if typ = NGoal then if typ = NGoal then
List.hd (Strings.rev_split '.' name) let new_name = List.hd (Strings.rev_split '.' name) in
let name_number = List.hd (Strings.split ' ' new_name) in
ignore (int_of_string name_number);
with _ ->
(* The name is empty or the first part is not a number *)
else name else name
in in
try try
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment