From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 1 Dec 2000 16:52:18 +0000 (+0000)
Subject: Minor modifications
X-Git-Tag: nogzip~117
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9b41de644d4cb6768310d2d5e55e29476cb0a938;p=helm.git

Minor modifications
---

diff --git a/helm/interface/Makefile b/helm/interface/Makefile
index 2697b7d52..d2fddf453 100644
--- a/helm/interface/Makefile
+++ b/helm/interface/Makefile
@@ -1,8 +1,8 @@
-LABLGTK_DIR = /usr/local/lib/ocaml/lablgtk
-LABLGTK_MATHVIEW_DIR = /usr/local/lib/ocaml/lablgtk/mathview
-MINIDOM_DIR = /usr/local/lib/ocaml/minidom
-PXP_DIR = /usr/local/lib/ocaml/site-lib/pxp
-NETSTRING_DIR = /usr/local/lib/ocaml/site-lib/netstring
+LABLGTK_DIR = /usr/lib/ocaml/lablgtk
+LABLGTK_MATHVIEW_DIR = /usr/lib/ocaml/lablgtk/mathview
+MINIDOM_DIR = /usr/lib/ocaml/minidom
+PXP_DIR = /usr/lib/ocaml/site-lib/pxp
+NETSTRING_DIR = /usr/lib/ocaml/site-lib/netstring
 OCAMLC = ocamlc -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview
 OCAMLOPT = ocamlopt -I $(LABLGTK_DIR) -I $(LABLGTK_MATHVIEW_DIR) -I mlgtk_devel -I $(PXP_DIR) -I $(NETSTRING_DIR) -I $(MINIDOM_DIR) -I mlmathview
 OCAMLDEP = ocamldep
diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index 05e19f288..5cd0faf0c 100755
--- a/helm/interface/mmlinterface.ml
+++ b/helm/interface/mmlinterface.ml
@@ -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