diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-21 19:30:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-21 19:30:29 +0000 |
| commit | ff1f2731ffd94c8117934e9222e502c20cc25ee7 (patch) | |
| tree | 84dcd36871f51d3502e1d691569056b391dadbaa /ide/coqide.ml | |
| parent | 27d86b4d9e5b1ba33bd754ac7cffcfc39cec7091 (diff) | |
Correction bugs ide undo et highlight (suite à typos)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 4420fcceb..cd2e0358f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1400,12 +1400,14 @@ Please restart and report NOW."; in begin match last_command with | {ast=_,com} when is_vernac_tactic_command com -> +prerr_endline "TACT"; begin try Pfedit.undo 1; ignore (pop ()); sync update_input () with _ -> self#backtrack_to_no_lock start None end | {reset_info=ResetAtSegmentStart (id, {contents=true})} -> +prerr_endline "SEG"; ignore (pop ()); reset_to_mod id; sync update_input () @@ -1413,7 +1415,7 @@ Please restart and report NOW."; if Pfedit.refining () then self#backtrack_to_no_lock start (Some id) else - (ignore (pop ()); sync update_input ()) + (ignore (pop ()); reset_to id; sync update_input ()) | {reset_info=ResetAtDecl (id,{contents=false})} -> ignore (pop ()); (try @@ -3348,7 +3350,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); \nContributors : Jean-Christophe Filliâtre\ \n Pierre Letouzey, Claude Marché\n\ \nFeature wish or bug report: use Web interface\n\ - \n\thttp://logical.futurs.inria.fr/coq-bugs\n\ + \n\thttp://logical.saclay.inria.fr/coq-bugs\n\ \nVersion information\ \n-------------------\n" in |