]> matita.cs.unibo.it Git - helm.git/commitdiff
Adding settings to the widget
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 9 Nov 2000 10:38:17 +0000 (10:38 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 9 Nov 2000 10:38:17 +0000 (10:38 +0000)
helm/interface/cadet
helm/interface/mmlinterface.ml

index 0c3768055f1ddc4b3753a1032b61085cc4ad0e47..aedf5b7007ae6b1bffb75035443cd67fe0665f95 100755 (executable)
@@ -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/
index 06248f9ba61062d726cb60ae04786dd36bb31730..bc72b09a725d5cd80a2090ffc813eb0c45db9383 100755 (executable)
@@ -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