diff options
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 *) } |