diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-07 21:53:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-11 10:06:50 +0200 |
| commit | 2dbb54b1bc3967ee5d6e838cce8c56b88bd9477d (patch) | |
| tree | 7671cdaccac0ba46a5c21f5a6d1fb88c07007064 /lib/cWarnings.mli | |
| parent | ccf5c0879e3341ebfc8d3d00d35cc10b8b32a9e4 (diff) | |
[warnings] Remove `set_current_loc` hack.
Instead of the current hack that won't work as soon as we check some
part of the document asynchronously, we make the warning processor
recover a proper location if the warning doesn't have one attached.
This is what CoqIDE does [but it queries it's own document model].
Fixes: #6172
Diffstat (limited to 'lib/cWarnings.mli')
| -rw-r--r-- | lib/cWarnings.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index fa96b18c8..f97a53c4d 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -10,8 +10,6 @@ type status = Disabled | Enabled | AsError -val set_current_loc : Loc.t option -> unit - val create : name:string -> category:string -> ?default:status -> ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit |