Merge PR #10375: [lexer] correctly update line number when lexing QUOTATION (fix #10350)

Ack-by: gares
Reviewed-by: ppedrot

6 files changed, 65 insertions, 0 deletions

diff --git a/test-suite/misc/quotation_token.sh b/test-suite/misc/quotation_token.sh
new file mode 100755
index 0000000000..6357e8d7ce
--- /dev/null
+++ b/test-suite/misc/quotation_token.sh
@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+
+set -e
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc/quotation_token/
+
+coq_makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/quotation_plugin.cma
+
+TMP=`mktemp`
+
+if make > $TMP 2>&1; then
+  echo "should fail"
+  rm $TMP
+  exit 1
+fi
+
+if grep "File.*quotation.v., line 12, characters 6-30" $TMP; then
+  rm $TMP
+  exit 0
+else
+  echo "wong loc: `grep File.*quotation.v $TMP`"
+  rm $TMP
+  exit 1
+fi
diff --git a/test-suite/misc/quotation_token/.gitignore b/test-suite/misc/quotation_token/.gitignore
new file mode 100644
index 0000000000..18da256f3e
--- /dev/null
+++ b/test-suite/misc/quotation_token/.gitignore
@@ -0,0 +1,2 @@
+/Makefile*
+/src/quotation.ml
diff --git a/test-suite/misc/quotation_token/_CoqProject b/test-suite/misc/quotation_token/_CoqProject
new file mode 100644
index 0000000000..1b3e7c6399
--- /dev/null
+++ b/test-suite/misc/quotation_token/_CoqProject
@@ -0,0 +1,6 @@
+-Q theories Quotation
+-I src
+
+src/quotation.mlg
+src/quotation_plugin.mlpack
+theories/quotation.v
diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg
new file mode 100644
index 0000000000..961b170a0d
--- /dev/null
+++ b/test-suite/misc/quotation_token/src/quotation.mlg
@@ -0,0 +1,12 @@
+{
+open Pcoq.Constr
+}
+GRAMMAR EXTEND Gram
+  GLOBAL: operconstr;
+
+  operconstr: LEVEL "0"
+    [ [ s = QUOTATION "foobar:" ->
+        {
+          CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ]
+  ;
+END
diff --git a/test-suite/misc/quotation_token/src/quotation_plugin.mlpack b/test-suite/misc/quotation_token/src/quotation_plugin.mlpack
new file mode 100644
index 0000000000..b372b94b30
--- /dev/null
+++ b/test-suite/misc/quotation_token/src/quotation_plugin.mlpack
@@ -0,0 +1 @@
+Quotation
diff --git a/test-suite/misc/quotation_token/theories/quotation.v b/test-suite/misc/quotation_token/theories/quotation.v
new file mode 100644
index 0000000000..66326e89c1
--- /dev/null
+++ b/test-suite/misc/quotation_token/theories/quotation.v
@@ -0,0 +1,13 @@
+
+Declare ML Module "quotation_plugin".
+
+Definition x := foobar:{{ hello
+  there
+}}.
+
+Definition y := foobar:{{ another
+  multi line
+  thing
+}}.
+Check foobar:{{ oops
+ ips }} y.