exception NoCurrentUri;;
exception NoNextOrPrevUri;;
-exception GtkInterfaceInternalError;;
let theory_get_current_uri () =
match !theory_visited_uris with
rendering_window#prevb#misc#set_sensitive false
;;
-exception SomethingWrong
-
(* called when an hyperlink is clicked *)
let jump rendering_window (node : Ominidom.o_mDOMNode) =
let module O = Ominidom in
match (node#get_attribute (O.o_mDOMString_of_string "href")) with
- | Some str ->
- let s = str#get_string in
- let uri = UriManager.uri_of_string s in
- rendering_window#show () ;
- rendering_window#prevb#misc#set_sensitive true ;
- rendering_window#nextb#misc#set_sensitive false ;
- visited_uris := uri::!visited_uris ;
- to_visit_uris := [] ;
- annotated_obj := None ;
- update_output rendering_window uri
- | None -> raise SomethingWrong
+ Some str ->
+ let s = str#get_string in
+ let uri = UriManager.uri_of_string s in
+ rendering_window#show () ;
+ rendering_window#prevb#misc#set_sensitive true ;
+ rendering_window#nextb#misc#set_sensitive false ;
+ visited_uris := uri::!visited_uris ;
+ to_visit_uris := [] ;
+ annotated_obj := None ;
+ update_output rendering_window uri
+ | None -> assert false
;;
let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
let module O = Ominidom in
let rec aux node =
match node#get_attribute (O.o_mDOMString_of_string "xref") with
- | Some _ -> rendering_window#output#set_selection (Some node)
+ Some _ -> rendering_window#output#set_selection (Some node)
| None -> aux (node#get_parent)
in
- match node with
- | Some x -> aux x
- | None -> rendering_window#output#set_selection None
+ match node with
+ Some x -> aux x
+ | None -> rendering_window#output#set_selection None
;;
else
!ann := None ;
match !annotated_obj with
- None -> raise GtkInterfaceInternalError
+ None -> assert false
| Some (annobj,_) ->
let uri = get_current_uri () in
let annxml = Annotation2Xml.pp_annotation annobj uri in