aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.mli
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-29 19:57:15 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-29 19:57:15 +0000
commit223400bd5f9afccdf2405af31cc37a1c92c9246c (patch)
treeb209ae19feee8a2946295966dd08ece77e43e108 /ide/ideutils.mli
parentc62d49b036e48d2753ec4d859e98c4fe027aff66 (diff)
Now CoqIDE separates answer and messages. This should hopefully
be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/ideutils.mli')
-rw-r--r--ide/ideutils.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 553c4c2bc..e7cfc4390 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -70,3 +70,6 @@ val requote : string -> string
val textview_width : #GText.view -> int
(** Returns an approximate value of the character width of a textview *)
+
+val default_logger : Interface.message_level -> string -> unit
+(** Default logger. It logs messages that the casual user should not see. *)