From: Claudio Sacerdoti Coen Date: Thu, 9 Nov 2000 10:38:17 +0000 (+0000) Subject: Adding settings to the widget X-Git-Tag: nogzip~188 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c55219403e079024a0e6a4741e10b13b7ea8219;p=helm.git Adding settings to the widget --- diff --git a/helm/interface/cadet b/helm/interface/cadet index 0c3768055..aedf5b700 100755 --- a/helm/interface/cadet +++ b/helm/interface/cadet @@ -15,3 +15,7 @@ export LD_LIBRARY_PATH=/usr/local/lib:$LD_LIBRARY_PATH export HELM_CONFIGURATION_PREFIX=/home/cadet/sacerdot export T1LIB_CONFIG=./t1.config + +# Stix font +xset fp +xset fp+ /home/cadet/sacerdot/fonts/ diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml index 06248f9ba..bc72b09a7 100755 --- a/helm/interface/mmlinterface.ml +++ b/helm/interface/mmlinterface.ml @@ -142,14 +142,14 @@ let theory_update_output rendering_window uri = rendering_window#label#set_text (UriManager.string_of_uri uri) ; ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ; let mmlfile = XsltProcessor.process uri true "theory" in - rendering_window#output#load mmlfile + !(rendering_window#output)#load mmlfile ;; let update_output rendering_window uri = rendering_window#label#set_text (UriManager.string_of_uri uri) ; ignore (rendering_window#errors#delete_text 0 rendering_window#errors#length) ; let mmlfile = XsltProcessor.process uri true "cic" in - rendering_window#output#load mmlfile + !(rendering_window#output)#load mmlfile ;; let theory_next rendering_window () = @@ -235,7 +235,7 @@ let choose_selection rendering_window node = aux ~first_time:false parent | Some s -> if not first_time then - rendering_window#output#set_selection (Some node) + !(rendering_window#output)#set_selection (Some node) in match node with None -> () (* No element selected *) @@ -243,7 +243,7 @@ let choose_selection rendering_window node = ;; let changefont rendering_window () = - rendering_window#output#set_font_size rendering_window#spinb#value_as_int + !(rendering_window#output)#set_font_size rendering_window#spinb#value_as_int ;; @@ -340,7 +340,7 @@ let check rendering_window () = let annotateb_pressed rendering_window annotation_window () = let module M = Minidom in - match rendering_window#output#get_selection with + match !(rendering_window#output)#get_selection with None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n" | Some node -> let xpath = @@ -422,6 +422,54 @@ let mktree selection_changed rendering_window = aux ;; +(* Stuff for the widget settings *) + +let export_to_postscript output () = + !output#export_to_postscript "output.ps" ; +;; + +let activate_t1 output sw () = + sw#remove !output#coerce ; + output := + (GMathView.math_view ~packing:sw#add ~width:50 ~height:50 + ~use_t1_lib:true ()) ; +(* ignore(!mathview#connect#jump jump) ; + ignore(!mathview#connect#clicked clicked) ; + ignore(!mathview#connect#selection_changed selection_changed) ; +*) +;; + + +class settings_window output sw = + let settings_window = GWindow.window ~title:"GtkMathView settings" () in + let table = GPack.table ~rows:5 ~columns:5 ~packing:settings_window#add () in + let button_t1 = + GButton.button ~label:"activate t1 fonts" + ~packing:(table#attach ~left:0 ~top:0) () 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.button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:1 ~top:3) () in + let button_set_kerning = GButton.button ~label:"set_kerning" ~packing:(table#attach ~left:3 ~top:3) () in + let button_set_log_verbosity = GButton.button ~label:"set_log_verbosity" ~packing:(table#attach ~left:0 ~top:4) () in +object(self) + method show = settings_window#show + initializer + ignore(button_t1#connect#clicked (activate_t1 output sw)) ; + (*ignore(font_size_spinb#connect#changed (changefont self)) ;*) +(* + (* Signals connection *) + ignore(button_set_anti_aliasing#connect#clicked (set_anti_aliasing mathview)) ; + ignore(button_set_kerning#connect#clicked (set_kerning mathview)) ; + ignore(button_set_log_verbosity#connect#clicked (set_log_verbosity mathview)) ; +*) () +end;; + +(* Main windows *) + class annotation_window output label = let window_to_annotate = GWindow.window ~title:"Annotating environment" ~border_width:2 () in @@ -461,7 +509,7 @@ object (self) method radio_some = radio_some method radio_none = radio_none method annotation_hints = annotation_hints - method output = (output : GMathView.math_view) + method output = (output : GMathView.math_view ref) method show () = window_to_annotate#show () initializer (* signal handlers here *) @@ -481,7 +529,7 @@ 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) + !output#load (parse_no_cache new_current_uri) )) ; ignore (abortb#connect#clicked (fun () -> @@ -507,7 +555,7 @@ class rendering_window annotation_window output (label : GMisc.label) = GPack.paned `HORIZONTAL ~packing:(vbox#pack ~padding:5) () in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in - let _ = scrolled_window0#add output#coerce in + let _ = scrolled_window0#add !output#coerce in let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in @@ -526,22 +574,21 @@ 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 + let settings_window = new settings_window output scrolled_window0 in object(self) method nextb = nextb method prevb = prevb method label = label - method spinb = spinb - method output = (output : GMathView.math_view) + method output = (output : GMathView.math_view ref) method errors = errors method show () = window#show () initializer @@ -549,14 +596,15 @@ object(self) prevb#misc#set_sensitive false ; (* signal handlers here *) - ignore(output#connect#jump (jump self)) ; - ignore(output#connect#selection_changed (choose_selection self)) ; + 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)) ; ignore(closeb#connect#clicked window#misc#hide) ; ignore(annotateb#connect#clicked (annotateb_pressed self annotation_window)) ; + 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;; @@ -573,7 +621,8 @@ class theory_rendering_window rendering_window = let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in let output = - GMathView.math_view ~width:400 ~height:380 ~packing:scrolled_window0#add () in + ref (GMathView.math_view ~use_t1_lib:true ~width:400 ~height:380 + ~packing:scrolled_window0#add ()) in let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:paned#add2 ~width:240 ~height:100 () in @@ -589,35 +638,35 @@ 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 + let settings_window = new settings_window output scrolled_window0 in object(self) method nextb = nextb method prevb = prevb method label = label - method output = (output : GMathView.math_view) + method output = (output : GMathView.math_view ref) method errors = errors - method spinb = spinb method show () = window#show () initializer nextb#misc#set_sensitive false ; prevb#misc#set_sensitive false ; (* signal handlers here *) - ignore(output#connect#jump (jump rendering_window)) ; - ignore(output#connect#selection_changed (choose_selection self)) ; + ignore(!output#connect#jump (jump rendering_window)) ; + ignore(!output#connect#selection_changed (choose_selection 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)) ; + 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;; @@ -673,7 +722,8 @@ end;; let _ = build_uri_tree () ; - let output = GMathView.math_view ~width:400 ~height:380 () + let output = + ref (GMathView.math_view ~use_t1_lib:false ~width:400 ~height:380 ()) and label = GMisc.label ~text:"???" () in let annotation_window = new annotation_window output label in let rendering_window = new rendering_window annotation_window output label in