diff options
| author | ppedrot | 2012-06-23 21:01:40 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-23 21:01:40 +0000 |
| commit | 6aa16ad45240ba17a16cfa270f5c8033120826b1 (patch) | |
| tree | 498f3ec4f874f3f2a7fb5dba235bb515967467ff /lib | |
| parent | f2ef419fe205e242bf11eb53d45fba56131beaf8 (diff) | |
Moving logging level to Interface.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15486 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/interface.mli | 7 | ||||
| -rw-r--r-- | lib/pp.ml4 | 2 | ||||
| -rw-r--r-- | lib/pp.mli | 9 |
3 files changed, 9 insertions, 9 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index 47692191de..2cffa71aed 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -101,6 +101,13 @@ type coq_info = { (** * Coq answers to CoqIde *) +type message_level = +| Debug of string +| Info +| Notice +| Warning +| Error + type location = (int * int) option (* start and end of the error *) type 'a value = diff --git a/lib/pp.ml4 b/lib/pp.ml4 index fb85af0ebc..4eaf962636 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -329,7 +329,7 @@ let msgerrnl x = msgnl_with !err_ft x (* Logging management *) -type level = +type level = Interface.message_level = | Debug of string | Info | Notice diff --git a/lib/pp.mli b/lib/pp.mli index a1be529a9a..3daecea1a6 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -79,14 +79,7 @@ val tclose : unit -> std_ppcmds (** {6 Sending messages to the user } *) -type level = -| Debug of string -| Info -| Notice -| Warning -| Error - -type logger = level -> std_ppcmds -> unit +type logger = Interface.message_level -> std_ppcmds -> unit val msg_info : std_ppcmds -> unit (** Message that displays information, usually in verbose mode, such as [Foobar |