For uniformity, changed the type [Syntax.trailer] from [string] to [Stretch.t].

Updated the lexer accordingly.
This has the benefit that a type error in a trailer will be correctly located
in the .mly file. Until now, it wasn't.

src/IL.mli

@@ -30,7 +30,7 @@ type program = {
     valdefs: valdef list;
 		
     (* Raw Objective Caml postlogue. *)
-    postlogue: string list;
+    postlogue: Stretch.t list;
 
   } 
 

src/coqBackend.ml

@@ -481,6 +481,6 @@ module Run (T: sig end) = struct
     write_theorems f;
 
     if not Settings.coq_no_actions then
-      List.iter (fprintf f "\n\n%s")
+      List.iter (fun stretch -> fprintf f "\n\n%s" stretch.Stretch.stretch_raw_content)
         Front.grammar.UnparameterizedSyntax.postludes
 end

src/fancy-parser.mly

@@ -24,7 +24,7 @@ open Positions
 %token <string Positions.located> LID UID 
 %token <Stretch.t> HEADER
 %token <Stretch.ocamltype> OCAMLTYPE
-%token <string Lazy.t> PERCENTPERCENT
+%token <Stretch.t Lazy.t> PERCENTPERCENT
 %token <Action.t> ACTION
 
 /* ------------------------------------------------------------------------- */

src/lexer.mll

@@ -264,12 +264,17 @@ rule main = parse
 | "%inline"
     { INLINE }
 | "%%"
-    { (* The token [PERCENTPERCENT] carries a string that contains
+    { (* The token [PERCENTPERCENT] carries a stretch that contains
          everything that follows %% in the input file. This string
-         is created lazily: the parser may or may not need it. *)
-      let ofs1 = lexeme_end lexbuf in
-      let ofs2 = String.length (Error.get_file_contents()) in
-      PERCENTPERCENT (lazy (chunk ofs1 ofs2)) }
+         must be created lazily. The parser decides (based on the
+         context) whether this stretch is needed. If it is indeed
+         needed, then constructing this stretch drives the lexer
+         to the end of the file. *)
+      PERCENTPERCENT (lazy (
+        let openingpos = lexeme_end_p lexbuf in
+        let closingpos = finish lexbuf in
+        mk_stretch openingpos closingpos false []
+      )) }
 | ":"
     { COLON }
 | ","
@@ -498,3 +503,15 @@ and char = parse
 | ""
    { () } 
 
+(* Read until the end of the file. This is used after finding a %%
+   that marks the end of the grammar specification. We update the
+   current position as we go. This allows us to build a stretch
+   for the trailer. *)
+
+and finish = parse
+| newline
+    { update_loc lexbuf; finish lexbuf }
+| eof
+    { lexeme_start_p lexbuf }
+| _
+    { finish lexbuf }

src/printer.ml

@@ -665,7 +665,7 @@ let program f p =
     nonrecvaldefs p.nonrecvaldefs
     (list moduledef nothing) p.moduledefs
     valdefs p.valdefs;
-  List.iter (output_string f) p.postlogue
+  List.iter (stretch false f) p.postlogue
 
 let valdecl f (x, ts) =
   fprintf f "val %s: %a%t%t" x typ ts.body nl nl

src/syntax.mli

@@ -17,11 +17,10 @@ type identifier =
 type filename = 
     string
 
-(* A trailer is also a source file fragment. It is represented
-   simply as a string. *)
+(* A trailer is a source file fragment. *)
 
 type trailer =
-    string
+    Stretch.t
 
 (* Objective Caml semantic actions are represented as stretches. *)
 

src/unparameterizedPrinter.ml

@@ -142,7 +142,7 @@ let print_branch mode f branch =
   Printf.fprintf f "}\n"
 
 let print_trailers b g =
-  List.iter (Printf.fprintf b "%s\n") g.postludes
+  List.iter (fun stretch -> Printf.fprintf b "%s\n" stretch.stretch_raw_content) g.postludes
 
 let branches_order r r' = 
   let branch_order b b' = 

src/yacc-parser.mly

@@ -16,7 +16,7 @@ open Positions
 %token <string Positions.located> LID UID 
 %token <Stretch.t> HEADER
 %token <Stretch.ocamltype> OCAMLTYPE
-%token <string Lazy.t> PERCENTPERCENT
+%token <Stretch.t Lazy.t> PERCENTPERCENT
 %token <Syntax.action> ACTION
 %start grammar
 %type <ConcreteSyntax.grammar> grammar