diff options
author | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-25 13:03:27 +0000 |
---|---|---|
committer | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-25 13:03:27 +0000 |
commit | 293b31aab50f0b7f947960ce15bf9ae6b6d576de (patch) | |
tree | 373f33c911c0d858722c863dc76515ab0f0e6ff9 /ide/coqide.ml | |
parent | 1b09b2be6b433730c92c40126af4381559998285 (diff) |
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
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r-- | ide/coqide.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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); |