diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-06-28 10:55:30 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-29 09:32:41 +0200 |
commit | 8e07227c5853de78eaed4577eefe908fb84507c0 (patch) | |
tree | b74780ac62cf49d9edc18dd846e96e79f6e24bf6 /ide/coqOps.ml | |
parent | c5e8224aa77194552b0e4c36f3bb8d40eb27a12b (diff) |
A new infrastructure for warnings.
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
Diffstat (limited to 'ide/coqOps.ml')
-rw-r--r-- | ide/coqOps.ml | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index f0e767cba..18557ab6b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -14,15 +14,17 @@ open Feedback let b2c = byte_offset_to_char_offset -type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string ] -type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ] +type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ] +type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ] let mem_flag_of_flag : flag -> mem_flag = function | `ERROR _ -> `ERROR + | `WARNING _ -> `WARNING | (`INCOMPLETE | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag let str_of_flag = function | `UNSAFE -> "U" | `PROCESSING -> "P" | `ERROR _ -> "E" + | `WARNING _ -> "W" | `INCOMPLETE -> "I" class type signals = @@ -470,6 +472,13 @@ object(self) self#attach_tooltip sentence loc msg; if not (Loc.is_ghost loc) then self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) + | Message(Warning, loc, msg), Some (id,sentence) -> + let loc = Option.default Loc.ghost loc in + let msg = Richpp.raw_print msg in + log "WarningMsg" id; + add_flag sentence (`WARNING (loc, msg)); + self#attach_tooltip sentence loc msg; + self#position_warning_tag_at_sentence sentence loc | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n @@ -511,6 +520,18 @@ object(self) let start, _, phrase = self#get_sentence sentence in self#position_error_tag_at_iter start phrase loc + method private position_warning_tag_at_iter iter_start iter_stop phrase loc = + if Loc.is_ghost loc then + buffer#apply_tag Tags.Script.warning ~start:iter_start ~stop:iter_stop + else + buffer#apply_tag Tags.Script.warning + ~start:(iter_start#forward_chars (b2c phrase loc.Loc.bp)) + ~stop:(iter_stop#forward_chars (b2c phrase loc.Loc.ep)) + + method private position_warning_tag_at_sentence sentence loc = + let start, stop, phrase = self#get_sentence sentence in + self#position_warning_tag_at_iter start stop phrase loc + method private process_interp_error queue sentence loc msg tip id = Coq.bind (Coq.return ()) (function () -> let start, stop, phrase = self#get_sentence sentence in |