From ae3d83a69e1c8189e11ef88d11a344c866300b6e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= Date: Thu, 7 Jan 2016 11:01:00 +0100 Subject: [PATCH] Pretty-printing width is now configurable, default is 80. --- generator/main.ml | 26 ++++++++++++++++---------- generator/print_coq.ml | 4 ++-- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/generator/main.ml b/generator/main.ml index f0f23d8..7b8f167 100644 --- a/generator/main.ml +++ b/generator/main.ml @@ -24,6 +24,21 @@ let outputfile = ref None (*#########################################################################*) +let spec = + Arg.align [ + ("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs), + " includes a directory where to look for interface files"); + ("-pure", Arg.Set Characteristic.pure_mode, " generate formulae for purely-functional code"); + ("-rectypes", Arg.Set Clflags.recursive_types, " activates recursive types"); + ("-credits", Arg.Set Characteristic.use_credits, " generate 'pay' instructions"); + ("-nostdlib", Arg.Set no_mystd_include, " do not include standard library"); + ("-nopervasives", Arg.Set Clflags.nopervasives, " do not include standard pervasives file"); + ("-o", Arg.String (fun s -> outputfile := Some s), " set the output file name"); + ("-onlycmj", Arg.Set onlycmj, " only generate the .cmj file, not the .v file"); + ("-debug", Arg.Set is_tracing, " trace the various steps"); + ("-width", Arg.Set_int Print_coq.width, " set pretty-printing width for the .v file"); + ] + let _ = Settings.configure(); @@ -31,16 +46,7 @@ let _ = trace "1) parsing of command line"; let files = ref [] in Arg.parse - [ ("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs), - "includes a directory where to look for interface files"); - ("-pure", Arg.Set Characteristic.pure_mode, "generate formulae for purely-functional code"); - ("-rectypes", Arg.Set Clflags.recursive_types, "activates recursive types"); - ("-credits", Arg.Set Characteristic.use_credits, "generate 'pay' instructions"); - ("-nostdlib", Arg.Set no_mystd_include, "do not include standard library"); - ("-nopervasives", Arg.Set Clflags.nopervasives, "do not include standard pervasives file"); - ("-o", Arg.String (fun s -> outputfile := Some s), "set the output file name"); - ("-onlycmj", Arg.Set onlycmj, "only generate the cmj file, not the coq file"); - ("-debug", Arg.Set is_tracing, "trace the various steps") ] + spec (fun f -> files := f::!files) ("usage: [-I dir] [..other options..] file.ml"); (* diff --git a/generator/print_coq.ml b/generator/print_coq.ml index 6540edf..52cc7c6 100644 --- a/generator/print_coq.ml +++ b/generator/print_coq.ml @@ -19,7 +19,7 @@ let indentation = 2 let width = - 80 + ref 80 (* -------------------------------------------------------------------------- *) @@ -442,5 +442,5 @@ let tops ts = (* The main entry point translates a list of toplevel elements to a string. *) let tops ts : string = - run (PPrintEngine.ToBuffer.pretty 0.9 width) (tops ts) + run (PPrintEngine.ToBuffer.pretty 0.9 !width) (tops ts) -- GitLab