From 199ba6d46e56f62680c309725475b181e847b712 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 5 Feb 2003 22:39:39 +0000 Subject: New files. --- etc/coq/parsingdot.v | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 etc/coq/parsingdot.v (limited to 'etc/coq') diff --git a/etc/coq/parsingdot.v b/etc/coq/parsingdot.v new file mode 100644 index 00000000..7f3fe174 --- /dev/null +++ b/etc/coq/parsingdot.v @@ -0,0 +1,55 @@ +(* + From: Pierre Courtieu +To: David Aspinall +Subject: little annoying bug - don't know how to solve it clean +Date: Tue, 4 Feb 2003 21:06:55 +0100 +Hi David, I am trying to remove a little bug of coq/pg. It happens when +the user types by mistake two dots, instead of one. It happens quite often +and it should be refused (i.e. not sent to Coq) by pg. + +Example *) + +Goal (A,B:Prop)(A /\ B) -> (B /\ A). + +Intros x y z.. + +(* Test 1: (setq proof-script-command-end-regexp "[.][\\. \t\n\r]" ) *) + +(* Test 2: (setq proof-script-command-end-regexp "[.]\\([\\. \t\n\r]\\)") *) + +(* +What happens now is that "Intros x y z.." is sent to Coq, Coq reads the +first part of the command "Intros x y z.", executes it, and then throws an +error because of the second part "." is not correct. So pg stays before +"Intros x y z..", which is incorrect since "Intros x y z." has been +acceted by Coq. + +Remember that the current config of Coq is the following: + +(setq proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)" ) + +this is due to the fact that foo.bar is a valid identifier (Module/Section). + +Problem is that: + + - I cannot use "[.]\\([^a-Z.]\\)" because if we have: + + Intros x y z.. + Auto. + + then the command sent to Coq would be "Intros x y z.. Auto.", which is + worse. + + - I cannot use "[.]" because it would cut qualified names ("foo.bar"). + +Actually what I would like to use is a proof-not-allowed-command-end +variable, or more generally a hook for the function +proof-script-parse-function. + +I have defined (not commited) a coq-script-parse-function below to do +the check by hand, it is a copy of proof-script-generic-parse-cmdend, +with a check for ".." at the end (error if yes). + +The behavior we want is really an error here: It must not be sent to +coq at all! +*) \ No newline at end of file -- cgit v1.2.3