From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 24 Dec 2010 11:53:29 +0100
Subject: Imported Upstream version 8.3pl1

---
 interp/dumpglob.ml | 33 +++++++++++++++++++++++++--------
 1 file changed, 25 insertions(+), 8 deletions(-)

(limited to 'interp/dumpglob.ml')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 0a42b78b..020c3622 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dumpglob.ml 13328 2010-07-26 11:05:30Z herbelin $ *)
+(* $Id: dumpglob.ml 13674 2010-12-04 10:34:11Z herbelin $ *)
 
 
 (* Dump of globalization (to be used by coqdoc) *)
@@ -181,15 +181,32 @@ let dump_libref loc dp ty =
 		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
 let cook_notation df sc =
+  (* We encode notations so that they are space-free and still human-readable *)
+  (* - all spaces are replaced by _ *)
+  (* - all _ denoting a non-terminal symbol are replaced by x *)
+  (* - all terminal tokens are surrounded by single quotes, including '_' *)
+  (*   which already denotes terminal _ *)
+  (* - all single quotes in terminal tokens are doubled *)
+  (* The output is decoded in function Index.prepare_entry of coqdoc *)
   let ntn = String.make (String.length df * 3) '_' in
   let j = ref 0 in
-  let quoted = ref false in
-  for i = 0 to String.length df - 1 do
-    if df.[i] = '\'' then quoted := not !quoted;
-    if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else
-    if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else
-    if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else
-    (ntn.[!j] <- df.[i]; incr j)
+  let l = String.length df - 1 in
+  let i = ref 0 in
+  while !i <= l do
+    assert (df.[!i] <> ' ');
+    if df.[!i] = '_' && (!i = l || df.[!i+1] = ' ') then
+      (* Next token is a non-terminal *)
+      (ntn.[!j] <- 'x'; incr j; incr i)
+    else begin
+      (* Next token is a terminal *)
+      ntn.[!j] <- '\''; incr j;
+      while !i <= l && df.[!i] <> ' ' do
+	if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j);
+	ntn.[!j] <- df.[!i]; incr j; incr i
+      done;
+      ntn.[!j] <- '\''; incr j
+    end;
+    if !i <= l then (ntn.[!j] <- '_'; incr j; incr i)
   done;
   let df = String.sub ntn 0 !j in
   match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
-- 
cgit v1.2.3