+ refresh_sequent rendering_window#proofw
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | None -> assert false (* "ERROR: No selection!!!" *)
+;;
+
+let focus rendering_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ match rendering_window#output#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ (*CSC: OCAML DIVERGE
+ ((element : G.element)#getAttributeNS
+ *)
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ try
+ match !current_cic_infos with
+ Some (ids_to_terms, ids_to_father_ids, _, _) ->
+ let id = xpath in
+ L.focus id ids_to_terms ids_to_father_ids ;
+ refresh_sequent rendering_window#proofw
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | None -> assert false (* "ERROR: No selection!!!" *)
+;;
+
+exception NoPrevGoal;;
+exception NoNextGoal;;
+
+let prevgoal metasenv metano =
+ let rec aux =
+ function
+ [] -> assert false
+ | [(m,_,_)] -> raise NoPrevGoal
+ | (n,_,_)::(m,_,_)::_ when m=metano -> n
+ | _::tl -> aux tl
+ in
+ aux metasenv
+;;
+
+let nextgoal metasenv metano =
+ let rec aux =
+ function
+ [] -> assert false
+ | [(m,_,_)] when m = metano -> raise NoNextGoal
+ | (m,_,_)::(n,_,_)::_ when m=metano -> n
+ | _::tl -> aux tl
+ in
+ aux metasenv
+;;
+
+let prev_or_next_goal select_goal rendering_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let metasenv =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
+ in
+ let metano =
+ match !ProofEngine.goal with
+ None -> assert false
+ | Some m -> m
+ in
+ try
+ ProofEngine.goal := Some (select_goal metasenv metano) ;
+ refresh_sequent rendering_window#proofw
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")