X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=64c068fc3b55da06d7a70dd1ff28806d6f7bc9e9;hb=4ef40e8fb4de63f9699268b389f052007bc87f54;hp=06248f9ba61062d726cb60ae04786dd36bb31730;hpb=e6a36a24f7c27739067073172a387b85cd0a6c5c;p=helm.git

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index 06248f9ba..64c068fc3 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
@@ -205,45 +229,32 @@ let prev rendering_window () =
 ;;
 
 (* called when an hyperlink is clicked *)
-let jump rendering_window node =
- let module M = Minidom in
-  let s =
-   match M.node_get_attribute node (M.mDOMString_of_string "href") with
-      None   -> assert false
-    | Some s -> M.string_of_mDOMString s
-  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
-;;
-
-let choose_selection rendering_window node =
- let module M = Minidom in
- let rec aux ~first_time node =
-  match M.node_get_attribute node (M.mDOMString_of_string "xref") with
-     None ->
-      let parent =
-       match M.node_get_parent node with
-          None -> assert false
-        | Some parent -> parent
-      in
-       aux ~first_time:false parent
-   | Some s ->
-      if not first_time then
-       rendering_window#output#set_selection (Some node)
- in
-  match node with
-     None      -> () (* No element selected *)
-   | Some node -> aux ~first_time:true node
+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 -> assert false
 ;;
 
