From: Claudio Sacerdoti Coen 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