diff options
| -rw-r--r-- | .depend.newcoq | 6 | ||||
| -rw-r--r-- | ide/coq.ml | 15 | ||||
| -rw-r--r-- | ide/coq.mli | 3 | ||||
| -rw-r--r-- | 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); |