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 /ide | |
| parent | 980431c745997587a9463ead5bdf849e872ce1ad (diff) | |
[test] for #9204
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/fake_ide.ml | 7 |
1 files changed, 7 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]*") ] |