From 7a7dd14e763d13887101834fc2288046740cb8a2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 24 Dec 2013 18:12:26 +0100
Subject: CoqIDE: new feedback "incomplete" to signal partial Qed

---
 lib/interface.mli | 2 ++
 lib/serialize.ml  | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'lib')

diff --git a/lib/interface.mli b/lib/interface.mli
index a01ec20aed..8d250f8507 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -127,6 +127,8 @@ type edit_or_state_id = Edit of edit_id | State of state_id
 type feedback_content =
   | AddedAxiom
   | Processed
+  | Incomplete
+  | Complete
   | GlobRef of Loc.t * string * string * string * string
   | ErrorMsg of Loc.t * string
   | InProgress of int
diff --git a/lib/serialize.ml b/lib/serialize.ml
index b1768d76dc..411fb9878e 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -328,6 +328,8 @@ let to_loc xml = match xml with
 let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "addedaxiom", _ -> AddedAxiom
   | "processed", _ -> Processed
+  | "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)
@@ -340,6 +342,8 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
 let of_feedback_content = function
   | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
   | Processed -> constructor "feedback_content" "processed" []
+  | Incomplete -> constructor "feedback_content" "incomplete" []
+  | Complete -> constructor "feedback_content" "complete" []
   | GlobRef(loc, filepath, modpath, ident, ty) ->
       constructor "feedback_content" "globref" [
         of_loc loc;
-- 
cgit v1.2.3