-let changefont rendering_window () =
- rendering_window#output#set_font_size rendering_window#spinb#value_as_int
+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)
+   | None   -> aux (node#get_parent)
+  in
+   match node with
+     Some x -> aux x
+   | None   -> rendering_window#output#set_selection None
 ;;
 
 
@@ -274,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
@@ -304,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 () =
@@ -339,41 +357,38 @@ let check rendering_window () =
 ;;
 
 let annotateb_pressed rendering_window annotation_window () =
- let module M = Minidom in
+ let module O = Ominidom in
  match rendering_window#output#get_selection with
-    None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
-  | Some node ->
-     let xpath =
-      match M.node_get_attribute node (M.mDOMString_of_string "xref") with
-         None -> assert false
-       | Some xpath -> M.string_of_mDOMString xpath
-     in
-      try
-       let annobj = get_annotated_obj ()
+ | 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#get_string) ;
+      CicAnnotationHinter.create_hints annotation_window annobj (xpath#get_string) ;
+      annotation#delete_text 0 annotation#length ;
+      begin
+       match !(!ann) with
+           None      ->
+            annotation#misc#set_sensitive false ;
+            annotation_window#radio_none#set_active true ;
+            radio_some_status := false
+         | Some ann' ->
+            annotation#insert ann' ;
+            annotation#misc#set_sensitive true ;
+            annotation_window#radio_some#set_active true ;
+            radio_some_status := true
+      end ;
+      GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
+      annotation_window#show () ;
+   | None ->
        (* 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 ;
-        annotation#delete_text 0 annotation#length ;
-        begin
-         match !(!ann) with
-             None      ->
-              annotation#misc#set_sensitive false ;
-              annotation_window#radio_none#set_active true ;
-              radio_some_status := false
-           | Some ann' ->
-              annotation#insert ann' ;
-              annotation#misc#set_sensitive true ;
-              annotation_window#radio_some#set_active true ;
-              radio_some_status := true
-        end ;
-        GMain.Grab.add (annotation_window#window_to_annotate#coerce) ;
-        annotation_window#show () ;
-      with
-        e ->
-         (* 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")
+       let errors = (rendering_window#errors : GEdit.text) in
+        errors#insert ("\nNo xref found\n")
+  end
+ | None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
 ;;
 
 (* called when the annotation is confirmed *)
@@ -383,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
@@ -407,21 +422,136 @@ 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 
 ;;
 
+(* Stuff for the widget settings *)
+
+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 
+ button_export_to_postscript button_t1 ()
+=
+ let is_set = button_t1#active in
+  output#set_font_manager_type
+   (if is_set then `font_manager_t1 else `font_manager_gtk) ;
+  if is_set then
+   begin
+    button_set_anti_aliasing#misc#set_sensitive true ;
+    button_set_kerning#misc#set_sensitive true ;
+    button_export_to_postscript#misc#set_sensitive true ;
+   end
+  else
+   begin
+    button_set_anti_aliasing#misc#set_sensitive false ;
+    button_set_kerning#misc#set_sensitive false ;
+    button_export_to_postscript#misc#set_sensitive false ;
+   end
+;;
+
+let set_anti_aliasing output button_set_anti_aliasing () =
+ output#set_anti_aliasing button_set_anti_aliasing#active
+;;
+
+let set_kerning output button_set_kerning () =
+ output#set_kerning button_set_kerning#active
+;;
+
+let changefont output font_size_spinb () =
+ output#set_font_size font_size_spinb#value_as_int
+;;
+
+let set_log_verbosity output log_verbosity_spinb () =
+ output#set_log_verbosity log_verbosity_spinb#value_as_int
+;;
+
+class settings_window output sw button_export_to_postscript jump_callback
+ selection_changed_callback
+=
+ let settings_window = GWindow.window ~title:"GtkMathView settings" () in
+ let vbox =
+  GPack.vbox ~packing:settings_window#add () in
+ let table =
+  GPack.table
+   ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+   ~border_width:5 ~packing:vbox#add () in
+ let button_t1 =
+  GButton.toggle_button ~label:"activate t1 fonts"
+   ~packing:(table#attach ~left:0 ~top:0) () in
+ let button_set_anti_aliasing =
+  GButton.toggle_button ~label:"set_anti_aliasing"
+   ~packing:(table#attach ~left:1 ~top:0) () in
+ let button_set_kerning =
+  GButton.toggle_button ~label:"set_kerning"
+   ~packing:(table#attach ~left:2 ~top:0) () in
+ let table =
+  GPack.table
+   ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+   ~border_width:5 ~packing:vbox#add () in
+ let font_size_label =
+  GMisc.label ~text:"font size:"
+   ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
+ let font_size_spinb =
+  let sadj =
+   GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
+  in
+   GEdit.spin_button 
+    ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
+ let log_verbosity_label =
+  GMisc.label ~text:"log verbosity:"
+   ~packing:(table#attach ~left:0 ~top:1) () in
+ let log_verbosity_spinb =
+  let sadj =
+   GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
+  in
+   GEdit.spin_button 
+    ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
+ let hbox =
+  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let closeb =
+  GButton.button ~label:"Close"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+object(self)
+ method show = settings_window#show
+ initializer
+  button_set_anti_aliasing#misc#set_sensitive false ;
+  button_set_kerning#misc#set_sensitive false ;
+  (* Signals connection *)
+  ignore(button_t1#connect#clicked
+   (activate_t1 output button_set_anti_aliasing button_set_kerning
+    button_export_to_postscript button_t1)) ;
+  ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
+  ignore(button_set_anti_aliasing#connect#toggled
+   (set_anti_aliasing output button_set_anti_aliasing));
+  ignore(button_set_kerning#connect#toggled
+   (set_kerning output button_set_kerning)) ;
+  ignore(log_verbosity_spinb#connect#changed
+   (set_log_verbosity output log_verbosity_spinb)) ;
+  ignore(closeb#connect#clicked settings_window#misc#hide)
+end;;
+
+(* Main windows *)
+
 class annotation_window output label =
  let window_to_annotate =
   GWindow.window ~title:"Annotating environment" ~border_width:2 () in
@@ -481,7 +611,8 @@ object (self)
      in
       visited_uris := new_current_uri::(List.tl !visited_uris) ;
        label#set_text (UriManager.string_of_uri new_current_uri) ;
-       output#load (parse_no_cache new_current_uri)
+       let mmlfile = parse_no_cache new_current_uri in
+        output#load mmlfile
    )) ;
   ignore (abortb#connect#clicked
    (fun () ->
@@ -504,7 +635,7 @@ class rendering_window annotation_window output (label : GMisc.label) =
   GPack.vbox ~packing:window#add () in
  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
  let paned =
-  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
+  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let scrolled_window0 =
   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
  let _ = scrolled_window0#add output#coerce in
@@ -526,13 +657,12 @@ class rendering_window annotation_window output (label : GMisc.label) =
  let annotateb =
   GButton.button ~label:"Annotate"
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let spinb =
-  let sadj =
-   GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
-  in
-   GEdit.spin_button 
-    ~adjustment:sadj ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5)
-    () in
+ let settingsb =
+  GButton.button ~label:"Settings"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let button_export_to_postscript =
+  GButton.button ~label:"export_to_postscript"
+  ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  let closeb =
   GButton.button ~label:"Close"
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -540,23 +670,28 @@ object(self)
  method nextb = nextb
  method prevb = prevb
  method label = label
- method spinb = spinb
  method output = (output : GMathView.math_view)
  method errors = errors
  method show () = window#show ()
  initializer
   nextb#misc#set_sensitive false ;
   prevb#misc#set_sensitive false ;
+  button_export_to_postscript#misc#set_sensitive false ;
 
   (* signal handlers here *)
   ignore(output#connect#jump (jump 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)) ;
-  ignore(spinb#connect#changed (changefont 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
+   button_export_to_postscript (jump self) (choose_selection self) in
+  ignore(settingsb#connect#clicked settings_window#show) ;
+  ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
 end;;
 
@@ -569,7 +704,7 @@ class theory_rendering_window rendering_window =
   GMisc.label ~text:"???"
    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
  let paned =
-  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in
+  GPack.paned `HORIZONTAL ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let scrolled_window0 =
   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
  let output =
@@ -589,13 +724,12 @@ class theory_rendering_window rendering_window =
  let checkb =
   GButton.button ~label:"Check"
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- let spinb =
-  let sadj =
-   GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
-  in
-   GEdit.spin_button 
-    ~adjustment:sadj ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5)
-    () in
+ let settingsb =
+  GButton.button ~label:"Settings"
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let button_export_to_postscript =
+  GButton.button ~label:"export_to_postscript"
+  ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  let closeb =
   GButton.button ~label:"Close"
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -605,11 +739,11 @@ object(self)
  method label = label
  method output = (output : GMathView.math_view)
  method errors = errors
- method spinb = spinb
  method show () = window#show ()
  initializer
   nextb#misc#set_sensitive false ;
   prevb#misc#set_sensitive false ;
+  button_export_to_postscript#misc#set_sensitive false ;
 
   (* signal handlers here *)
   ignore(output#connect#jump (jump rendering_window)) ;
@@ -617,7 +751,10 @@ object(self)
   ignore(nextb#connect#clicked (theory_next self)) ;
   ignore(prevb#connect#clicked (theory_prev self)) ;
   ignore(checkb#connect#clicked (theory_check self)) ;
-  ignore(spinb#connect#changed (changefont self)) ;
+  let settings_window = new settings_window output scrolled_window0
+   button_export_to_postscript (jump rendering_window)(choose_selection self) in
+  ignore(settingsb#connect#clicked settings_window#show) ;
+  ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
   ignore(closeb#connect#clicked window#misc#hide) ;
   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true ))
 end;;
@@ -629,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 =
@@ -652,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