diff options
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r-- | toplevel/coqtop.ml | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a699e528b..d66e975fc 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -21,7 +21,7 @@ open Coqinit let get_version_date () = try - let coqlib = Envars.coqlib () in + let coqlib = Envars.coqlib () in let ch = open_in (Filename.concat coqlib "revision") in let ver = input_line ch in let rev = input_line ch in @@ -37,7 +37,7 @@ let output_context = ref false let memory_stat = ref false -let print_memory_stat () = +let print_memory_stat () = if !memory_stat then Format.printf "total heap size = %d kbytes\n" (heap_size_kb ()) @@ -47,7 +47,7 @@ let engagement = ref None let set_engagement c = engagement := Some c let engage () = match !engagement with Some c -> Global.set_engagement c | None -> () - + let set_batch_mode () = batch_mode := true let toplevel_default_name = make_dirpath [id_of_string "Top"] @@ -76,7 +76,7 @@ let set_include d p = let p = dirpath_of_string p in push_include (d,p) let set_rec_include d p = - let p = dirpath_of_string p in + let p = dirpath_of_string p in push_rec_include(d,p) let load_vernacular_list = ref ([] : (string * bool) list) @@ -84,7 +84,7 @@ let add_load_vernacular verb s = load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list let load_vernacular () = List.iter - (fun (s,b) -> + (fun (s,b) -> if Flags.do_beautify () then with_option beautify_file (Vernac.load_vernac b) s else @@ -93,7 +93,7 @@ let load_vernacular () = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj -let load_vernac_obj () = +let load_vernac_obj () = List.iter (fun f -> Library.require_library_from_file None f None) (List.rev !load_vernacular_obj) @@ -106,7 +106,7 @@ let require () = let compile_list = ref ([] : (bool * string) list) let add_compile verbose s = set_batch_mode (); - Flags.make_silent true; + Flags.make_silent true; compile_list := (verbose,s) :: !compile_list let compile_files () = let init_state = States.freeze() in @@ -142,11 +142,11 @@ let re_exec is_ide = if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin let s = if s = "" then if is_native then "opt" else "byte" else s in - let newprog = + let newprog = let dir = Filename.dirname prog in let coqtop = if is_ide then "coqide." else "coqtop." in let com = coqtop ^ s ^ Coq_config.exec_extension in - if dir <> "." then Filename.concat dir com else com + if dir <> "." then Filename.concat dir com else com in Sys.argv.(0) <- newprog; Unix.handle_unix_error (Unix.execvp newprog) Sys.argv @@ -189,12 +189,12 @@ let parse_args is_ide = let glob_opt = ref false in let rec parse = function | [] -> () - | "-with-geoproof" :: s :: rem -> + | "-with-geoproof" :: s :: rem -> if s = "yes" then Coq_config.with_geoproof := true else if s = "no" then Coq_config.with_geoproof := false else usage (); parse rem - | "-impredicative-set" :: rem -> + | "-impredicative-set" :: rem -> set_engagement Declarations.ImpredicativeSet; parse rem | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem @@ -221,13 +221,13 @@ let parse_args is_ide = | "-full" :: rem -> warning "option -full deprecated\n"; parse rem | "-batch" :: rem -> set_batch_mode (); parse rem - | "-boot" :: rem -> boot := true; no_load_rc (); parse rem + | "-boot" :: rem -> boot := true; no_load_rc (); parse rem | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem | "-outputstate" :: s :: rem -> set_outputstate s; parse rem | "-outputstate" :: [] -> usage () | "-nois" :: rem -> set_inputstate ""; parse rem - + | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem | ("-inputstate"|"-is") :: [] -> usage () @@ -237,11 +237,11 @@ let parse_args is_ide = | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem | "-load-ml-source" :: [] -> usage () - | ("-load-vernac-source"|"-l") :: f :: rem -> + | ("-load-vernac-source"|"-l") :: f :: rem -> add_load_vernacular false f; parse rem | ("-load-vernac-source"|"-l") :: [] -> usage () - | ("-load-vernac-source-verbose"|"-lv") :: f :: rem -> + | ("-load-vernac-source-verbose"|"-lv") :: f :: rem -> add_load_vernacular true f; parse rem | ("-load-vernac-source-verbose"|"-lv") :: [] -> usage () @@ -278,9 +278,9 @@ let parse_args is_ide = | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem - | "-emacs-U" :: rem -> Flags.print_emacs := true; + | "-emacs-U" :: rem -> Flags.print_emacs := true; Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem - + | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem @@ -302,7 +302,7 @@ let parse_args is_ide = | "-user" :: u :: rem -> set_rcuser u; parse rem | "-user" :: [] -> usage () - | "-notactics" :: rem -> + | "-notactics" :: rem -> warning "Obsolete option \"-notactics\"."; remove_top_ml (); parse rem @@ -320,7 +320,7 @@ let parse_args is_ide = | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem - | s :: rem -> + | s :: rem -> if is_ide then begin ide_args := s :: !ide_args; parse rem @@ -330,7 +330,7 @@ let parse_args is_ide = in try parse (List.tl (Array.to_list Sys.argv)) - with + with | UserError(_,s) as e -> begin try Stream.empty s; exit 1 @@ -368,10 +368,10 @@ let init is_ide = exit 1 end; if !batch_mode then - (flush_all(); + (flush_all(); if !output_context then Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ()); - Profile.print_profile (); + Profile.print_profile (); exit 0); Lib.declare_initial_state () |