diff options
| author | Enrico Tassi | 2018-12-13 10:23:23 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-12-13 10:24:09 +0100 |
| commit | 00263f3211c67b16a488c6b0c2bc6432a1837256 (patch) | |
| tree | 320db41e12b7497246dea24549c44dbd017e9489 | |
| parent | 980431c745997587a9463ead5bdf849e872ce1ad (diff) | |
[test] for #9204
| -rw-r--r-- | ide/fake_ide.ml | 7 | ||||
| -rw-r--r-- | test-suite/ide/join.fake | 20 |
2 files changed, 27 insertions, 0 deletions
diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index 521aff6bf6..ae88f36b1c 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.ml @@ -257,10 +257,15 @@ let eval_print l coq = eval_call (wait ()) coq | [ Tok(_,"JOIN") ] -> eval_call (status true) coq + | [ Tok(_,"FAILJOIN") ] -> + after_fail coq (base_eval_call ~fail:false (status true) coq) | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] -> let to_id, _ = get_id id in if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip" else prerr_endline "Good tip" + | [ Tok(_,"ABORT") ] -> + prerr_endline "Quitting fake_ide"; + exit 0 | Tok("#[^\n]*",_) :: _ -> () | _ -> error "syntax error" @@ -276,6 +281,8 @@ let grammar = ; Seq [Item (eat_rex "JOIN")] ; Seq [Item (eat_rex "GOALS")] ; Seq [Item (eat_rex "FAILGOALS")] + ; Seq [Item (eat_rex "FAILJOIN")] + ; Seq [Item (eat_rex "ABORT")] ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ] ; Item (eat_rex "#[^\n]*") ] diff --git a/test-suite/ide/join.fake b/test-suite/ide/join.fake new file mode 100644 index 0000000000..c4c696ad9a --- /dev/null +++ b/test-suite/ide/join.fake @@ -0,0 +1,20 @@ +# Script simulating a dialog between coqide and coqtop -ideslave +# Run it via fake_ide +# +# Error resiliency +# + +ADD { Section x. } +ADD { Lemma x : True. } +ADD { Proof using. } +ADD here { trivial. } +ADD { fail. } +ADD { Qed. } +ADD { Lemma y : True. } +ADD { Proof using. } +ADD { trivial. } +ADD { Qed. } +ADD { End x. } +FAILJOIN +ASSERT TIP here +ABORT |