diff options
author | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-26 17:09:55 +0000 |
---|---|---|
committer | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-26 17:09:55 +0000 |
commit | 0e839c7150c33d5603d95bf0f861efa7216037cb (patch) | |
tree | 180d647873bdf0a0e40f2663a624dfd32493f425 | |
parent | 611bab7e223707ab23ee4b6d9f074dd6981e1ff3 (diff) |
coqide: addloadpath corrige
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3792 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | ide/coq.ml | 13 | ||||
-rw-r--r-- | ide/coqide.ml | 34 |
2 files changed, 32 insertions, 15 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 32d21ad1c..0678c16c7 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -43,14 +43,15 @@ let is_in_coq_lib dir = Coq_config.coqlib (Filename.concat "theories" s) in - prerr_endline ("Comparing to : "^fdir); - let fstat = Unix.stat dir in - fstat.Unix.st_dev = stat.Unix.st_dev && - fstat.Unix.st_ino = stat.Unix.st_ino - with _ -> false + prerr_endline (" Comparing to : "^fdir); + let fstat = Unix.stat fdir in + (fstat.Unix.st_dev = stat.Unix.st_dev) && + (fstat.Unix.st_ino = stat.Unix.st_ino) && + (prerr_endline " YES";true) + with _ -> prerr_endline " No(because of a local exn)";false ) Coq_config.theories_dirs - with _ -> false + with _ -> prerr_endline " No(because of a global exn)";false let interp s = prerr_endline s; diff --git a/ide/coqide.ml b/ide/coqide.ml index 6b63c788e..b6aa92112 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -106,7 +106,7 @@ module Vector = struct let exists f t = let l = Array.length !t in let rec test i = - i < l && ((!t.(i) <> None && f (out_some !t.(i))) || test (i+1)) + (i < l) && (((!t.(i) <> None) && f (out_some !t.(i))) || test (i+1)) in test 0 end @@ -304,11 +304,18 @@ let do_if_not_computing f x = (* push a new Coq phrase *) -let update_on_end_of_proof () = +let update_on_end_of_proof id = let lookup_lemma = function | { ast = _, ( VernacDefinition (_, _, ProveBody _, _, _) - | VernacStartTheoremProof _) ; reset_info = Reset (_, r) } -> - r := true; raise Exit + | VernacStartTheoremProof _) ; + reset_info = Reset (_, r) } -> + if not !r then begin + prerr_endline "Toggling Reset info to true"; + r := true; raise Exit end + else begin + prerr_endline "Toggling Changing Reset id"; + r:=false + end | { ast = _, (VernacAbort _ | VernacAbortAll) } -> raise Exit | _ -> () in @@ -321,7 +328,7 @@ let update_on_end_of_segment id = | VernacDeclareModule (id',_,_,None) | VernacDeclareModuleType (id',_,None)); reset_info = Reset (_, r) } - when id = id' -> raise Exit + when id = id' -> raise Exit | { reset_info = Reset (_, r) } -> r := false | _ -> () in @@ -331,7 +338,9 @@ let push_phrase start_of_phrase_mark end_of_phrase_mark ast = let x = {start = start_of_phrase_mark; stop = end_of_phrase_mark; ast = ast; - reset_info = Coq.compute_reset_info (snd ast)} in + reset_info = Coq.compute_reset_info (snd ast) + } + in push x; match snd ast with | VernacEndProof (_, None) -> update_on_end_of_proof () @@ -776,7 +785,7 @@ object(self) !flash_info "Coq is computing"; process_pending (); while ((stop#compare self#get_start_of_input>=0) - && self#process_next_phrase false false) + && (self#process_next_phrase false false)) do () done; self#show_goals; input_buffer#remove_tag_by_name ~start ~stop "to_process" ; @@ -887,9 +896,16 @@ object(self) reset_to id; update_input () | { ast = _, ( VernacStartTheoremProof _ - | VernacDefinition (_,_,ProveBody _,_,_)) } -> + | VernacDefinition (_,_,ProveBody _,_,_)); + reset_info=Reset(id,{contents=false})} -> ignore (pop ()); - Pfedit.delete_current_proof (); + (try + Pfedit.delete_current_proof () + with e -> + begin + prerr_endline "WARNING : found a closed environment"; + raise e + end); update_input () | _ -> self#backtrack_to start |