- match C.get_current_scratch_infos () with
- (* term is the whole goal in the scratch_area *)
- Some (term,ids_to_terms, ids_to_father_ids,_) ->
- let term_of_node node =
- let xpath =
- ((node : Gdome.element)#getAttributeNS
- ~namespaceURI:Misc.helmns
- ~localName:(G.domString "xref"))#to_string
- in
- if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
- else
- let id = xpath in
- Hashtbl.find ids_to_terms id
- in
- let terms = List.map term_of_node l in
- let expr = tactic terms term in
- let mml,scratch_infos =
- ApplyStylesheets.mml_of_cic_term 111 expr
- in
- C.set_current_scratch_infos (Some scratch_infos) ;
- scratch_window#show () ;
- scratch_window#mmlwidget#load_doc ~dom:mml
- | None -> assert false (* "ERROR: No current term!!!" *)
+ let expr = tactic terms scratch_window#term in
+ scratch_window#sequent_viewer#load_sequent
+ scratch_window#metasenv (111,scratch_window#context,expr) ;
+ scratch_window#set_term expr ;
+ scratch_window#show () ;