fix computation of names from expl or goal name

src/ide/gmain.ml

@@ -750,7 +750,7 @@ let notify any =
   (* name is set by notify since upgrade policy may update the prover name *)
   goals_model#set ~row:row#iter ~column:name_column
     (match any with
-      | S.Goal g -> S.goal_expl g
+      | S.Goal g -> S.goal_expl_or_name g
       | S.Theory th -> th.S.theory_name.Ident.id_string
       | S.File f -> Filename.basename f.S.file_name
       | S.Proof_attempt a ->

src/session/session.ml

@@ -523,15 +523,19 @@ exception NoTask
 let goal_task g = Opt.get_exn NoTask g.goal_task
 let goal_task_option g = g.goal_task
 
-let goal_expl g =
+let goal_expl_lazy g =
   match g.goal_expl with
-  | Some s -> assert (s <> ""); s
+  | Some s -> s
   | None ->
-     let s =
-       try let _,_,l = restore_path g.goal_name in
-           String.concat "." l
-       with Not_found -> g.goal_name.Ident.id_string
-     in assert (s <> ""); g.goal_expl <- Some s; s
+      let _name,expl,_task = Termcode.goal_expl_task ~root:false (goal_task g) in
+      g.goal_expl <- Some expl; expl
+
+let goal_expl_or_name g =
+  let s = goal_expl_lazy g in
+  if s <> "" then s else
+    try let _,_,l = restore_path g.goal_name in
+        String.concat "." l
+    with Not_found -> g.goal_name.Ident.id_string
 
 (************************)
 (* saving state on disk *)
@@ -1057,9 +1061,8 @@ let raw_add_task ~version ~(keygen:'a keygen) ~(expanded:bool) parent name expl
   let sum = Some (Termcode.task_checksum ~version t) in
   (* let shape = Termcode.t_shape_buf ~version (Task.task_goal_fmla t) in *)
   let shape = Termcode.t_shape_task ~version ~expl t in
-  let expl = if expl = "" then None else Some expl in
   let goal = { goal_name = name;
-               goal_expl = expl;
+               goal_expl = Some expl;
                goal_parent = parent;
                goal_task = Some t ;
                goal_checksum = sum;
@@ -1888,7 +1891,7 @@ let add_registered_metas ~keygen env added0 g =
     let metas = raw_add_metas ~keygen ~expanded:true g added idpos in
     let goal =
       raw_add_task ~version:env.session.session_shape_version
-        ~keygen ~expanded:true (Parent_metas metas) g.goal_name (goal_expl g) task
+        ~keygen ~expanded:true (Parent_metas metas) g.goal_name (goal_expl_lazy g) task
     in
     metas.metas_goal <- goal;
     metas
@@ -2330,7 +2333,7 @@ let rec recover_sub_tasks ~theories env_session task g =
   *)
   let version = env_session.session.session_shape_version in
   let sum = Termcode.task_checksum ~version task in
-  let expl = goal_expl g in
+  let expl = goal_expl_lazy g in
   let shape = Termcode.t_shape_task ~version ~expl task in
   if not ((match g.goal_checksum with
           | None -> false
@@ -2434,7 +2437,7 @@ and merge_metas_aux ~ctxt ~theories env to_goal _ from_metas =
   let to_goal =
     raw_add_task ~version:env.session.session_shape_version
       ~keygen:ctxt.keygen (Parent_metas to_metas) ~expanded:true
-      to_goal.goal_name (goal_expl to_goal) task
+      to_goal.goal_name (goal_expl_lazy to_goal) task
   in
   to_metas.metas_goal <- to_goal;
   Debug.dprintf debug "[Reload] metas done@\n";
@@ -2560,7 +2563,7 @@ let merge_file ~ctxt ~theories env from_f to_f =
 
 let rec recompute_all_shapes_goal ~release g =
   let t = goal_task g in
-  let expl = goal_expl g in
+  let expl = goal_expl_lazy g in
   g.goal_shape <- Termcode.t_shape_task ~expl t;
   g.goal_checksum <- Some (Termcode.task_checksum t);
   if release then release_task g;
@@ -2727,7 +2730,7 @@ and add_metas_to_goal ~keygen env to_goal from_metas =
     raw_add_task ~version:env.session.session_shape_version
       ~keygen ~expanded:true (Parent_metas to_metas)
       from_metas.metas_goal.goal_name
-      (goal_expl from_metas.metas_goal) task
+      (goal_expl_lazy from_metas.metas_goal) task
   in
   to_metas.metas_goal <- to_goal;
   add_goal_to_parent ~keygen env from_metas.metas_goal to_goal;

src/session/session.mli

@@ -318,8 +318,8 @@ val goal_task : 'key goal -> Task.task
 val goal_task_option : 'key goal -> Task.task option
 (** Return the task of a goal. *)
 
-val goal_expl : 'key goal -> string
-(** Return the explication of a goal *)
+val goal_expl_or_name : 'key goal -> string
+(** Return the explication of a goal, or its name if no explanation *)
 
 val proof_verified : 'key proof_attempt -> float option
 (** Return [Some t] if the proof is not obsolete and the result is

src/session/termcode.ml

@@ -76,7 +76,7 @@ let goal_expl_task ~root task =
   let info =
     match info with
       | Some i -> i
-      | None -> gid.Ident.id_string
+      | None -> ""
   in
   gid, info, task
 

src/why3session/why3session_html.ml

@@ -191,7 +191,7 @@ let rec num_lines acc tr =
       (color_of_status ~dark:false) (Opt.inhabited (S.goal_verified g))
       (max_depth - depth + 1);
     (* for i=1 to depth-1 do fprintf fmt "    " done; *)
-    fprintf fmt "%s</td>" (S.goal_expl g);
+    fprintf fmt "%s</td>" (S.goal_expl_or_name g);
 (*    for i=depth to max_depth-1 do fprintf fmt "<td></td>" done; *)
     print_results fmt provers (goal_external_proofs g);
     fprintf fmt "</tr>@\n";

src/why3session/why3session_latex.ml

@@ -190,7 +190,7 @@ let rec goal_latex_stat fmt prov depth depth_max subgoal g =
 	  if depth > 0 then fprintf fmt " & "
       end;
     if (depth <= 1) then
-      fprintf fmt "\\explanation{%s} " (protect (S.goal_expl g))
+      fprintf fmt "\\explanation{%s} " (protect (S.goal_expl_or_name g))
     else
       fprintf fmt " " ;
     let proofs = S.goal_external_proofs g in
@@ -243,13 +243,13 @@ let rec goal_latex2_stat fmt prov depth depth_max subgoal g =
   let proofs = S.goal_external_proofs g in
   if S.PHprover.length proofs > 0 then
     begin
-      style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
+      style_2_row fmt depth prov subgoal (protect (S.goal_expl_or_name g));
       print_result_prov proofs prov fmt
     end
  else
     if (*depth = 0*) true then
       begin
-        style_2_row fmt depth prov subgoal (protect (S.goal_expl g));
+        style_2_row fmt depth prov subgoal (protect (S.goal_expl_or_name g));
 	fprintf fmt "& \\multicolumn{%d}{|c|}{}\\\\ @."
           (List.length prov)
       end;