diff options
| author | Emilio Jesus Gallego Arias | 2016-03-03 16:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-03-03 17:07:45 +0100 |
| commit | a8962654c562349f24728613352ea76268227471 (patch) | |
| tree | 8fbafaafec6783164b6e1b3b07a467a22b538e0a /mathcomp/ssreflect/plugin | |
| parent | 42ae48695694641c67a86adb299e34f6c1366f4f (diff) | |
[search] Use msg_info to notify search results.
By default, the search command calls `Pp.msg` to print search results.
Unfortunately, this bypasses the `log_via_feedback` option and produces
not very nice results on feedback-depending IDES like JsCoq.
A proper fix would involve merging coq/coq#143 , and the upcoming search
cleanup, but this should do the trick for now.
I couldn't observe any problem with the usual testing.
Diffstat (limited to 'mathcomp/ssreflect/plugin')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index 0d2326f..d6a5175 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -1456,7 +1456,7 @@ let interp_modloc mr = let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in - msg (hov 2 pr_res ++ fnl ()) + msg_info (hov 2 pr_res ++ fnl ()) VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY | [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] -> diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 index d76f761..c40d965 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 @@ -1437,7 +1437,7 @@ let interp_modloc mr = let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in - msg (hov 2 pr_res ++ fnl ()) + msg_info (hov 2 pr_res ++ fnl ()) VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY | [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] -> |