diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-26 18:41:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-11-27 16:06:54 +0100 |
| commit | 10af47a5790987ee5211bac88c3a16396f30bcb0 (patch) | |
| tree | 9c260091569dd7cc4c9d8897cf6d2d8115918d5e /lib/feedback.mli | |
| parent | 894a3d16471f19bd527730490ea242e218b62ff6 (diff) | |
Feedback: API cleaned up, documented and made user extensible
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/lib/feedback.mli b/lib/feedback.mli index bda15fc58..b7822b27b 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -35,25 +35,30 @@ type route_id = int val default_route : route_id type feedback_content = - | AddedAxiom + (* STM mandatory data (must be displayed) *) | Processed | Incomplete | Complete - | GlobRef of Loc.t * string * string * string * string - | GlobDef of Loc.t * string * string * string | ErrorMsg of Loc.t * string + (* STM optional data *) + | ProcessingIn of string | InProgress of int - | SlaveStatus of string * string - | ProcessingInMaster + | WorkerStatus of string * string + (* Generally useful metadata *) | Goals of Loc.t * string - | StructuredGoals of Loc.t * xml + | AddedAxiom + | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string | FileDependency of string option * string | FileLoaded of string * string + (* Extra metadata *) + | Custom of Loc.t * string * xml + (* Old generic messages *) | Message of message type feedback = { id : edit_or_state_id; (* The document part concerned *) - content : feedback_content; (* The payload *) + contents : feedback_content; (* The payload *) route : route_id; (* Extra routing info *) } |