← Back to branch summary

~ubuntu-branches/debian/jessie/coq/jessie

« back to all changes in this revision

Viewing changes to plugins/extraction/extract_env.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2011-12-25 13:46:09 UTC
  • mfrom: (1.3.6) (6.1.10 sid)
  • Revision ID: package-import@ubuntu.com-20111225134609-zwqkzmeni9g2xlq1
Tags: 8.3.pl3+dfsg-1
* New upstream release
  - remove all patches (applied upstream)

Show diffs side-by-side

added added

removed removed

Lines of Context:
plugins/extraction/extract_env.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(*i $Id: extract_env.ml 14012 2011-04-15 16:45:27Z letouzey $ i*)
 
9
(*i $Id: extract_env.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
10
10
 
11
11
open Term
12
12
open Declarations
404
404
 
405
405
(*s Extraction of a ml struct to a file. *)
406
406
 
 
407
(** For Recursive Extraction, writing directly on stdout
 
408
    won't work with coqide, we use a buffer instead *)
 
409
 
 
410
let buf = Buffer.create 1000
 
411
 
407
412
let formatter dry file =
408
413
  let ft =
409
414
    if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
410
 
    else Pp_control.with_output_to (Option.default stdout file)
 
415
    else
 
416
      match file with
 
417
        | Some f -> Pp_control.with_output_to f
 
418
        | None -> Format.formatter_of_buffer buf
411
419
  in
412
420
  (* We never want to see ellipsis ... in extracted code *)
413
421
  Format.pp_set_max_boxes ft max_int;
421
429
  ft
422
430
 
423
431
let print_structure_to_file (fn,si,mo) dry struc =
 
432
  Buffer.clear buf;
424
433
  let d = descr () in
425
434
  reset_renaming_tables AllButExternal;
426
435
  let unsafe_needs = {
463
472
         close_out cout; raise e
464
473
       end;
465
474
       info_file si)
466
 
    (if dry then None else si)
 
475
    (if dry then None else si);
 
476
  (* Print the buffer content via Coq standard formatter (ok with coqide). *)
 
477
  if Buffer.length buf <> 0 then begin
 
478
    Pp.message (Buffer.contents buf);
 
479
    Buffer.reset buf
 
480
  end
467
481
 
468
482
 
469
483
(*********************************************)