Merge branch 'trunk' into pr379

5 files changed, 18 insertions, 11 deletions

diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4
index 02a720d2d9..3b84eaa816 100644
--- a/parsing/cLexer.ml4
+++ b/parsing/cLexer.ml4
@@ -105,7 +105,7 @@ module Error = struct
              Printf.sprintf "Unsupported Unicode character (0x%x)" x)
 
   (* Require to fix the Camlp4 signature *)
-  let print ppf x = Pp.pp_with ~pp_tag:Ppstyle.pp_tag ppf (Pp.str (to_string x))
+  let print ppf x = Pp.pp_with ppf (Pp.str (to_string x))
 
 end
 open Error
@@ -240,18 +240,19 @@ let unfreeze tt = (token_tree := tt)
 
 (* The string buffering machinery *)
 
-let buff = ref (String.create 80)
+let buff = ref (Bytes.create 80)
 
 let store len x =
-  if len >= String.length !buff then
-    buff := !buff ^ String.create (String.length !buff);
-  !buff.[len] <- x;
+  let open Bytes in
+  if len >= length !buff then
+    buff := cat !buff (create (length !buff));
+  set !buff len x;
   succ len
 
 let rec nstore n len cs =
   if n>0 then nstore (n-1) (store len (Stream.next cs)) cs else len
 
-let get_buff len = String.sub !buff 0 len
+let get_buff len = Bytes.sub_string !buff 0 len
 
 (* The classical lexer: idents, numbers, quoted strings, comments *)
 
@@ -382,6 +383,7 @@ let push_char c =
     real_push_char c
 
 let push_string s = Buffer.add_string current_comment s
+let push_bytes s = Buffer.add_bytes current_comment s
 
 let null_comment s =
   let rec null i =
@@ -716,13 +718,13 @@ let strip s =
   in
   if len == String.length s then s
   else
-    let s' = String.create len in
+    let s' = Bytes.create len in
     let rec loop i i' =
       if i == String.length s then s'
       else if s.[i] == ' ' then loop (i + 1) i'
-      else begin s'.[i'] <- s.[i]; loop (i + 1) (i' + 1) end
+      else begin Bytes.set s' i' s.[i]; loop (i + 1) (i' + 1) end
     in
-    loop 0 0
+    Bytes.to_string (loop 0 0)
 
 let terminal s =
   let s = strip s in
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 820514b08a..2db91b8f87 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -34,7 +34,7 @@ GEXTEND Gram
   GLOBAL:
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
-    ne_string string pattern_ident pattern_identref by_notation smart_global;
+    ne_string string lstring pattern_ident pattern_identref by_notation smart_global;
   preident:
     [ [ s = IDENT -> s ] ]
   ;
@@ -106,6 +106,9 @@ GEXTEND Gram
   string:
     [ [ s = STRING -> s ] ]
   ;
+  lstring:
+    [ [ s = string -> (!@loc, s) ] ]
+  ;
   integer:
     [ [ i = INT      -> my_int_of_string (!@loc) i
       | "-"; i = INT -> - my_int_of_string (!@loc) i ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d46880831f..18807113c9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1112,7 +1112,7 @@ GEXTEND Gram
 	 idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
            VernacSyntacticDefinition
 	     (id,(idl,c),local,b)
-     | IDENT "Notation"; local = obsolete_locality; s = ne_lstring; ":=";
+     | IDENT "Notation"; local = obsolete_locality; s = lstring; ":=";
 	 c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index c5823440ac..b8405ca8c5 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -267,6 +267,7 @@ module Prim =
     let integer = gec_gen "integer"
     let bigint = Gram.entry_create "Prim.bigint"
     let string = gec_gen "string"
+    let lstring = Gram.entry_create "Prim.lstring"
     let reference = make_gen_entry uprim "reference"
     let by_notation = Gram.entry_create "by_notation"
     let smart_global = Gram.entry_create "smart_global"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d987bb4557..cf5174af96 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -136,6 +136,7 @@ module Prim :
     val bigint : Bigint.bigint Gram.entry
     val integer : int Gram.entry
     val string : string Gram.entry
+    val lstring : string located Gram.entry
     val qualid : qualid located Gram.entry
     val fullyqualid : Id.t list located Gram.entry
     val reference : reference Gram.entry