diff options
| -rw-r--r-- | checker/check.mllib | 2 | ||||
| -rw-r--r-- | dev/printers.mllib | 2 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 2 | ||||
| -rw-r--r-- | lib/feedback.ml | 46 | ||||
| -rw-r--r-- | lib/feedback.mli | 19 | ||||
| -rw-r--r-- | lib/pp.ml | 45 | ||||
| -rw-r--r-- | lib/pp.mli | 7 | ||||
| -rw-r--r-- | stm/stm.ml | 1 |
8 files changed, 87 insertions, 37 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index cbabd208c..22df37562 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -17,6 +17,8 @@ Control Pp_control Loc Serialize +Stateid +Feedback Pp Segmenttree Unicodetable diff --git a/dev/printers.mllib b/dev/printers.mllib index 8477df76c..4afa9d4fc 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -20,6 +20,8 @@ Flags Control Loc Serialize +Stateid +Feedback Pp Segmenttree Unicodetable diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index a18951f4b..0b168377d 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -16,6 +16,8 @@ Pp_control Flags Loc Serialize +Stateid +Feedback Pp Errors CList diff --git a/lib/feedback.ml b/lib/feedback.ml index 4eb611157..27ed44724 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -9,6 +9,49 @@ open Xml_datatype open Serialize +type message_level = + | Debug of string + | Info + | Notice + | Warning + | Error + +type message = { + message_level : message_level; + message_content : string; +} + +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_string 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_string 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 @@ -26,6 +69,7 @@ type feedback_content = | ProcessingInMaster | Goals of Loc.t * string | FileLoaded of string * string + | Message of message type feedback = { id : edit_or_state_id; @@ -51,6 +95,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "goals", [loc;s] -> Goals (to_loc loc, to_string s) | "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" [] @@ -83,6 +128,7 @@ let of_feedback_content = function 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 diff --git a/lib/feedback.mli b/lib/feedback.mli index c245ec76a..b3c0c8896 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -8,6 +8,24 @@ open Xml_datatype +(* Old plain messages (used to be in Pp) *) +type message_level = + | Debug of string + | Info + | Notice + | Warning + | Error + +type message = { + message_level : message_level; + message_content : string; +} + +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 @@ -26,6 +44,7 @@ type feedback_content = | ProcessingInMaster | Goals of Loc.t * string | FileLoaded of string * string + | Message of message type feedback = { id : edit_or_state_id; @@ -345,50 +345,23 @@ let msgerrnl x = msgnl_with !err_ft x (* Logging management *) -type message_level = +type message_level = Feedback.message_level = | Debug of string | Info | Notice | Warning | Error -type message = { +type message = Feedback.message = { message_level : message_level; message_content : string; } -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_string 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_string content } - | _ -> raise Serialize.Marshal_error - -let is_message = function - | Xml_datatype.Element ("message", _, _) -> true - | _ -> false +let of_message = Feedback.of_message +let to_message = Feedback.to_message +let is_message = Feedback.is_message type logger = message_level -> std_ppcmds -> unit -type modern_logger = id:Feedback.edit_or_state_id -> message_level -> std_ppcmds -> unit let print_color s x = x (* FIXME *) @@ -421,7 +394,6 @@ let msg_error x = !logger ~id:!feedback_id Error x let msg_debug x = !logger ~id:!feedback_id (Debug "_") x let set_logger l = logger := (fun ~id:_ lvl msg -> l lvl msg) -let set_modern_logger (l : modern_logger) = logger := l let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg @@ -445,6 +417,13 @@ let string_of_ppcmds c = msg_with Format.str_formatter c; Format.flush_str_formatter () +let log_via_feedback () = logger := (fun ~id lvl msg -> + !feeder { + Feedback.content = Feedback.Message { + message_level = lvl; + message_content = string_of_ppcmds msg }; + Feedback.id = id }) + (* Copy paste from Util *) let pr_comma () = str "," ++ spc () diff --git a/lib/pp.mli b/lib/pp.mli index ef7f6d11a..ebb6290f9 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -78,14 +78,14 @@ val close : unit -> std_ppcmds val tclose : unit -> std_ppcmds (** {6 Sending messages to the user} *) -type message_level = +type message_level = Feedback.message_level = | Debug of string | Info | Notice | Warning | Error -type message = { +type message = Feedback.message = { message_level : message_level; message_content : string; } @@ -115,8 +115,7 @@ val std_logger : logger val set_logger : logger -> unit -type modern_logger = id:Feedback.edit_or_state_id -> message_level -> std_ppcmds -> unit -val set_modern_logger : modern_logger -> unit +val log_via_feedback : unit -> unit val of_message : message -> Xml_datatype.xml val to_message : Xml_datatype.xml -> message diff --git a/stm/stm.ml b/stm/stm.ml index eb1c4df1b..697fd9c8f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1107,6 +1107,7 @@ end = struct feedback_queue := []; flush oc in Pp.set_feeder (slave_feeder !slave_oc); + Pp.log_via_feedback (); Universes.set_remote_new_univ_level (bufferize (fun () -> marshal_response !slave_oc RespGetCounterNewUnivLevel; match unmarshal_more_data !slave_ic with |