← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to toplevel/cerrors.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
toplevel/cerrors.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: cerrors.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
10
 
 
11
open Pp
 
12
open Util
 
13
open Indtypes
 
14
open Type_errors
 
15
open Pretype_errors
 
16
open Indrec
 
17
open Lexer
 
18
 
 
19
let print_loc loc =
 
20
  if loc = dummy_loc then 
 
21
    (str"<unknown>")
 
22
  else 
 
23
    let loc = unloc loc in
 
24
    (int (fst loc) ++ str"-" ++ int (snd loc))
 
25
 
 
26
let guill s = "\""^s^"\""
 
27
 
 
28
let where s =
 
29
  if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
30
 
 
31
(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
 
32
 
 
33
let rec explain_exn_default_aux anomaly_string report_fn = function
 
34
  | Stream.Failure -> 
 
35
      hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
 
36
  | Stream.Error txt -> 
 
37
      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
 
38
  | Token.Error txt -> 
 
39
      hov 0 (str "Syntax error: " ++ str txt ++ str ".")
 
40
  | Sys_error msg -> 
 
41
      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
 
42
  | UserError(s,pps) -> 
 
43
      hov 0 (str "Error: " ++ where s ++ pps)
 
44
  | Out_of_memory -> 
 
45
      hov 0 (str "Out of memory.")
 
46
  | Stack_overflow -> 
 
47
      hov 0 (str "Stack overflow.")
 
48
  | Anomaly (s,pps) -> 
 
49
      hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
 
50
  | Match_failure(filename,pos1,pos2) ->
 
51
      hov 0 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ 
 
52
      if Sys.ocaml_version = "3.06" then
 
53
                   (str " from character " ++ int pos1 ++ 
 
54
                    str " to " ++ int pos2)
 
55
                 else
 
56
                   (str " at line " ++ int pos1 ++
 
57
                    str " character " ++ int pos2)
 
58
                   ++ report_fn ())
 
59
  | Not_found -> 
 
60
      hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ())
 
61
  | Failure s -> 
 
62
      hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ())
 
63
  | Invalid_argument s -> 
 
64
      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
 
65
  | Sys.Break -> 
 
66
      hov 0 (fnl () ++ str "User interrupt.")
 
67
  | Univ.UniverseInconsistency (o,u,v) ->
 
68
      let msg = 
 
69
        if !Constrextern.print_universes then
 
70
          spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
 
71
          str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
 
72
          ++ spc() ++ Univ.pr_uni v ++ str")"
 
73
        else
 
74
          mt() in
 
75
      hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
 
76
  | TypeError(ctx,te) -> 
 
77
      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
 
78
  | PretypeError(ctx,te) ->
 
79
      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
 
80
  | Typeclasses_errors.TypeClassError(env, te) ->
 
81
      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te)
 
82
  | InductiveError e -> 
 
83
      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
 
84
  | RecursionSchemeError e -> 
 
85
      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
 
86
  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when s <> mt () ->
 
87
      explain_exn_default_aux anomaly_string report_fn exc
 
88
  | Proof_type.LtacLocated (s,exc) ->
 
89
      hov 0 (Himsg.explain_ltac_call_trace s ++ fnl ()
 
90
             ++ explain_exn_default_aux anomaly_string report_fn exc)
 
91
  | Cases.PatternMatchingError (env,e) -> 
 
92
      hov 0
 
93
        (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
 
94
  | Tacred.ReductionTacticError e -> 
 
95
      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e)
 
96
  | Logic.RefinerError e -> 
 
97
      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e)
 
98
  | Nametab.GlobalizationError q ->
 
99
      hov 0 (str "Error:" ++ spc () ++
 
100
               str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 
101
               spc () ++ str "was not found" ++ 
 
102
               spc () ++ str "in the current" ++ spc () ++ str "environment.")
 
103
  | Nametab.GlobalizationConstantError q ->
 
104
      hov 0 (str "Error:" ++ spc () ++
 
105
               str "No constant of this name:" ++ spc () ++ 
 
106
               Libnames.pr_qualid q ++ str ".")
 
107
  | Refiner.FailError (i,s) ->
 
108
      hov 0 (str "Error: Tactic failure" ++ 
 
109
                (if s <> mt() then str ":" ++ s else mt ()) ++
 
110
                if i=0 then str "." else str " (level " ++ int i ++ str").")
 
111
  | Stdpp.Exc_located (loc,exc) ->
 
112
      hov 0 ((if loc = dummy_loc then (mt ())
 
113
               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
 
114
               ++ explain_exn_default_aux anomaly_string report_fn exc)
 
115
  | Lexer.Error Illegal_character -> 
 
116
      hov 0 (str "Syntax error: Illegal character.")
 
117
  | Lexer.Error Unterminated_comment -> 
 
118
      hov 0 (str "Syntax error: Unterminated comment.")
 
119
  | Lexer.Error Unterminated_string -> 
 
120
      hov 0 (str "Syntax error: Unterminated string.")
 
121
  | Lexer.Error Undefined_token -> 
 
122
      hov 0 (str "Syntax error: Undefined token.")
 
123
  | Lexer.Error (Bad_token s) -> 
 
124
      hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
 
125
  | Assert_failure (s,b,e) ->
 
126
      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
 
127
               (if s <> "" then 
 
128
                 if Sys.ocaml_version = "3.06" then
 
129
                   (str ("(file \"" ^ s ^ "\", characters ") ++ 
 
130
                    int b ++ str "-" ++ int e ++ str ")")
 
131
                 else
 
132
                   (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
 
133
                    str ", characters " ++ int e ++ str "-" ++
 
134
                    int (e+6) ++ str ")")
 
135
               else
 
136
                 (mt ())) ++
 
137
               report_fn ())
 
138
  | reraise ->
 
139
      hov 0 (anomaly_string () ++ str "Uncaught exception " ++ 
 
140
               str (Printexc.to_string reraise) ++ report_fn ())
 
141
 
 
142
let anomaly_string () = str "Anomaly: "
 
143
 
 
144
let report () = (str "." ++ spc () ++ str "Please report.")
 
145
 
 
146
let explain_exn_default =
 
147
  explain_exn_default_aux anomaly_string report
 
148
 
 
149
let raise_if_debug e =
 
150
  if !Flags.debug then raise e
 
151
 
 
152
let _ = Tactic_debug.explain_logic_error := explain_exn_default
 
153
 
 
154
let _ = Tactic_debug.explain_logic_error_no_anomaly :=
 
155
          explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
 
156
 
 
157
let explain_exn_function = ref explain_exn_default
 
158
 
 
159
let explain_exn e = !explain_exn_function e