From 293b31aab50f0b7f947960ce15bf9ae6b6d576de Mon Sep 17 00:00:00 2001
From: monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 25 Jun 2003 13:03:27 +0000
Subject: coqide : status bar more informative, forbid Section/Module in proo
 mode

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4208 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 .depend.newcoq |  6 ------
 ide/coq.ml     | 15 +++++++++++++--
 ide/coq.mli    |  3 +++
 ide/coqide.ml  |  4 +++-
 4 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/.depend.newcoq b/.depend.newcoq
index 8e5bf3ee5..9cdc3b1da 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -1,9 +1,3 @@
-newtheories/FSets/FSet.vo: newtheories/FSets/FSet.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetBridge.vo newtheories/FSets/FSetProperties.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetRBT.vo
-newtheories/FSets/FSetList.vo: newtheories/FSets/FSetList.v newtheories/FSets/FSetInterface.vo
-newtheories/FSets/FSetBridge.vo: newtheories/FSets/FSetBridge.v newtheories/FSets/FSetInterface.vo
-newtheories/FSets/FSetProperties.vo: newtheories/FSets/FSetProperties.v newcontrib/omega/Omega.vo newtheories/FSets/FSetInterface.vo newtheories/Bool/Bool.vo newtheories/Bool/Sumbool.vo newtheories/Bool/Zerob.vo
-newtheories/FSets/FSetInterface.vo: newtheories/FSets/FSetInterface.v newtheories/Bool/Bool.vo newtheories/Lists/PolyList.vo newtheories/Sorting/Sorting.vo newtheories/Setoids/Setoid.vo
-newtheories/FSets/FSetRBT.vo: newtheories/FSets/FSetRBT.v newtheories/FSets/FSetInterface.vo newtheories/FSets/FSetList.vo newtheories/FSets/FSetBridge.vo newcontrib/omega/Omega.vo newtheories/ZArith/ZArith.vo
 newtheories/Reals/TypeSyntax.vo: newtheories/Reals/TypeSyntax.v
 newtheories/Reals/Rdefinitions.vo: newtheories/Reals/Rdefinitions.v newtheories/ZArith/ZArith_base.vo newtheories/Reals/TypeSyntax.vo
 newtheories/Reals/Rsyntax.vo: newtheories/Reals/Rsyntax.v newtheories/Reals/Rdefinitions.vo
diff --git a/ide/coq.ml b/ide/coq.ml
index c71669994..408054ee1 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -86,13 +86,14 @@ let interp s =
 	     Pcoq.main_entry 
 	     (Pcoq.Gram.parsable (Stream.of_string s)) 
   in match pe with 
-    | Some (loc,(VernacDefinition _  | VernacStartTheoremProof _ )) 
+    | Some (loc,(VernacDefinition _  | VernacStartTheoremProof _ | VernacBeginSection _ 
+		| VernacDefineModule _ | VernacDeclareModuleType _))
       when is_in_proof_mode () 
 	-> 
 	raise (Stdpp.Exc_located (loc, 
 			   Util.UserError
 			     ("CoqIde",
-			      (str "Proof imbrications are forbidden"))
+			      (str "cannot do that while in proof mode."))
 				 ))
     | _ -> 
 	Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
@@ -407,3 +408,13 @@ let is_state_preserving = function
       prerr_endline "state preserving command found"; true
   | _ -> 
       false
+
+
+let current_status () = 
+  let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
+  let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
+  try
+    path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ()))
+  with _ -> path
+
+  
diff --git a/ide/coq.mli b/ide/coq.mli
index 8625e93ee..641bcf201 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -59,3 +59,6 @@ type tried_tactic =
 
 val try_interptac: string -> tried_tactic
 
+(* Message to display in lower status bar. *)
+
+val current_status : unit -> string
diff --git a/ide/coqide.ml b/ide/coqide.ml
index f17beb604..01805ab1e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1996,7 +1996,9 @@ let main files =
       end
   in
 
-  let do_or_activate f = do_if_not_computing (do_or_activate f) in
+  let do_or_activate f = 
+    do_if_not_computing (do_or_activate (fun av -> f av ; !pop_info();!push_info (Coq.current_status())))
+  in
 
   let add_to_menu_toolbar text ~tooltip ~key ~callback icon = 
     ignore (navigation_factory#add_item text ~key ~callback);
-- 
cgit v1.2.3