diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-07 23:35:34 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-07 23:35:34 +0000 |
commit | 966a0d7534763c65e65d32b5d6223fd34cfa2445 (patch) | |
tree | 96df0796402a6642b977d9587ff880e6291357fb /ide/coqide.ml | |
parent | f3db9d5424d411205c3fdde6d5b7ef11399de691 (diff) |
Improved error messages in CoqIDE:
- add a check that coqtop can be run before starting the interface
- returns the error message in case of problem
- made illegal option message more informative
- use coqtop.byte when coqide.byte (is it a good heuristic?)
- made debugging messages silent by default in ide/undo.ml (Ctrl-C was
calling Pervasives.prerr_endline instead of Ideutils.prerr_endline)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13627 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r-- | ide/coqide.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 2d22ca1fa..05f93863c 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -3085,8 +3085,10 @@ let process_argv argv = let continue,filtered = filter_coq_opts (List.tl argv) in if not continue then (List.iter Pervasives.prerr_endline filtered; exit 0); - if List.exists (fun arg -> String.get arg 0 == '-') filtered then - (output_string stderr "illegal coqide option\n"; exit 1); + let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in + if opts <> [] then + (output_string stderr ("Illegal option: "^List.hd opts^"\n"); + exit 1); filtered with _ -> (output_string stderr "coqtop choked on one of your option"; exit 1) @@ -3095,6 +3097,7 @@ let start () = let argl = Array.to_list Sys.argv in let files = process_argv argl in sup_args := String.concat " " (List.filter (fun x -> not (List.mem x files)) (List.tl argl)); + check_connection !sup_args; ignore_break (); GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc"); (try |