X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=b95303d2f0805cac49c62d046f6bbec222ec8822;hb=fb158d51c621e55962a6139d03cd1678cfb2e8f1;hp=05e19f2881bb7661127862a092d9613037d3f04c;hpb=f1e359680060835d3cd2f3859fa2896a1d9ac1ae;p=helm.git diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 05e19f288..b95303d2f 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + (******************************************************************************) (* *) (* PROJECT HELM *) @@ -109,7 +134,6 @@ let to_visit_uris = ref [];; exception NoCurrentUri;; exception NoNextOrPrevUri;; -exception GtkInterfaceInternalError;; let theory_get_current_uri () = match !theory_visited_uris with @@ -204,35 +228,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 ;; @@ -263,29 +285,13 @@ let selection_changed rendering_window uri () = update_output rendering_window uri' ;; -(* CSC: unificare con la creazione la prima volta *) -let rec updateb_pressed theory_rendering_window rendering_window - (sw1, sw ,(hbox : GPack.box)) mktree () -= - Getter.update () ; - (* let's empty the uri trees and rebuild them *) - uritree := [] ; - theoryuritree := [] ; - build_uri_tree () ; - hbox#remove !sw1#coerce ; - hbox#remove !sw#coerce ; - +let create_gtk_trees (hbox : GPack.box) rendering_window theory_rendering_window mktree = let sw3 = GBin.scrolled_window ~width:250 ~height:600 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let tree1 = GTree.tree ~selection_mode:`BROWSE ~packing:sw3#add_with_viewport () in let tree_item1 = GTree.tree_item ~label:"theory:/" ~packing:tree1#append () in - sw1 := sw3 ; - ignore(tree_item1#connect#select - (theory_selection_changed theory_rendering_window None)) ; - mktree theory_selection_changed theory_rendering_window tree_item1 - (Dir ("theory:/",theoryuritree)) ; let sw2 = GBin.scrolled_window ~width:250 ~height:600 @@ -293,9 +299,32 @@ let rec updateb_pressed theory_rendering_window rendering_window let tree = GTree.tree ~selection_mode:`BROWSE ~packing:sw2#add_with_viewport () in let tree_item = GTree.tree_item ~label:"cic:/" ~packing:tree#append () in - sw := sw2 ; + ignore(tree_item#connect#select (selection_changed rendering_window None)) ; - mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) + mktree selection_changed rendering_window tree_item (Dir ("cic:/",uritree)) ; + + ignore(tree_item1#connect#select + (theory_selection_changed theory_rendering_window None)) ; + mktree theory_selection_changed theory_rendering_window tree_item1 + (Dir ("theory:/",theoryuritree)) ; + (sw3,sw2) +;; + +let updateb_pressed theory_rendering_window rendering_window + (sw1, sw ,(hbox : GPack.box)) mktree () += + Getter.update () ; + (* let's empty the uri trees and rebuild them *) + uritree := [] ; + theoryuritree := [] ; + build_uri_tree () ; + hbox#remove !sw1#coerce ; + hbox#remove !sw#coerce ; + let (sw3,sw2) = + create_gtk_trees hbox rendering_window theory_rendering_window mktree + in + sw1 := sw3 ; + sw := sw2 ;; let theory_check rendering_window () = @@ -369,7 +398,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 @@ -393,16 +422,22 @@ let mktree selection_changed rendering_window = Dir (dirname, content) -> let subtree = GTree.tree () in treeitem#set_subtree subtree ; - List.iter - (fun ti -> - let label = get_name ti - and uri = get_uri ti in - let treeitem2 = GTree.tree_item ~label:label () in - subtree#append treeitem2 ; - ignore(treeitem2#connect#select - (selection_changed rendering_window uri)) ; - aux treeitem2 ti - ) (List.sort compare !content) + let expand_sons = + List.map + (fun ti -> + let label = get_name ti + and uri = get_uri ti in + let treeitem2 = GTree.tree_item ~label:label () in + subtree#append treeitem2 ; + ignore(treeitem2#connect#select + (selection_changed rendering_window uri)) ; + (* Almost lazy function *) + (fun () -> aux treeitem2 ti) + ) (List.sort compare !content) + in + let lazy_expand_sons = lazy (List.iter (fun f -> f ()) expand_sons) in + ignore(treeitem#connect#expand + (fun () -> Lazy.force lazy_expand_sons)) ; | _ -> () in aux @@ -648,7 +683,9 @@ object(self) ignore(output#connect#selection_changed (choose_selection self)) ; ignore(nextb#connect#clicked (next self)) ; ignore(prevb#connect#clicked (prev self)) ; - ignore(checkb#connect#clicked (check self)) ; + (* LUCA: check disabled while compression is not fully implemented *) + (* ignore(checkb#connect#clicked (check self)) ; *) + checkb#misc#set_sensitive false ; ignore(closeb#connect#clicked window#misc#hide) ; ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ; let settings_window = new settings_window output scrolled_window0 @@ -729,18 +766,9 @@ class selection_window theory_rendering_window rendering_window = let win = GWindow.window ~title:"Known uris" ~border_width:2 () in let vbox = GPack.vbox ~packing:win#add () in let hbox1 = GPack.hbox ~packing:(vbox#pack ~padding:5) () in - let sw1 = GBin.scrolled_window ~width:250 ~height:600 - ~packing:(hbox1#pack ~padding:5) () in - let tree1 = - GTree.tree ~selection_mode:`BROWSE ~packing:sw1#add_with_viewport () in - let tree_item1 = - GTree.tree_item ~label:theorylabel ~packing:tree1#append () in - let sw = GBin.scrolled_window ~width:250 ~height:600 - ~packing:(hbox1#pack ~padding:5) () in - let tree = - GTree.tree ~selection_mode:`BROWSE ~packing:sw#add_with_viewport () in - let tree_item = - GTree.tree_item ~label:label ~packing:tree#append () in + let (sw1,sw) = + create_gtk_trees hbox1 rendering_window theory_rendering_window mktree + in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let updateb = @@ -752,16 +780,7 @@ class selection_window theory_rendering_window rendering_window = object (self) method show () = win#show () initializer - mktree theory_selection_changed theory_rendering_window tree_item1 - (Dir ("theory:/",theoryuritree)); - mktree selection_changed rendering_window tree_item - (Dir ("cic:/",uritree)); - (* signal handlers here *) - ignore (tree_item1#connect#select - ~callback:(theory_selection_changed theory_rendering_window None)) ; - ignore (tree_item#connect#select - ~callback:(selection_changed rendering_window None)) ; ignore (win#connect#destroy ~callback:GMain.Main.quit) ; ignore (quitb#connect#clicked GMain.Main.quit) ; ignore(updateb#connect#clicked (updateb_pressed @@ -772,6 +791,8 @@ end;; (* MAIN *) let _ = + (* first of all initialize the processor by requiring the desired stylesheets *) + XsltProcessor.initialize () ; build_uri_tree () ; let output = GMathView.math_view ~width:400 ~height:380 () and label = GMisc.label ~text:"???" () in