diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/feedback.ml | 136 | ||||
| -rw-r--r-- | lib/feedback.mli | 20 | ||||
| -rw-r--r-- | lib/richpp.ml | 4 | ||||
| -rw-r--r-- | lib/richpp.mli | 5 | ||||
| -rw-r--r-- | lib/stateid.ml | 18 | ||||
| -rw-r--r-- | lib/stateid.mli | 8 |
6 files changed, 17 insertions, 174 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml index dce4372ec0..d6f580fd16 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 = diff --git a/lib/feedback.mli b/lib/feedback.mli index 1e96f9a497..50ffd22db9 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -16,20 +16,12 @@ type level = | Warning | Error -type message = { - message_level : level; - message_content : xml; -} - -val of_message : message -> xml -val to_message : xml -> message -val is_message : xml -> bool - (** Coq "semantic" infos obtained during parsing/execution *) type edit_id = int type state_id = Stateid.t type edit_or_state_id = Edit of edit_id | State of state_id + type route_id = int val default_route : route_id @@ -54,18 +46,14 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Old generic messages *) - | Message of message + | Message of level * Richpp.richpp type feedback = { - id : edit_or_state_id; (* The document part concerned *) + id : edit_or_state_id; (* The document part concerned *) contents : feedback_content; (* The payload *) - route : route_id; (* Extra routing info *) + route : route_id; (* Extra routing info *) } -val of_feedback : feedback -> xml -val to_feedback : xml -> feedback -val is_feedback : xml -> bool - (** {6 Feedback sent, even asynchronously, to the user interface} *) (** Moved here from pp.ml *) diff --git a/lib/richpp.ml b/lib/richpp.ml index fe3edd99ca..a98273edb2 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -194,7 +194,3 @@ let raw_print xml = let () = print xml in Buffer.contents buf -let of_richpp x = Element ("richpp", [], [x]) -let to_richpp xml = match xml with -| Element ("richpp", [], [x]) -> x -| _ -> raise Serialize.Marshal_error diff --git a/lib/richpp.mli b/lib/richpp.mli index 807d52aba4..287d265a8f 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -57,10 +57,7 @@ val richpp_of_string : string -> richpp val repr : richpp -> Xml_datatype.xml (** Observe the styled text as XML *) -(** {5 Serialization} *) - -val of_richpp : richpp -> Xml_datatype.xml -val to_richpp : Xml_datatype.xml -> richpp +(** {5 Debug/Compat} *) (** Represent the semi-structured document as a string, dropping any additional information. *) diff --git a/lib/stateid.ml b/lib/stateid.ml index 59cf206e2e..c17df2b321 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Xml_datatype - type t = int let initial = 1 let dummy = 0 @@ -15,20 +13,14 @@ let fresh, in_range = let cur = ref initial in (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur) let to_string = string_of_int -let of_int id = assert(in_range id); id +let of_int id = + (* Coqide too to parse ids too, but cannot check if they are valid. + * Hence we check for validity only if we are an ide slave. *) + if !Flags.ide_slave then assert (in_range id); + id let to_int id = id let newer_than id1 id2 = id1 > id2 -let of_xml = function - | Element ("state_id",["val",i],[]) -> - let id = int_of_string i in - (* Coqide too to parse ids too, but cannot check if they are valid. - * Hence we check for validity only if we are an ide slave. *) - if !Flags.ide_slave then assert(in_range id); - id - | _ -> raise (Invalid_argument "to_state_id") -let to_xml i = Element ("state_id",["val",string_of_int i],[]) - let state_id_info : (t * t) Exninfo.t = Exninfo.make () let add exn ?(valid = initial) id = Exninfo.add exn state_id_info (valid, id) diff --git a/lib/stateid.mli b/lib/stateid.mli index 2c12c30c3c..516ad891ff 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Xml_datatype - type t val equal : t -> t -> bool @@ -19,13 +17,11 @@ val initial : t val dummy : t val fresh : unit -> t val to_string : t -> string + val of_int : int -> t val to_int : t -> int -val newer_than : t -> t -> bool -(* XML marshalling *) -val to_xml : t -> xml -val of_xml : xml -> t +val newer_than : t -> t -> bool (* Attaches to an exception the concerned state id, plus an optional * state id that is a valid state id before the error. |