Commit 74299a1a authored by Sylvain Dailler's avatar Sylvain Dailler

Focus on proofattempt actually focus on the parent.

parent 01d600d2
......@@ -1171,8 +1171,13 @@ end
| Get_first_unproven_node ni ->
notify_first_unproven_node d ni
| Focus_req nid ->
let d = get_server_data () in
let s = d.cont.controller_session in
let any = any_from_node_ID nid in
focused_node := Some any
(match any with
| APa pa ->
focused_node := Some (APn (Session_itp.get_proof_attempt_parent s pa))
| _ -> focused_node := Some any)
| Unfocus_req ->
focused_node := None
| Remove_subtree nid ->
......
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