X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=496e35e55527af64d82782983d18b8a642d0483c;hb=21029c2bc06d1467c21763abe36aaaf7b8afd8ca;hp=2dfc5e4f9f8cadd2e60476b0b3ba5a47409f1b12;hpb=0e4b2d04d664c513754c9308fc0a4923aa56783e;p=helm.git diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 2dfc5e4f9..496e35e55 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -230,7 +230,7 @@ let jump rendering_window node = let choose_selection rendering_window node = let module M = Minidom in - let rec aux ~first_time node = + let rec aux node = match M.node_get_attribute node (M.mDOMString_of_string "xref") with None -> let parent = @@ -238,14 +238,12 @@ let choose_selection rendering_window node = 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) + aux parent + | Some s -> !(rendering_window#output)#set_selection (Some node) in match node with - None -> () (* No element selected *) - | Some node -> aux ~first_time:true node + None -> !(rendering_window#output)#set_selection None + | Some node -> aux node ;; @@ -430,27 +428,46 @@ let export_to_postscript output () = !output#export_to_postscript "output.ps" ; ;; -let activate_t1 output sw is_set jump_callback selection_changed_callback - last_uri () +let activate_t1 output button_set_anti_aliasing button_set_kerning + button_export_to_postscript sw button_t1 jump_callback + selection_changed_callback last_uri () = - is_set := not !is_set ; - sw#remove !output#coerce ; - output := - (GMathView.math_view ~packing:sw#add ~width:400 ~height:380 - ~use_t1_lib:!is_set ()) ; - !output#load !last_uri ; - ignore(!output#connect#jump jump_callback) ; - ignore(!output#connect#selection_changed selection_changed_callback) ; -;; - -let set_anti_aliasing output is_set () = - is_set := not !is_set ; - !output#set_anti_aliasing !is_set -;; - -let set_kerning output is_set () = - is_set := not !is_set ; - !output#set_kerning !is_set + let is_set = button_t1#active in + sw#remove !output#coerce ; + let font_size = !output#get_font_size in + let log_verbosity = !output#get_log_verbosity in + let anti_aliasing = button_set_anti_aliasing#active in + let kerning = button_set_kerning#active in + output := + (GMathView.math_view ~packing:sw#add ~width:400 ~height:380 + ~use_t1_lib:is_set ()) ; + !output#set_font_size font_size ; + !output#set_log_verbosity log_verbosity ; + 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 ; + !output#set_anti_aliasing anti_aliasing ; + !output#set_kerning kerning ; + 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 ; + !output#load !last_uri ; + ignore(!output#connect#jump jump_callback) ; + ignore(!output#connect#selection_changed selection_changed_callback) ; +;; + +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 () = @@ -461,47 +478,70 @@ let set_log_verbosity output log_verbosity_spinb () = !output#set_log_verbosity log_verbosity_spinb#value_as_int ;; -class settings_window output sw jump_callback selection_changed_callback - last_uri +class settings_window output sw button_export_to_postscript jump_callback + selection_changed_callback last_uri = let settings_window = GWindow.window ~title:"GtkMathView settings" () in - let table = GPack.table ~rows:5 ~columns:5 ~packing:settings_window#add () 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:4 ~top:2) () in - let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:3) () in - let button_set_kerning = - GButton.toggle_button ~label:"set_kerning" - ~packing:(table#attach ~left:3 ~top:3) () in + ~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:2 ~top:2) () in + ~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 *) - let is_set_use_t1_lib = ref false in - ignore(button_t1#connect#clicked - (activate_t1 output sw is_set_use_t1_lib jump_callback - selection_changed_callback last_uri)) ; + ignore(button_t1#connect#clicked + (activate_t1 output button_set_anti_aliasing button_set_kerning + button_export_to_postscript sw button_t1 jump_callback + selection_changed_callback last_uri)) ; ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; - let is_set_anti_aliasing = ref false in - ignore(button_set_anti_aliasing#connect#toggled - (set_anti_aliasing output is_set_anti_aliasing)); - let is_set_kerning = ref false in - ignore(button_set_kerning#connect#toggled - (set_kerning output is_set_kerning)) ; + 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)) + (set_log_verbosity output log_verbosity_spinb)) ; + ignore(closeb#connect#clicked settings_window#misc#hide) end;; (* Main windows *) @@ -590,7 +630,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 @@ -631,6 +671,7 @@ object(self) 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)) ; @@ -641,7 +682,7 @@ object(self) 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 - (jump self) (choose_selection self) loaded_uri in + button_export_to_postscript (jump self) (choose_selection self) loaded_uri 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 )) @@ -656,7 +697,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 = @@ -696,6 +737,7 @@ object(self) 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)) ; @@ -704,7 +746,8 @@ object(self) ignore(prevb#connect#clicked (theory_prev self)) ; ignore(checkb#connect#clicked (theory_check self)) ; let settings_window = new settings_window output scrolled_window0 - (jump rendering_window) (choose_selection self) theory_loaded_uri in + button_export_to_postscript (jump rendering_window) (choose_selection self) + theory_loaded_uri 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) ;