- if script#onGoingProof () then
- script#proofMetasenv
- else
- []
- in
- let string_of_cic_sequent cic_sequent =
- let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
- Cic2acic.asequent_of_sequent metasenv cic_sequent
- in
- let _, _, _, annterm = acic_sequent in
- let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
- in
- let pped_ast = TermContentPres.pp_ast ast in
- let markup = CicNotationPres.render ids_to_uris pped_ast in
- BoxPp.render_to_string text_width markup
- in
- let cic_info, unsh_sequent =
- match self#cic_info with
- | Some ((Some unsh_sequent, _, _, _, _, _) as info) ->
- info, unsh_sequent
- | Some ((None, _, _, _, _, _) as info) ->
- (* building a dummy sequent for obj *)
- let t = self#find_obj_conclusion id in
-(* HLog.debug (CicPp.ppterm t); *)
- info, (~-1, [], t)
- | None -> assert false
- in
- let paste_as_pattern_sequent term unsh_sequent =
- match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with
- | [context, _] ->
- (let context_len = List.length context in
- let _, unsh_context, conclusion = unsh_sequent in
- try
- (match
- List.nth unsh_context (List.length unsh_context - context_len - 1)
- with
- | None -> assert false (* can't select a restricted hyp *)
- | Some (name, Cic.Decl ty) ->
- let pattern =
- ProofEngineHelpers.pattern_of ~term:ty [term]
- in
-(* HLog.debug (CicPp.ppname name ^ ":" ^ CicPp.ppterm pattern); *)
- ~-1, [], pattern
- | Some (name, Cic.Def (bo, _)) ->
- let pattern =
- ProofEngineHelpers.pattern_of ~term:bo [term]
- in
-(* HLog.debug (CicPp.ppname name ^ ":=" ^ CicPp.ppterm pattern); *)
- ~-1, [], pattern)
- with Failure _ | Invalid_argument _ ->
- let pattern =
- ProofEngineHelpers.pattern_of ~term:conclusion [term]
- in
-(* HLog.debug ("\\vdash " ^ CicPp.ppterm pattern); *)
- ~-1, [], pattern)
- | _ -> assert false (* since it uses physical equality *)
- in
- let paste_as_term_sequent term unsh_sequent =
- let context' =
- match ProofEngineHelpers.locate_in_conjecture term unsh_sequent with
- | [context,_] -> context
- | _ -> assert false (* since it uses physical equality *)
- in
- ~-1, context', term
- in
+ if script#onGoingProof () then script#proofMetasenv else [] in
+ let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
+ Cic2acic.asequent_of_sequent metasenv cic_sequent in
+ let _, _, _, annterm = acic_sequent in
+ let ast, ids_to_uris =
+ TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in
+ let pped_ast = TermContentPres.pp_ast ast in
+ let markup = CicNotationPres.render ids_to_uris pped_ast in
+ BoxPp.render_to_string text_width markup
+
+ method private pattern_of term context unsh_sequent =
+ let context_len = List.length context in
+ let _, unsh_context, conclusion = unsh_sequent in
+ try
+ (match
+ List.nth unsh_context (List.length unsh_context - context_len - 1)
+ with
+ | None -> assert false (* can't select a restricted hypothesis *)
+ | Some (name, Cic.Decl ty) ->
+ ProofEngineHelpers.pattern_of ~term:ty [term]
+ | Some (name, Cic.Def (bo, _)) ->
+ ProofEngineHelpers.pattern_of ~term:bo [term])
+ with Failure _ | Invalid_argument _ ->
+ ProofEngineHelpers.pattern_of ~term:conclusion [term]
+
+ method private get_cic_info id =
+ match self#cic_info with
+ | Some ((Some unsh_sequent, _, _, _, _, _) as info) -> info, unsh_sequent
+ | Some ((None, _, _, _, _, _) as info) ->
+ let t = self#find_obj_conclusion id in
+ info, (~-1, [], t) (* dummy sequent for obj *)
+ | None -> assert false
+
+ method private sequent_of_id ~(paste_kind:paste_kind) id =
+ let cic_info, unsh_sequent = self#get_cic_info id in