X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=2688fc1befcb86fdb90fd1e270dfa2fe84a4a85a;hb=4e1bc40b1d12427dbd8e3c749fba7aa9ab1797b9;hp=a164883a5c47cde36bda6ee58e82a7ddea76629d;hpb=458ba0f68b06b74a3d947c6496dc23a509715a89;p=helm.git

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index a164883a5..2688fc1be 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
@@ -207,30 +206,30 @@ let prev rendering_window () =
 (* called when an hyperlink is clicked *)
 let jump rendering_window (node : Ominidom.o_mDOMNode) =
  let module O = Ominidom in
-  let s = (node#get_attribute (O.o_mDOMString_of_string "href"))#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
+  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 -> assert false
 ;;
 
 let choose_selection rendering_window (node : Ominidom.o_mDOMNode option) =
  let module O = Ominidom in
- let rec aux node =
-  try
-   let _ = node#get_attribute (O.o_mDOMString_of_string "xref") in
-    rendering_window#output#set_selection node
-  with
-   O.Minidom_exception _ ->
-    aux (node#get_parent)
- in
-  match node with
-     None      -> rendering_window#output#reset_selection
-   | Some node -> aux node
+  let rec aux node =
+   match node#get_attribute (O.o_mDOMString_of_string "xref") with
+     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
 ;;
 
 
@@ -261,29 +260,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
@@ -291,9 +274,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 () =
@@ -327,17 +333,16 @@ let check rendering_window () =
 
 let annotateb_pressed rendering_window annotation_window () =
  let module O = Ominidom in
- try
-  let node = rendering_window#output#get_selection in
-   let xpath =
-     (node#get_attribute (O.o_mDOMString_of_string "xref"))#get_string
-   in
-    try
+ match rendering_window#output#get_selection with
+ | Some node ->
+  begin
+   match (node#get_attribute (O.o_mDOMString_of_string "xref")) with
+   | Some xpath ->
      let annobj = get_annotated_obj ()
      (* next "cast" can't got rid of, but I don't know why *)
      and annotation = (annotation_window#annotation : GEdit.text) in
-      ann := CicXPath.get_annotation annobj xpath ;
-      CicAnnotationHinter.create_hints annotation_window annobj xpath ;
+      ann := CicXPath.get_annotation annobj (xpath#get_string) ;
+      CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
       annotation#delete_text 0 annotation#length ;
       begin
        match !(!ann) with
@@ -353,14 +358,12 @@ let annotateb_pressed rendering_window annotation_window () =
       end ;
       GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
       annotation_window#show () ;
-    with
-      e ->
+   | None ->
        (* next "cast" can't got rid of, but I don't know why *)
        let errors = (rendering_window#errors : GEdit.text) in
-        errors#insert ("\n" ^ Printexc.to_string e ^ "\n")
- with
-  O.Minidom_exception _ ->
-    (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
+        errors#insert ("\nNo xref found\n")
+  end
+ | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
 ;;
 
 (* called when the annotation is confirmed *)
@@ -370,7 +373,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
@@ -394,16 +397,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 
@@ -411,9 +420,8 @@ let mktree selection_changed rendering_window =
 
 (* Stuff for the widget settings *)
 
-let export_to_postscript output () =
- output#export_to_postscript ~width:595 ~height:822 ~x_margin:72
-  ~y_margin:72 ~disable_colors:false "output.ps" ;
+let export_to_postscript (output : GMathView.math_view) () =
+ output#export_to_postscript ~filename:"output.ps" ();
 ;;
 
 let activate_t1 output button_set_anti_aliasing button_set_kerning 
@@ -421,10 +429,7 @@ let activate_t1 output button_set_anti_aliasing button_set_kerning
 =
  let is_set = button_t1#active in
   output#set_font_manager_type
-   (if is_set then
-     GtkMathView.MathView.FontManagerT1
-    else
-     GtkMathView.MathView.FontManagerGtk) ;
+   (if is_set then `font_manager_t1 else `font_manager_gtk) ;
   if is_set then
    begin
     button_set_anti_aliasing#misc#set_sensitive true ;
@@ -734,18 +739,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 =
@@ -757,16 +753,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