aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/feedback.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-01 16:51:15 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-06-02 16:45:39 +0200
commitffd89ea323937b7d323e24a2b6d53cdc857117dd (patch)
tree0e2a089a429486362bf5a4cd00e7662dee450a11 /lib/feedback.ml
parente020cc70578b65609ac7337537f16a1c25254e77 (diff)
Encapsulate xml serialization in xmlprotocol.mli
This eases the task of replacing/improving the serializer, as well as making it more resistant. See pitfalls below: Main changes are: - fold `message` type into `feedback` type - make messages of type `Richpp.richpp` so we are explicit about the content being a rich document. - moved serialization functions for messages and stateid to `Xmlprotocol` - improved a couple of internal API points (`is_message`). Tested.
Diffstat (limited to 'lib/feedback.ml')
-rw-r--r--lib/feedback.ml136
1 files changed, 5 insertions, 131 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml
index dce4372ec..d6f580fd1 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Xml_datatype
-open Serialize
type level =
| Debug of string
@@ -16,42 +15,6 @@ type level =
| Warning
| Error
-type message = {
- message_level : level;
- message_content : xml;
-}
-
-let of_message_level = function
- | Debug s ->
- Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
- | Info -> Serialize.constructor "message_level" "info" []
- | Notice -> Serialize.constructor "message_level" "notice" []
- | Warning -> Serialize.constructor "message_level" "warning" []
- | Error -> Serialize.constructor "message_level" "error" []
-let to_message_level =
- Serialize.do_match "message_level" (fun s args -> match s with
- | "debug" -> Debug (Serialize.raw_string args)
- | "info" -> Info
- | "notice" -> Notice
- | "warning" -> Warning
- | "error" -> Error
- | _ -> raise Serialize.Marshal_error)
-
-let of_message msg =
- let lvl = of_message_level msg.message_level in
- let content = Serialize.of_xml msg.message_content in
- Xml_datatype.Element ("message", [], [lvl; content])
-let to_message xml = match xml with
- | Xml_datatype.Element ("message", [], [lvl; content]) -> {
- message_level = to_message_level lvl;
- message_content = Serialize.to_xml content }
- | _ -> raise Serialize.Marshal_error
-
-let is_message = function
- | Xml_datatype.Element ("message", _, _) -> true
- | _ -> false
-
-
type edit_id = int
type state_id = Stateid.t
type edit_or_state_id = Edit of edit_id | State of state_id
@@ -71,8 +34,10 @@ type feedback_content =
| GlobDef of Loc.t * string * string * string
| FileDependency of string option * string
| FileLoaded of string * string
+ (* Extra metadata *)
| Custom of Loc.t * string * xml
- | Message of message
+ (* Old generic messages *)
+ | Message of level * Richpp.richpp
type feedback = {
id : edit_or_state_id;
@@ -80,94 +45,6 @@ type feedback = {
route : route_id;
}
-let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
- | "addedaxiom", _ -> AddedAxiom
- | "processed", _ -> Processed
- | "processingin", [where] -> ProcessingIn (to_string where)
- | "incomplete", _ -> Incomplete
- | "complete", _ -> Complete
- | "globref", [loc; filepath; modpath; ident; ty] ->
- GlobRef(to_loc loc, to_string filepath,
- to_string modpath, to_string ident, to_string ty)
- | "globdef", [loc; ident; secpath; ty] ->
- GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
- | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s)
- | "inprogress", [n] -> InProgress (to_int n)
- | "workerstatus", [ns] ->
- let n, s = to_pair to_string to_string ns in
- WorkerStatus(n,s)
- | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
- | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
- | "filedependency", [from; dep] ->
- FileDependency (to_option to_string from, to_string dep)
- | "fileloaded", [dirpath; filename] ->
- FileLoaded (to_string dirpath, to_string filename)
- | "message", [m] -> Message (to_message m)
- | _ -> raise Marshal_error)
-let of_feedback_content = function
- | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
- | Processed -> constructor "feedback_content" "processed" []
- | ProcessingIn where ->
- constructor "feedback_content" "processingin" [of_string where]
- | Incomplete -> constructor "feedback_content" "incomplete" []
- | Complete -> constructor "feedback_content" "complete" []
- | GlobRef(loc, filepath, modpath, ident, ty) ->
- constructor "feedback_content" "globref" [
- of_loc loc;
- of_string filepath;
- of_string modpath;
- of_string ident;
- of_string ty ]
- | GlobDef(loc, ident, secpath, ty) ->
- constructor "feedback_content" "globdef" [
- of_loc loc;
- of_string ident;
- of_string secpath;
- of_string ty ]
- | ErrorMsg(loc, s) ->
- constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
- | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
- | WorkerStatus(n,s) ->
- constructor "feedback_content" "workerstatus"
- [of_pair of_string of_string (n,s)]
- | Goals (loc,s) ->
- constructor "feedback_content" "goals" [of_loc loc;of_string s]
- | Custom (loc, name, x) ->
- constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
- | FileDependency (from, depends_on) ->
- constructor "feedback_content" "filedependency" [
- of_option of_string from;
- of_string depends_on]
- | FileLoaded (dirpath, filename) ->
- constructor "feedback_content" "fileloaded" [
- of_string dirpath;
- of_string filename ]
- | Message m -> constructor "feedback_content" "message" [ of_message m ]
-
-let of_edit_or_state_id = function
- | Edit id -> ["object","edit"], of_edit_id id
- | State id -> ["object","state"], Stateid.to_xml id
-
-let of_feedback msg =
- let content = of_feedback_content msg.contents in
- let obj, id = of_edit_or_state_id msg.id in
- let route = string_of_int msg.route in
- Element ("feedback", obj @ ["route",route], [id;content])
-let to_feedback xml = match xml with
- | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
- id = Edit(to_edit_id id);
- route = int_of_string route;
- contents = to_feedback_content content }
- | Element ("feedback", ["object","state";"route",route], [id;content]) -> {
- id = State(Stateid.of_xml id);
- route = int_of_string route;
- contents = to_feedback_content content }
- | _ -> raise Marshal_error
-
-let is_feedback = function
- | Element ("feedback", _, _) -> true
- | _ -> false
-
let default_route = 0
(** Feedback and logging *)
@@ -264,11 +141,8 @@ let feedback ?id ?route what =
}
let feedback_logger lvl msg =
- feedback ~route:!feedback_route ~id:!feedback_id (
- Message {
- message_level = lvl;
- message_content = Richpp.of_richpp (Richpp.richpp_of_pp msg);
- })
+ feedback ~route:!feedback_route ~id:!feedback_id
+ (Message (lvl, Richpp.richpp_of_pp msg))
(* Output to file *)
let ft_logger old_logger ft level mesg =