diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index c15320f187bc56bce139f65db7b595f621791e26..d597ee199799e1ae860676ec5f7bc9b8504848b6 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -190,7 +190,8 @@ let consolidated wpo =
(* -------------------------------------------------------------------------- *)
let main t = t.main
-let head t = match t.head with
+let head t = t.head
+let head_goal t = match t.head with
| None -> t.main
| Some n -> n.goal
let goal n = n.goal
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 33cb4ae786c960a0d0cc42f06e9e58f66ca2293b..f974522b22969fbf5b1439fc7ccc34a5fb14d313 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -63,8 +63,9 @@ val current : tree -> current
val goto : tree -> position -> unit
val main : tree -> Wpo.t
-val head : tree -> Wpo.t
val goal : node -> Wpo.t
+val head : tree -> node option
+val head_goal : tree -> Wpo.t
val tree_context : tree -> WpContext.t
val node_context : node -> WpContext.t
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index 862ef1c023bb7c86faae6dbbad93bbf3965c1590..4440b768d7be65fc0ac0278face838658303715e 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -421,12 +421,18 @@ let default () =
) @@
Wp_parameters.DefaultStrategies.get ()
-let hints goal =
- let hs =
- let pid = goal.Wpo.po_pid in
- List.filter_map (fun (name,_) -> Hashtbl.find_opt strategies name) @@
- List.filter (fun (_,ps) -> WpPropId.select_by_name ps pid) !revhints
- in List.rev_append hs (default ())
+let hints ?node goal =
+ let pool = ref [] in
+ let add s = if not @@ List.memq s !pool then pool := s :: !pool in
+ let addname name = Option.iter add @@ Hashtbl.find_opt strategies name in
+ Option.iter addname (Option.bind node ProofEngine.get_hint) ;
+ let pid = goal.Wpo.po_pid in
+ List.iter
+ (fun (name,ps) ->
+ if WpPropId.select_by_name ps pid then addname name
+ ) !revhints ;
+ List.iter add @@ List.rev @@ default () ;
+ List.rev !pool
let has_hint goal =
let pid = goal.Wpo.po_pid in
diff --git a/src/plugins/wp/ProofStrategy.mli b/src/plugins/wp/ProofStrategy.mli
index 9e84f5bd61d90bfbd76ba4b2c6772f80d884e96c..90c5995b1f8ba0022ada4f5756ea4c67069b732f 100644
--- a/src/plugins/wp/ProofStrategy.mli
+++ b/src/plugins/wp/ProofStrategy.mli
@@ -34,7 +34,7 @@ val typecheck : unit -> unit
val name : strategy -> string
val loc : strategy -> Cil_types.location
val find : string -> strategy option
-val hints : Wpo.t -> strategy list
+val hints : ?node:ProofEngine.node -> Wpo.t -> strategy list
val has_hint : Wpo.t -> bool
val iter : (strategy -> unit) -> unit
diff --git a/src/plugins/wp/gui/GuiGoal.ml b/src/plugins/wp/gui/GuiGoal.ml
index 0148e3f44485bb1f35da507c9c9ed4ffbeb38aeb..c4b555bd1ff2032fa2cca9ab0ccdea6d28d422fc 100644
--- a/src/plugins/wp/gui/GuiGoal.ml
+++ b/src/plugins/wp/gui/GuiGoal.ml
@@ -386,11 +386,13 @@ class pane (gprovers : GuiConfig.provers) =
autosearch#connect None ;
strategies#connect None ;
List.iter (fun tactic -> tactic#clear) tactics
- | Some(tree,wpo,sequent,sel) ->
+ | Some(tree,sequent,sel) ->
on_proof_context tree
begin fun () ->
(* configure strategies *)
- let hints = ProofStrategy.hints wpo in
+ let node = ProofEngine.head tree in
+ let wpo = ProofEngine.head_goal tree in
+ let hints = ProofStrategy.hints ?node wpo in
autosearch#connect (Some (self#autosearch sequent));
strategies#connect ~hints (Some self#strategies);
(* configure tactics *)
@@ -515,12 +517,11 @@ class pane (gprovers : GuiConfig.provers) =
self#update_provers None ;
self#update_tactics None ;
| Proof proof ->
- let wpo = ProofEngine.head proof in
begin
- self#update_provers (Some wpo) ;
+ self#update_provers (Some (ProofEngine.head_goal proof)) ;
let sequent = printer#sequent in
let select = printer#selection in
- self#update_tactics (Some(proof,wpo,sequent,select)) ;
+ self#update_tactics (Some(proof,sequent,select)) ;
end
| Composer _ | Browser _ -> ()
@@ -560,7 +561,7 @@ class pane (gprovers : GuiConfig.provers) =
text#hrule ;
scripter#tree proof ;
text#hrule ;
- text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+ text#printf "%t@." (printer#goal (ProofEngine.head_goal proof)) ;
text#printf "@{<bf>Goal id:@} %s@." main.po_gid ;
text#printf "@{<bf>Short id:@} %s@." main.po_sid ;
text#hrule ;
@@ -576,7 +577,7 @@ class pane (gprovers : GuiConfig.provers) =
self#update in
text#printf "%t@." (composer#print cc ~quit) ;
text#hrule ;
- text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+ text#printf "%t@." (printer#goal (ProofEngine.head_goal proof)) ;
end ()
| Browser(proof,cc,tgt) ->
on_proof_context proof
@@ -588,7 +589,7 @@ class pane (gprovers : GuiConfig.provers) =
self#update in
text#printf "%t@." (browser#print cc ~quit) ;
text#hrule ;
- text#printf "%t@." (printer#goal (ProofEngine.head proof)) ;
+ text#printf "%t@." (printer#goal (ProofEngine.head_goal proof)) ;
end ()
| Forking _ -> ()
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 597d31342dd50eeb2c417ad50964747d0b7fc47e..3b5f932999ac3233b3e619b243c2da003ecfe92b 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -96,8 +96,7 @@ let do_print_goal_status fmt (g : Wpo.t) =
Format.fprintf fmt "%tSubgoal %d/%d:@\n" Wpo.pp_flow (succ i) n ;
ProofEngine.goto tree (`Leaf i) ;
do_print_current fmt tree ;
- let g = ProofEngine.head tree in
- Wpo.pp_goal fmt g
+ Wpo.pp_goal fmt @@ ProofEngine.head_goal tree
done
end ;
Wpo.pp_flow fmt ;