]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/interface/mmlinterface.ml
Minor modifications
[helm.git] / helm / interface / mmlinterface.ml
index 05e19f2881bb7661127862a092d9613037d3f04c..5cd0faf0c999460cb0b7f67b0578758b46c4d80c 100755 (executable)
@@ -109,7 +109,6 @@ let to_visit_uris = ref [];;
 
 exception NoCurrentUri;;
 exception NoNextOrPrevUri;;
-exception GtkInterfaceInternalError;;
 
 let theory_get_current_uri () =
  match !theory_visited_uris with
@@ -204,35 +203,33 @@ let prev rendering_window () =
       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
 ;;
 
 
@@ -369,7 +366,7 @@ let save_annotation annotation =
  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