From a4a492ca1c1fe2caa3f5de785fe08662d9520725 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 29 Mar 2010 21:48:43 +0000
Subject: Several bug-fixes and improvements of coqdoc - make links to section
 variables working (used qualified names for   disambiguation and fixed the
 place in intern_var where to dump them)   (wish #2277) - mapping of physical
 to logical paths now follows coq (see bug #2274)   (incidentally, it was also
 incorrectly seeing foobar.v as a in directory foo) - added links for
 notations - added new category "other" for indexing entries not starting with
 latin letter   (e.g. notations or non-latin identifiers which was otherwise
 broken) - protected non-notation strings (from String.v) from utf8 symbol
 interpretation - incidentally quoted parseable _ in notations to avoid
 confusion with   placeholder in the "_ + _" form of notation - improved
 several "Sys_error" error messages - fixed old bug about second dot of ".."
 being interpreted as regular dot - removed obsolete lexer in index.mll (and
 renamed index.mll to index.ml) - added a test-suite file for testing various
 features of coqdoc

Things that still do not work:
- when a notation is redefined several times in the same scope, only
  the link to the first definition works
- if chars and symbols are not separated in advance, idents
  that immediately follow symbols are not detected
  (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations

Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
  same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
  line per each proper location covered by the notation)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/coqdoc/links.v | 102 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 102 insertions(+)
 create mode 100644 test-suite/coqdoc/links.v

(limited to 'test-suite/coqdoc')

diff --git a/test-suite/coqdoc/links.v b/test-suite/coqdoc/links.v
new file mode 100644
index 000000000..b09d64a9a
--- /dev/null
+++ b/test-suite/coqdoc/links.v
@@ -0,0 +1,102 @@
+(** Various checks for coqdoc
+
+- symbols should not be inlined in string g
+- links to both kinds of notations in a' should work to the right notation
+- with utf8 option, forall must be unicode
+- spliting between symbols and ident should be correct in a' and c
+- ".." should be rendered correctly
+*)
+
+Require Import String.
+
+Definition g := "dfjkh""sdfhj forall <> * ~"%string.
+
+Definition a (b: nat) := b.
+
+Definition f := forall C:Prop, C.
+
+Notation "n ++ m" := (plus n m).
+
+Notation "n ++ m" := (mult n m). (* redefinition *)
+
+Notation "n % m" := (plus n m) (at level 60).
+
+Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).
+
+Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : x = x :>A
+
+where "x = y :> A" := (@eq A x y) : type_scope.
+
+Definition eq0 := 0 = 0 :> nat.
+
+Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).
+
+Definition p := ((0#0;0) , (0 % 0)).
+
+Notation h := a.
+
+  Section test.
+
+    Variables b' b2: nat.
+
+    Notation "n + m" := (plus n m) : my_scope.
+
+    Delimit Scope my_scope with my.
+
+    Notation l := 0.
+
+    Definition α := (0 + l)%my.
+
+    Definition a' b := b'++0++b2 _ ++x b.
+
+    Definition c := {True}+{True}.
+
+    Definition d := (1+2)%nat.
+
+    Lemma e : nat + nat.
+    Admitted.
+
+  End test.
+
+  Section test2.
+
+    Variables b': nat.
+
+    Section test.
+
+      Variables b2: nat.
+
+      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.
+
+    End test.
+
+  End test2.
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
+(** skip *)
+
-- 
cgit v1.2.3