diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/interface.mli | 28 | ||||
| -rw-r--r-- | lib/pp.ml | 12 | ||||
| -rw-r--r-- | lib/pp.mli | 16 | ||||
| -rw-r--r-- | lib/serialize.ml | 36 | ||||
| -rw-r--r-- | lib/serialize.mli | 4 |
5 files changed, 83 insertions, 13 deletions
diff --git a/lib/interface.mli b/lib/interface.mli index 349f7baf98..d54fb84760 100644 --- a/lib/interface.mli +++ b/lib/interface.mli @@ -103,7 +103,7 @@ type coq_info = { compile_date : string; } -(** Coq messages *) +(** Coq unstructured messages *) type message_level = | Debug of string @@ -117,6 +117,20 @@ type message = { message_content : string; } +(** Coq "semantic" infos obtained during parsing/execution *) +type edit_id = int + +type feedback_content = + | AddedAxiom + | Processed + +type feedback = { + edit_id : edit_id; + content : feedback_content; +} + +(** Calls result *) + type location = (int * int) option (* start and end of the error *) type 'a value = @@ -126,18 +140,16 @@ type 'a value = (* Request/Reply message protocol between Coq and CoqIde *) -(** Running a command (given as a string). - The 1st flag indicates whether to use "raw" mode - (less sanity checks, no impact on the undo stack). - Suitable e.g. for queries, or for the Set/Unset +(** Running a command (given as its id and its text). + "raw" mode (less sanity checks, no impact on the undo stack) + is suitable for queries, or for the Set/Unset of display options that coqide performs all the time. - The 2nd flag controls the verbosity. The returned string contains the messages produced - by this command, but not the updated goals (they are + but not the updated goals (they are to be fetch by a separated [current_goals]). *) -type interp_sty = raw * verbose * string (* spiwack: [Inl] for safe and [Inr] for unsafe. *) type interp_rty = (string,string) Util.union +type interp_sty = edit_id * raw * verbose * string (** Backtracking by at least a certain number of phrases. No finished proofs will be re-opened. Instead, @@ -354,6 +354,18 @@ let msg_debug x = !logger (Debug "_") x let set_logger l = logger := l +(** Feedback *) + +let feeder = ref ignore +let feedback_id = ref 0 +let set_id_for_feedback i = feedback_id := i +let feedback what = + !feeder { + Interface.edit_id = !feedback_id; + Interface.content = what + } +let set_feeder f = feeder := f + (** Utility *) let string_of_ppcmds c = diff --git a/lib/pp.mli b/lib/pp.mli index b46115fd4a..bc7441836b 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -106,6 +106,22 @@ val std_logger : logger val set_logger : logger -> unit +(** {6 Feedback sent, even asynchronously, to the user interface *) + +(* This stuff should be available to most of the system, line msg_* above. + * But I'm unsure this is the right place, especially for the global edit_id. + * + * Morally the parser gets a string and an edit_id, and gives back an AST. + * Feedbacks during the parsing phase are attached to this edit_id. + * The interpreter assignes an exec_id to the ast, and feedbacks happening + * during interpretation are attached to the exec_id (still unimplemented, + * since the two phases are performed sequentially) *) + +val feedback : Interface.feedback_content -> unit + +val set_id_for_feedback : Interface.edit_id -> unit +val set_feeder : (Interface.feedback -> unit) -> unit + (** {6 Utilities} *) val string_of_ppcmds : std_ppcmds -> string diff --git a/lib/serialize.ml b/lib/serialize.ml index 0b9cc0a14f..fd8c7e7e4e 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -359,9 +359,10 @@ let to_value f = function | _ -> raise Marshal_error let of_call = function -| Interp (raw, vrb, cmd) -> +| Interp (id,raw, vrb, cmd) -> let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in - Element ("call", ("val", "interp") :: flags, [PCData cmd]) + Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags, + [PCData cmd]) | Rewind n -> Element ("call", ("val", "rewind") :: ["steps", string_of_int n], []) | Goal () -> @@ -394,9 +395,10 @@ let to_call = function let ans = massoc "val" attrs in begin match ans with | "interp" -> + let id = List.assoc "id" attrs in let raw = List.mem_assoc "raw" attrs in let vrb = List.mem_assoc "verbose" attrs in - Interp (raw, vrb, raw_string l) + Interp (int_of_string id, raw, vrb, raw_string l) | "rewind" -> let steps = int_of_string (massoc "steps" attrs) in Rewind steps @@ -525,6 +527,30 @@ let is_message = function | Element ("message", _, _) -> true | _ -> false +let to_feedback_content xml = do_match xml "feedback_content" + (fun s args -> match s with + | "addedaxiom" -> AddedAxiom + | "processed" -> Processed + | _ -> raise Marshal_error) + +let of_feedback_content = function +| AddedAxiom -> constructor "feedback_content" "addedaxiom" [] +| Processed -> constructor "feedback_content" "processed" [] + +let of_feedback msg = + let content = of_feedback_content msg.content in + Element ("feedback", ["id",string_of_int msg.edit_id], [content]) + +let to_feedback xml = match xml with +| Element ("feedback", ["id",id], [content]) -> + { edit_id = int_of_string id; + content = to_feedback_content content } +| _ -> raise Marshal_error + +let is_feedback = function +| Element ("feedback", _, _) -> true +| _ -> false + (** Conversions between ['a value] and xml answers When decoding an xml answer, we dynamically check that it is compatible @@ -617,10 +643,10 @@ let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" let pr_union pr1 pr2 = function Util.Inl x -> pr1 x | Util.Inr x -> pr2 x let pr_call = function - | Interp (r,b,s) -> + | Interp (id,r,b,s) -> let raw = if r then "RAW" else "" in let verb = if b then "" else "SILENT" in - "INTERP"^raw^verb^" ["^s^"]" + "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]" | Rewind i -> "REWIND "^(string_of_int i) | Goal _ -> "GOALS" | Evars _ -> "EVARS" diff --git a/lib/serialize.mli b/lib/serialize.mli index 3ecf066bef..4af4d09749 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -48,6 +48,10 @@ val of_message : message -> xml val to_message : xml -> message val is_message : xml -> bool +val of_feedback : feedback -> xml +val to_feedback : xml -> feedback +val is_feedback : xml -> bool + val of_answer : 'a call -> 'a value -> xml val to_answer : xml -> 'a call -> 'a value |