From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 9 Nov 2000 11:46:57 +0000 (+0000)
Subject: New improvements
X-Git-Tag: nogzip~187
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=0e4b2d04d664c513754c9308fc0a4923aa56783e

New improvements
---

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index bc72b09a7..2dfc5e4f9 100755
--- a/helm/interface/mmlinterface.ml
+++ b/helm/interface/mmlinterface.ml
@@ -28,6 +28,10 @@ type item =
 let uritree = ref []
 let theoryuritree = ref []
 
+(* Brutti, per via del widget che non e' imperativo *)
+let loaded_uri = ref "";;
+let theory_loaded_uri = ref "";;
+
 let get_name =
  function
     Dir (name,_) -> name
@@ -142,6 +146,7 @@ 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
+   theory_loaded_uri := mmlfile ;
    !(rendering_window#output)#load mmlfile
 ;;
 
@@ -149,6 +154,7 @@ 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
+   loaded_uri := mmlfile ;
    !(rendering_window#output)#load mmlfile
 ;;
 
@@ -242,10 +248,6 @@ let choose_selection rendering_window node =
    | Some node -> aux ~first_time:true node
 ;;
 
-let changefont rendering_window () =
- !(rendering_window#output)#set_font_size rendering_window#spinb#value_as_int
-;;
-
 
 let theory_selection_changed rendering_window uri () =
  match uri with
@@ -428,23 +430,44 @@ let export_to_postscript output () =
  !output#export_to_postscript "output.ps" ;
 ;;
 
-let activate_t1 output sw () =
+let activate_t1 output sw is_set jump_callback selection_changed_callback 
+ last_uri ()
+=
+ is_set := not !is_set ;
  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) ;
-*)
+ (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
+;;
 
-class settings_window output sw =
+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 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 button_t1 =
-  GButton.button ~label:"activate t1 fonts"
+  GButton.toggle_button ~label:"activate t1 fonts"
    ~packing:(table#attach ~left:0 ~top:0) () in
  let font_size_spinb =
   let sadj =
@@ -452,20 +475,33 @@ class settings_window output sw =
   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
+ 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
+ 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
 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)) ;
-*) ()
+  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(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(log_verbosity_spinb#connect#changed
+   (set_log_verbosity output log_verbosity_spinb))
 end;;
 
 (* Main windows *)
@@ -529,7 +565,9 @@ 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
+        loaded_uri := mmlfile ;
+        !output#load mmlfile
    )) ;
   ignore (abortb#connect#clicked
    (fun () ->
@@ -583,7 +621,6 @@ class rendering_window annotation_window output (label : GMisc.label) =
  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
@@ -603,6 +640,8 @@ object(self)
   ignore(checkb#connect#clicked (check 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
   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 ))
@@ -621,7 +660,7 @@ class theory_rendering_window rendering_window =
  let scrolled_window0 =
   GBin.scrolled_window ~border_width:10 ~packing:paned#add1 () in
  let output =
-  ref (GMathView.math_view ~use_t1_lib:true ~width:400 ~height:380
+  ref (GMathView.math_view ~use_t1_lib:false ~width:400 ~height:380
    ~packing:scrolled_window0#add ()) in
  let scrolled_window =
   GBin.scrolled_window
@@ -647,7 +686,6 @@ class theory_rendering_window rendering_window =
  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
@@ -665,6 +703,8 @@ object(self)
   ignore(nextb#connect#clicked (theory_next 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
   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) ;