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 | |
| 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
| -rw-r--r-- | ide/coqide.ml | 6 | ||||
| -rw-r--r-- | ide/highlight.mll | 2 | ||||
| -rw-r--r-- | test-suite/ide/undo.v | 5 |
3 files changed, 10 insertions, 3 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 diff --git a/ide/highlight.mll b/ide/highlight.mll index 44de2f358..cbbaa112e 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -89,7 +89,7 @@ let multiword_command = | "Delimit" space+ "Scope" | "Next" space+ "Obligation" | "Solve" space+ "Obligations" -| "Require" space+ ("Import"|"Exportp") +| "Require" space+ ("Import"|"Export")? | "Infix" space+ locality | "Notation" space+ locality | "Hint" space+ locality ident diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v index a76817a87..d50f545da 100644 --- a/test-suite/ide/undo.v +++ b/test-suite/ide/undo.v @@ -72,3 +72,8 @@ Definition p := O. assert True by trivial. trivial. Qed. + +(* Undoing declarations, not in proof *) + +Definition q := O. +Definition r := O. |