From cffe0bf6b541c6322e89ef6827d3e7d9f299bbe4 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 11 May 2012 15:28:49 +0000
Subject: Slightly modified the coqtop interface by adding an identifier in
 goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15303 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/interface.mli | 2 ++
 lib/serialize.ml  | 8 +++++---
 2 files changed, 7 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/interface.mli b/lib/interface.mli
index a72e5b7b0f..52b5dbb7cb 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -15,6 +15,8 @@ type verbose = bool
 
 (** The type of coqtop goals *)
 type goal = {
+  goal_id : string;
+  (** Unique goal identifier *)
   goal_hyp : string list;
   (** List of hypotheses *)
   goal_ccl : string;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 3b43861314..a793e800eb 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -311,13 +311,15 @@ let to_evar = function
 let of_goal g =
   let hyp = of_list of_string g.goal_hyp in
   let ccl = of_string g.goal_ccl in
-  Element ("goal", [], [hyp; ccl])
+  let id = of_string g.goal_id in
+  Element ("goal", [], [id; hyp; ccl])
 
 let to_goal = function
-| Element ("goal", [], [hyp; ccl]) ->
+| Element ("goal", [], [id; hyp; ccl]) ->
   let hyp = to_list to_string hyp in
   let ccl = to_string ccl in
-  { goal_hyp = hyp; goal_ccl = ccl }
+  let id = to_string id in
+  { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
 | _ -> raise Marshal_error
 
 let of_goals g =
-- 
cgit v1.2.3