aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-15 10:36:39 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-15 10:36:39 +0200
commit2f22a7f9f7f8369c2edc893e72e131e3b22bb19b (patch)
tree6afaf9ba1ba1e152d4871d66cccfa1ebdcc20d0f /ide
parent9e3c68fba148f68f72666e70f18e357a901b0228 (diff)
parentd3856bd7f6fb903a20124d57ea2a7bd6154b9039 (diff)
Merge PR #1042: Fixing minor typos in stm/coqide
Diffstat (limited to 'ide')
-rw-r--r--ide/coqOps.ml8
-rw-r--r--ide/ide_slave.ml1
2 files changed, 4 insertions, 5 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 364fc883b..9be70e6d3 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -463,7 +463,7 @@ object(self)
self#attach_tooltip ~loc sentence
(Printf.sprintf "%s %s %s" filepath ident ty)
| Message(Error, loc, msg), Some (id,sentence) ->
- log_pp ?id Pp.(str "ErrorMsg" ++ msg);
+ log_pp ?id Pp.(str "ErrorMsg " ++ msg);
remove_flag sentence `PROCESSING;
let rmsg = Pp.string_of_ppcmds msg in
add_flag sentence (`ERROR (loc, rmsg));
@@ -471,17 +471,17 @@ object(self)
self#attach_tooltip ?loc sentence rmsg;
self#position_tag_at_sentence ?loc Tags.Script.error sentence
| Message(Warning, loc, msg), Some (id,sentence) ->
- log_pp ?id Pp.(str "WarningMsg" ++ msg);
+ log_pp ?id Pp.(str "WarningMsg " ++ msg);
let rmsg = Pp.string_of_ppcmds msg in
add_flag sentence (`WARNING (loc, rmsg));
self#attach_tooltip ?loc sentence rmsg;
self#position_tag_at_sentence ?loc Tags.Script.warning sentence;
messages#push Warning msg
| Message(lvl, loc, msg), Some (id,sentence) ->
- log_pp ?id Pp.(str "Msg" ++ msg);
+ log_pp ?id Pp.(str "Msg " ++ msg);
messages#push lvl msg
| Message(lvl, loc, msg), None ->
- log_pp Pp.(str "Msg" ++ msg);
+ log_pp Pp.(str "Msg " ++ msg);
messages#push lvl msg
| InProgress n, _ ->
if n < 0 then processed <- processed + abs n
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 67391f556..b11a11606 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -1,5 +1,4 @@
(************************************************************************)
-
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)