+ method string_of_selected_terms =
+ let get_id (node: Gdome.element) =
+ let xref_attr =
+ node#getAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref_ds
+ in
+ xref_attr#to_string
+ in
+ let script = MatitaScript.instance () in
+ let metasenv = script#proofMetasenv in
+ let context = script#proofContext in
+ let conclusion = script#proofConclusion in
+ let cic_terms =
+ List.map
+ (fun node -> self#get_term_by_id context (get_id node))
+ self#get_selections
+ in
+(* TODO: code for patterns
+ let conclusion = (MatitaScript.instance ())#proofConclusion in
+ let conclusion_pattern =
+ ProofEngineHelpers.pattern_of ~term:conclusion cic_terms
+ in
+*)
+ let dummy_goal = ~-1 in
+ let cic_sequent =
+ match cic_terms with
+ | [] -> assert false
+ | `Term t :: _ ->
+ let context' =
+ ProofEngineHelpers.locate_in_conjecture t
+ (dummy_goal, context, conclusion)
+ in
+ dummy_goal, context', t
+ | `Hyp context :: _ -> dummy_goal, context, Cic.Rel 1
+ in
+(* TODO: code for patterns
+ (* TODO context shouldn't be empty *)
+ let cic_sequent = ~-1, [], conclusion_pattern 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 =
+ CicNotationRew.ast_of_acic ids_to_inner_sorts annterm
+ in
+ let pped_ast = CicNotationRew.pp_ast ast in
+ let markup = CicNotationPres.render ids_to_uris pped_ast in
+ BoxPp.render_to_string text_width markup
+