X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2Fmmlinterface.ml;h=bc72b09a725d5cd80a2090ffc813eb0c45db9383;hb=2c55219403e079024a0e6a4741e10b13b7ea8219;hp=d364ffe4b0257efbff9d48eb0da54a8742f83741;hpb=413a5e0b1fde6296a09a6651cef7948bc408c6e4;p=helm.git

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index d364ffe4b..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 () =
@@ -205,19 +205,45 @@ let prev rendering_window () =
 ;;
 
 (* called when an hyperlink is clicked *)
-let jump rendering_window s =
- 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 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 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
 ;;
 
 
@@ -313,36 +339,41 @@ let check rendering_window () =
 ;;
 
 let annotateb_pressed rendering_window annotation_window () =
- let xpath = (rendering_window#output#get_selection : string option) in
-  match xpath with
-     None -> (rendering_window#errors : GEdit.text)#insert "\nNo selection!\n"
-   | Some xpath ->
-    try
-     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 ;
-      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 ->
+ let module M = Minidom 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 ()
        (* 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")
+       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")
 ;;
 
 (* called when the annotation is confirmed *)
@@ -391,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
@@ -430,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 *)
@@ -450,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 () ->
@@ -476,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
@@ -495,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
@@ -518,13 +596,15 @@ object(self)
   prevb#misc#set_sensitive false ;
 
   (* signal handlers here *)
-  ignore(output#connect#jump (jump 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;;
 
@@ -541,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
@@ -557,34 +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#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;;
@@ -640,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