- let ty =
- CicTypeChecker.type_of_aux' metasenv
- (P.cic_context_of_named_context context) term
- in
- let (meta,perforated) =
- (* If the selected term is already a meta, we return it. *)
- (* Otherwise, we are trying to refine a non-meta term... *)
- match term with
- Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
- | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
- in
- perforated
+ let ty = CicTypeChecker.type_of_aux' metasenv context term in
+ P.perforate context term ty (* P.perforate also sets the goal *)
+;;
+
+exception FocusOnlyOnMeta;;
+
+(* If the current selection is a Meta, that Meta becomes the current goal *)
+let focus id ids_to_terms ids_to_father_ids =
+ let module P = ProofEngine in
+ let term = Hashtbl.find ids_to_terms id in
+ let context = get_context ids_to_terms ids_to_father_ids id in
+ let metasenv =
+ match !P.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
+ in
+ let ty = CicTypeChecker.type_of_aux' metasenv context term in
+ match term with
+ Cic.Meta (n,_) -> P.goal := Some n
+ | _ -> raise FocusOnlyOnMeta