9 files changed, 122 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index a48a71c159..ec61f60791 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -299,6 +299,11 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK)
 	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \
 	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
 	$(HIDE)./$<.test
+unit-tests/ide/%.ml.log: unit-tests/ide/%.ml unit-tests/src/$(UNIT_LINK)
+	$(SHOW) 'TEST      $<'
+	$(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.ide,oUnit \
+	     -I unit-tests/src $(UNIT_LINK) $< -o $<.test;
+	$(HIDE)./$<.test
 
 #######################################################################
 # Other generic tests
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index adabb7a0a0..8447cf10db 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -11,7 +11,7 @@ let evil t f =
   let te = Declare.definition_entry
       ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu
   in
-  let tc = Declare.declare_constant t (DefinitionEntry te, k) in
+  let tc = Declare.declare_constant t (Declare.DefinitionEntry te, k) in
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
@@ -19,4 +19,4 @@ let evil t f =
       ~types:(Term.mkArrowR tc tu)
       (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1))
   in
-  ignore (Declare.declare_constant f (DefinitionEntry fe, k))
+  ignore (Declare.declare_constant f (Declare.DefinitionEntry fe, k))
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.
diff --git a/test-suite/unit-tests/ide/lex_tests.ml b/test-suite/unit-tests/ide/lex_tests.ml
new file mode 100644
index 0000000000..3082acdf1f
--- /dev/null
+++ b/test-suite/unit-tests/ide/lex_tests.ml
@@ -0,0 +1,50 @@
+open Utest
+
+let log_out_ch = open_log_out_ch __FILE__
+
+let lex s =
+  let n =
+    let last = String.length s - 1 in
+    if s.[last] = '.' then Some last else None in
+  let stop = ref None in
+  let f i _ = assert(!stop = None); stop := Some i in
+  begin try Coq_lex.delimit_sentences f s
+  with Coq_lex.Unterminated -> () end;
+  if n <> !stop then begin
+    let p_opt = function None -> "None" | Some i -> "Some " ^ string_of_int i in
+    Printf.fprintf log_out_ch "ERROR: %S\nEXPECTED: %s\nGOT: %s\n" s (p_opt n) (p_opt !stop)
+  end;
+  n = !stop
+
+let i2s i = "test at line: " ^ string_of_int i
+
+let tests = [
+
+  mk_bool_test (i2s __LINE__) "no quotation" @@ lex
+  "foo.+1 bar."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation" @@ lex
+  "foo constr:(xxx)."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot" @@ lex
+  "foo constr:(xxx. yyy)."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot double paren" @@ lex
+  "foo constr:((xxx. (foo.+1 ) \")\" yyy))."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot paren [" @@ lex
+  "foo constr:[xxx. (foo.+1 ) \")\" yyy]."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot double paren [" @@ lex
+  "foo constr:[[xxx. (foo.+1 ) \")\" yyy]]."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation with dot triple paren [" @@ lex
+  "foo constr:[[[xxx. (foo.+1 @@ [] ) \"]])\" yyy]]]."
+  ;
+  mk_bool_test (i2s __LINE__) "quotation nesting {" @@ lex
+  "bar:{{ foo {{ hello. }} }}."
+  ;
+
+]
+
+let _ = run_tests __FILE__ log_out_ch tests