Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 37 insertions, 3 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index f19cd91c9b..3d489dcb54 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -19,6 +19,7 @@ open Printer
 open Environ
 open Evarutil
 open Evd
+open Decl_mode
 open Hipattern
 open Tacmach
 open Reductionops
@@ -110,7 +111,9 @@ let is_in_coq_path f =
     false  
 
 let is_in_proof_mode () = 
-  try ignore (get_pftreestate ()); true with _ -> false
+  match Decl_mode.get_current_mode () with
+      Decl_mode.Mode_none -> false
+    | _ -> true
 
 let user_error_loc l s =
   raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
@@ -252,6 +255,7 @@ type hyp = env * evar_map *
            ((identifier * string) * constr option * constr) * 
            (string * string)
 type concl = env * evar_map * constr * string
+type meta = env * evar_map * string
 type goal = hyp list * concl
 
 let prepare_hyp sigma env ((i,c,d) as a) =
@@ -273,6 +277,37 @@ let prepare_goal sigma g =
   (prepare_hyps sigma env,
    (env, sigma, g.evar_concl, msg (pr_lconstr_env_at_top env g.evar_concl)))
 
+let prepare_hyps_filter info sigma env =
+  assert (rel_context env = []);
+  let hyps =
+    fold_named_context
+      (fun env ((id,_,_) as d) acc ->
+	 if true || Idset.mem id info.pm_hyps then
+	   let hyp = prepare_hyp sigma env d in hyp :: acc
+	 else acc)
+      env ~init:[] 
+  in
+  List.rev hyps
+
+let prepare_meta sigma env (m,typ)  =
+  env, sigma, 
+  (msg (str " ?" ++ int m ++ str " : " ++ pr_lconstr_env_at_top env typ))
+
+let prepare_metas info sigma env =
+  List.fold_right 
+    (fun cpl acc ->  
+      let meta = prepare_meta sigma env cpl in meta :: acc)
+    info.pm_subgoals [] 
+
+let get_current_pm_goal () =
+  let pfts = get_pftreestate ()  in
+  let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in
+  let info = Decl_mode.get_info gls.it in
+  let env = pf_env gls in
+  let sigma= sig_sig gls in
+    (prepare_hyps_filter info sigma env,
+     prepare_metas info sigma env)
+
 let get_current_goals () = 
     let pfts = get_pftreestate () in
     let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
@@ -281,14 +316,13 @@ let get_current_goals () =
 
 let get_current_goals_nb () = 
   try List.length (get_current_goals ()) with _ -> 0
-
   
 let print_no_goal () =
     let pfts = get_pftreestate () in
     let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in 
     assert (gls = []);
     let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in
-    msg (Printer.pr_subgoals sigma gls)
+    msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls)
 
 
 type word_class = Normal | Kwd | Reserved