From 2837753608c077b543467ad086d393dddf9c3f9d Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 3 Mar 2015 12:01:34 +0100
Subject: Declarative mode: fix the focus behaviour.

I had previously mistakenly enforced the property that after solving every goal in a block, unfocusing was performed automatically until one goal is in focus. This is not how the declarative mode is supposed to behave. Rather every focus must be explicitely unfocused by a closing command.

This hit a few bad interaction with the pure representation of proof introduced for the asynchronous processing.

Some of the invariants seem fragile, so this minimally disruptive solution is probably not long-term. In particular since each block uses the same focus kind, an `end <block>` may close another block than intended if the number of unfocussing command executed is not the right one.
---
 plugins/decl_mode/decl_mode.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'plugins/decl_mode/decl_mode.ml')

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index d169dc1372..07bf6d3268 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -89,7 +89,7 @@ let get_info sigma gl=
 let try_get_info sigma gl =
   Store.get (Goal.V82.extra sigma gl) info
 
-let get_stack pts =
+let get_goal_stack pts =
   let { it = goals ; sigma = sigma } = Proof.V82.subgoals pts in
   let info = get_info sigma (List.hd goals) in
   info.pm_stack
@@ -99,7 +99,7 @@ let proof_focus = Proof.new_focus_kind ()
 let proof_cond = Proof.no_cond proof_focus
 
 let focus p =
-  let inf = get_stack p in
+  let inf = get_goal_stack p in
   Proof_global.simple_with_current_proof (fun _ -> Proof.focus proof_cond inf 1)
 
 let unfocus () =
@@ -116,6 +116,8 @@ let get_top_stack pts =
     let info = get_info sigma gl in
     info.pm_stack
 
+let get_stack pts = Proof.get_at_focus proof_focus pts
+
 let get_last env = match Environ.named_context env with
   | (id,_,_)::_ -> id
   | [] -> error "no previous statement to use"
-- 
cgit v1.2.3


From 71fcb53fd93edcac1925f97d619871e8597e24e2 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 12 Mar 2015 17:32:50 +0100
Subject: Declarative mode: remove dead code.

---
 plugins/decl_mode/decl_mode.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'plugins/decl_mode/decl_mode.ml')

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 07bf6d3268..da41cd86db 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -105,9 +105,6 @@ let focus p =
 let unfocus () =
   Proof_global.simple_with_current_proof (fun _ p -> Proof.unfocus proof_focus p ())
 
-let maximal_unfocus () = 
-  Proof_global.simple_with_current_proof (fun _ -> Proof.maximal_unfocus proof_focus)
-
 let get_top_stack pts =
   try
     Proof.get_at_focus proof_focus pts
-- 
cgit v1.2.3


From edb3302188af4b5b75111339e3f466a6ec09aef2 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 12 Mar 2015 17:46:35 +0100
Subject: Declarative mode: make it so that unfocussing can only be done for
 closed subproofs.

The front-end is supposed to take care of that, but it may help to catch bugs.
---
 plugins/decl_mode/decl_mode.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode/decl_mode.ml')

diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index da41cd86db..07df7c7f09 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -96,7 +96,7 @@ let get_goal_stack pts =
 
 
 let proof_focus = Proof.new_focus_kind ()
-let proof_cond = Proof.no_cond proof_focus
+let proof_cond = Proof.done_cond proof_focus
 
 let focus p =
   let inf = get_goal_stack p in
-- 
cgit v1.2.3