From 1c496f7b3e9f69da2b9a6072dc4c94fb841601ab Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 27 Jun 2003 16:53:31 +0000 Subject: [PATCH] The "Save proof" menu item is now activated when a finished proof is reopened. --- helm/gTopLevel/gTopLevel.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index d71162d1e..0f2f73c28 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1653,7 +1653,8 @@ let open_ () = Some (uri, metasenv, bo, ty) ; ProofEngine.goal := None ; refresh_goals notebook ; - refresh_proof output + refresh_proof output ; + !save_set_sensitive true with InvokeTactics.RefreshSequentException e -> output_html outputhtml -- 2.39.2