X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=pa_goal.ml;h=c95095c78259c34df8c6a0be86a93f777df56d70;hb=c233ce39dd4be632238faba62e93ff4b9a48766e;hp=13ea23c81ced03b1de612dca10794531ce4b7908;hpb=087ea609510e7c85e1048219f4aa96348d1eaeda;p=goaljobs.git

diff --git a/pa_goal.ml b/pa_goal.ml
index 13ea23c..c95095c 100644
--- a/pa_goal.ml
+++ b/pa_goal.ml
@@ -91,6 +91,8 @@ let generate_let_goal _loc (r : rec_flag) (lets : binding) =
         (* Define a goal name which the body may use. *)
         let goalname = $str:name$ in
 
+        _enter_goal goalname;
+
         (* Source location. *)
         let goalloc = $str:goalloc$ in
 
@@ -114,6 +116,7 @@ let generate_let_goal _loc (r : rec_flag) (lets : binding) =
           $body$ ;
           _call_onruns ();
           _call_onsuccesses ();
+          _leave_goal goalname;
 
           (* Avoid a compiler warning: *)
           ignore (goalname); ignore (goalloc)
@@ -123,9 +126,11 @@ let generate_let_goal _loc (r : rec_flag) (lets : binding) =
          * ordinary function exit.
          *)
         | Goal_result Goal_OK ->
+          _leave_goal goalname;
           _call_onsuccesses ();
           ()
         | exn ->
+          _leave_goal goalname;
           _call_onfails exn;
           raise exn
       >> in
@@ -155,7 +160,7 @@ let generate_let_goal _loc (r : rec_flag) (lets : binding) =
           let () = publish $str:name$ (
             function
             | [] ->
-              Goaljobs.require $lid:gname$
+              Goaljobs.require $str:name$ $lid:gname$
             | _ ->
               failwith (Printf.sprintf "goal '%s' does not take any arguments"
                           $str:name$);
@@ -168,20 +173,23 @@ let generate_let_goal _loc (r : rec_flag) (lets : binding) =
  * 'expr' is a function call.
  *)
 let generate_require _loc expr =
-  (* Note that 'f a b c' is parsed as '((f a) b) c' so the actually
+  (* Note that 'f a b c' is parsed as '((f a) b) c' so the actual
    * function name is buried deeply in the tree.  Rewrite the name.
    *)
   let rec rewrite = function
     | ExApp (_loc, ExId (_loc1, IdLid (_loc2, name)), right) ->
       let gname = "goal_" ^ name in
-      ExApp (_loc, ExId (_loc1, IdLid (_loc2, gname)), right)
+      ExApp (_loc, ExId (_loc1, IdLid (_loc2, gname)), right), name
+
     | ExApp (_loc, (ExApp _ as expr), right) ->
-      ExApp (_loc, rewrite expr, right)
+      let expr, name = rewrite expr in
+      ExApp (_loc, expr, right), name
+
     | _ ->
       locfail _loc "require (...) expression must contain a call to a goal"
   in
-  let expr = rewrite expr in
-  <:expr< Goaljobs.require (fun () -> $expr$) >>
+  let expr, name = rewrite expr in
+  <:expr< Goaljobs.require $str:name$ (fun () -> $expr$) >>
 
 ;;