diff options
| author | coq | 2004-02-04 15:30:44 +0000 |
|---|---|---|
| committer | coq | 2004-02-04 15:30:44 +0000 |
| commit | 836276d44d2bad23c2dbc8ee66a74c7f71856a5f (patch) | |
| tree | 1d3325b539b6635979e813019be9f6da53a8dbc5 /toplevel | |
| parent | cf45343a65cc1c84dc5c521a34c6c112fb7b5fe7 (diff) | |
search window
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5288 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/cerrors.ml | 14 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
2 files changed, 9 insertions, 9 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 97ab8a9b74..719f7434a4 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -33,15 +33,15 @@ let report () = (str "." ++ spc () ++ str "Please report.") let rec explain_exn_default = function | Stream.Failure -> - hov 0 (str "Anomaly: Uncaught Stream.Failure.") + hov 0 (str "Anomaly: uncaught Stream.Failure.") | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) | Token.Error txt -> hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> - hov 0 (str "Error: OS: " ++ str msg) + hov 0 (str "Anomaly: uncaught exception Sys_error " ++ str (guill msg) ++ report ()) | UserError(s,pps) -> - hov 1 (str"Error: " ++ where s ++ pps) + hov 1 (str "User error: " ++ where s ++ pps) | Out_of_memory -> hov 0 (str "Out of memory") | Stack_overflow -> @@ -56,13 +56,13 @@ let rec explain_exn_default = function int pos1 ++ str " to #" ++ int pos2 ++ report ()) | Not_found -> - hov 0 (str "Anomaly: Search error" ++ report ()) + hov 0 (str "Anomaly: uncaught exception Not_found" ++ report ()) | Failure s -> - hov 0 (str "Anomaly: Failure " ++ str (guill s) ++ report ()) + hov 0 (str "Anomaly: uncaught exception Failure " ++ str (guill s) ++ report ()) | Invalid_argument s -> - hov 0 (str "Anomaly: Invalid argument " ++ str (guill s) ++ report ()) + hov 0 (str "Anomaly: uncaught exception Invalid_argument " ++ str (guill s) ++ report ()) | Sys.Break -> - hov 0 (fnl () ++ str"User Interrupt.") + hov 0 (fnl () ++ str "User Interrupt.") | Univ.UniverseInconsistency -> hov 0 (str "Error: Universe Inconsistency.") | TypeError(ctx,te) -> diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 6c82aaad0d..7c19954542 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -620,13 +620,13 @@ let vernac_add_ml_path isrec s = let vernac_declare_ml_module l = Mltop.declare_ml_modules l let vernac_chdir = function - | None -> print_endline (Sys.getcwd()) + | None -> message (Sys.getcwd()) | Some s -> begin try Sys.chdir (System.glob s) with Sys_error str -> warning ("Cd failed: " ^ str) end; - if_verbose print_endline (Sys.getcwd()) + if_verbose message (Sys.getcwd()) (********************) |