diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqargs.ml | 11 | ||||
| -rw-r--r-- | toplevel/coqargs.mli | 4 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
3 files changed, 12 insertions, 4 deletions
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 8c643a285e..7c28ef24d4 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -49,7 +49,7 @@ type coq_cmdopts = { batch_mode : bool; compilation_mode : compilation_mode; - toplevel_name : Names.DirPath.t; + toplevel_name : Stm.interactive_top; compile_list: (string * bool) list; (* bool is verbosity *) compilation_output_name : string option; @@ -88,6 +88,8 @@ type coq_cmdopts = { } +let default_toplevel = Names.(DirPath.make [Id.of_string "Top"]) + let init_args = { load_init = true; @@ -101,7 +103,7 @@ let init_args = { batch_mode = false; compilation_mode = BuildVo; - toplevel_name = Names.(DirPath.make [Id.of_string "Top"]); + toplevel_name = Stm.TopLogical default_toplevel; compile_list = []; compilation_output_name = None; @@ -487,7 +489,10 @@ let parse_args arglist : coq_cmdopts * string list = let topname = Libnames.dirpath_of_string (next ()) in if Names.DirPath.is_empty topname then CErrors.user_err Pp.(str "Need a non empty toplevel module name"); - { oval with toplevel_name = topname } + { oval with toplevel_name = Stm.TopLogical topname } + + |"-topfile" -> + { oval with toplevel_name = Stm.TopPhysical (next()) } |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()); oval diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index accb6c2beb..b709788dde 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -11,6 +11,8 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo type color = [`ON | `AUTO | `OFF] +val default_toplevel : Names.DirPath.t + type coq_cmdopts = { load_init : bool; @@ -26,7 +28,7 @@ type coq_cmdopts = { batch_mode : bool; compilation_mode : compilation_mode; - toplevel_name : Names.DirPath.t; + toplevel_name : Stm.interactive_top; compile_list: (string * bool) list; (* bool is verbosity *) compilation_output_name : string option; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index c2437836f3..c43538017c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -32,6 +32,7 @@ let print_usage_channel co command = \n -R dir coqdir recursively map physical dir to logical coqdir\ \n -Q dir coqdir map physical dir to logical coqdir\ \n -top coqdir set the toplevel name to be coqdir instead of Top\ +\n -topfile f set the toplevel name as though compiling f\ \n -coqlib dir set the coq standard library directory\ \n -exclude-dir f exclude subdirectories named f for option -R\ \n\ |