diff options
| author | Maxime Dénès | 2016-06-28 13:55:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-06-28 13:57:33 +0200 |
| commit | 0e07e69dae3f3f4a99f824533f54a3991aacac6a (patch) | |
| tree | f2022d27c1742b3f3e99d76204a51860b6bc6ad5 /ide/session.ml | |
| parent | eb72574e1b526827706ee06206eb4a9626af3236 (diff) | |
Revert "A new infrastructure for warnings."
This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0.
I forgot that Jenkins gave me a spurious success when trying to build this PR.
There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue
has been fixed by Matej. Sorry for the noise.
Diffstat (limited to 'ide/session.ml')
| -rw-r--r-- | ide/session.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/ide/session.ml b/ide/session.ml index e998337604..cdec392ecc 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -195,8 +195,12 @@ let set_buffer_handlers to a point indicated by coq. *) if !no_coq_action_required then begin let start, stop = get_start (), get_stop () in - List.iter (fun tag -> buffer#remove_tag tag ~start ~stop) - Tags.Script.ephemere; + buffer#remove_tag Tags.Script.error ~start ~stop; + buffer#remove_tag Tags.Script.error_bg ~start ~stop; + buffer#remove_tag Tags.Script.tooltip ~start ~stop; + buffer#remove_tag Tags.Script.processed ~start ~stop; + buffer#remove_tag Tags.Script.to_process ~start ~stop; + buffer#remove_tag Tags.Script.incomplete ~start ~stop; Sentence.tag_on_insert buffer end; end in |