aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.ml
diff options
context:
space:
mode:
authorGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-03 15:53:40 +0000
committerGravatar marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-03-03 15:53:40 +0000
commitcc4b49c10a523ed752a13497a91ab36f62b37c0f (patch)
tree31b7c2c4c196a7aeda6658c03e5068da2a79e2b4 /ide/coq.ml
parentad8585656fe4c3e902aab93a4c470079640844a2 (diff)
ide: silent behavior better, save icon, -byte works
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 71bc09cc2..17db71802 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -107,7 +107,7 @@ let is_in_proof_mode () =
let user_error_loc l s =
raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
-let interp s =
+let interp verbosely s =
prerr_endline "Starting interp...";
prerr_endline s;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
@@ -149,7 +149,7 @@ let interp s =
| VernacFixpoint _
| VernacCoFixpoint _
| VernacEndProof _
- -> Options.make_silent false
+ -> Options.make_silent (not verbosely)
| _ -> ()
end;
Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s));
@@ -158,7 +158,7 @@ let interp s =
last
let interp_and_replace s =
- let result = interp s in
+ let result = interp false s in
let msg = read_stdout () in
result,msg