From 9af598ece6749c1854799f5aa83133b9e3da052c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 4 May 2004 10:46:39 +0000 Subject: [PATCH] - moved up in the grammar precedences command entry so that sequence of commands are not permitted - added parsing of "abort" command --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 8eca10630..1b2ef3657 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -304,7 +304,9 @@ EXTEND ]; tactical0: [ [ t = tactical; SYMBOL "." -> t ] ]; tactical: - [ "sequence" LEFTA + [ "command" NONA + [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ] + | "sequence" LEFTA [ tactics = LIST1 NEXT SEP SYMBOL ";" -> return_tactical loc (TacticAst.Seq tactics) ] @@ -329,7 +331,6 @@ EXTEND | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac | tac = tactic -> return_tactical loc (TacticAst.Tactic tac) - | cmd = command -> return_tactical loc (TacticAst.Command cmd) ] ]; theorem_flavour: [ (* all flavours but Goal *) @@ -341,7 +342,8 @@ EXTEND ] ]; command: [ - [ [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof + [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort + | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof | [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit | [ IDENT "qed" | IDENT "Qed" ] -> return_command loc (TacticAst.Qed None) -- 2.39.2