X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FcicMathView.ml;h=e06e0055d6da93d8ea9531fceca880048f5d3609;hb=3c8da07d7a5d7cf0432a83732a6d103f527afaef;hp=ea7fd5160ee58e1821f5e92770f644f51c44530e;hpb=b804ff9f8fba300ffaa54add291e0f6490b757ce;p=helm.git

diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml
index ea7fd5160..e06e0055d 100644
--- a/matita/matita/cicMathView.ml
+++ b/matita/matita/cicMathView.ml
@@ -30,19 +30,16 @@ open MatitaGtkMisc
 open MatitaGuiTypes
 open GtkSourceView2
 
-let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; grafite_status: GrafiteTypes.status; setGoal: int option -> unit >));;
+let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; status: GrafiteTypes.status >));;
 let register_matita_script_current f = matita_script_current := f;;
 let get_matita_script_current () = !matita_script_current ();;
 
-type document_element = string
+type document_element = (int * int * string) list * string (* hyperlinks,text *)
 
 class type cicMathView =
 object
   inherit GObj.widget
 
-  method set_font_size: int -> unit
-  method update_font_size: unit
-
   method load_root : root:document_element -> unit
   method remove_selections: unit
   method set_selection: document_element option -> unit
@@ -70,10 +67,10 @@ let xref_ds = Gdome.domString "xref"
 
   (** Gdome.element of a MathML document whose rendering should be blank. Used
   * by cicBrowser to render "about:blank" document *)
-let empty_mathml = lazy ""
+let empty_mathml = lazy ([],"")
 
   (** shown for goals closed by side effects *)
-let closed_goal_mathml = lazy "chiuso per side effect..."
+let closed_goal_mathml = lazy ([],"chiuso per side effect...")
 
 (*
 let rec has_maction (elt :Gdome.element) = 
@@ -182,33 +179,84 @@ object (self)
   inherit GSourceView2.source_view obj
 
   method strings_of_selection = (assert false : (paste_kind * string) list)
-  method update_font_size =
-   self#misc#modify_font_by_name
-     (sprintf "%s %d" BuildTimeConf.script_font (MatitaMisc.get_current_font_size ()))
-  method set_href_callback = (function _ -> () : (string -> unit) option -> unit)
+
+  val mutable href_callback: (string -> unit) option = None
+  method set_href_callback f = href_callback <- f
+
+  val mutable href_statusbar_msg:
+    (GMisc.statusbar_context * Gtk.statusbar_message) option = None
+    (* <statusbar ctxt, statusbar msg> *)
+
   method private set_cic_info = (function _ -> () : unit (*(Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t *
          (Cic.id, Cic.hypothesis) Hashtbl.t *
          (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option)*) option -> unit)
   (* dal widget di Luca *)
-  method load_root ~root =
-    self#buffer#delete ~start:(self#buffer#get_iter `START)
-    ~stop:(self#buffer#get_iter `END);
-    self#buffer#insert root
+  method load_root ~root:(hyperlinks,text) =
+    self#buffer#set_text text;
+    let all_tag = self#buffer#create_tag [] in
+    self#buffer#apply_tag all_tag ~start:(self#buffer#get_iter `START)
+     ~stop:(self#buffer#get_iter `END);
+    ignore(all_tag#connect#event
+      ~callback:(fun ~origin event pos ->
+        match GdkEvent.get_type event with
+         | `MOTION_NOTIFY -> 
+             Gdk.Window.set_cursor
+              (match self#get_window `TEXT with None -> assert false | Some x -> x)
+              (Gdk.Cursor.create `ARROW);
+             HExtlib.iter_option (fun (ctxt, msg) -> ctxt#remove msg)
+              href_statusbar_msg;
+             false
+         | _ -> false));
+     let hyperlink_tag = self#buffer#create_tag [] in
+     ignore(hyperlink_tag#connect#event
+       ~callback:(fun ~origin event pos ->
+         let offset = (new GText.iter pos)#offset in
+         let _,_,href =
+          try
+           List.find
+            (fun (start,stop,href) -> start <= offset && offset <= stop
+            ) hyperlinks
+          with
+           Not_found -> assert false
+         in
+         match GdkEvent.get_type event with
+            `BUTTON_PRESS -> 
+              (match href_callback with
+                  None -> ()
+                | Some f -> f href);
+              true
+          | `MOTION_NOTIFY -> 
+              Gdk.Window.set_cursor
+               (match self#get_window `TEXT with None -> assert false | Some x -> x)
+               (Gdk.Cursor.create `HAND1);
+              let ctxt = (MatitaMisc.get_gui ())#main#statusBar#new_context ~name:"href" in
+              let msg = ctxt#push href in
+              href_statusbar_msg <- Some (ctxt, msg);
+              false
+          | _ -> false));
+     List.iter
+      ( fun (start,stop,(href : string)) ->
+          self#buffer#apply_tag hyperlink_tag
+           ~start:(self#buffer#get_iter_at_char start)
+           ~stop:(self#buffer#get_iter_at_char (stop+1));
+      ) hyperlinks
+
+
   method action_toggle = (fun _ -> assert false : document_element -> bool)
   method remove_selections = (() : unit)
   method set_selection = (fun _ -> () : document_element option -> unit)
   method get_selections = (assert false : document_element list)
-  method set_font_size font_size =
-   self#misc#modify_font_by_name
-     (sprintf "%s %d" BuildTimeConf.script_font font_size)
 
   initializer
-    self#set_font_size (MatitaMisc.get_current_font_size ());
     self#source_buffer#set_language (Some MatitaGtkMisc.matita_lang);
     self#source_buffer#set_highlight_syntax true;
-    self#set_editable false
+    self#set_editable false;
+    MatitaMisc.observe_font_size
+     (fun size ->
+       self#misc#modify_font_by_name
+        (sprintf "%s %d" BuildTimeConf.script_font size))
 
-(* MATITA1.0
+(* MATITA 1.0
   inherit GMathViewAux.multi_selection_math_view obj
 
   val mutable href_callback: (string -> unit) option = None
@@ -223,7 +271,6 @@ object (self)
   val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW
 
   initializer
-    self#set_font_size (MatitaMisc.get_current_font_size ());
     ignore (self#connect#selection_changed self#choose_selection_cb);
     ignore (self#event#connect#button_press self#button_press_cb);
     ignore (self#event#connect#button_release self#button_release_cb);
@@ -448,8 +495,6 @@ object (self)
     | None -> self#set_selection None);
     selection_changed <- true
 
-  method update_font_size = self#set_font_size (MatitaMisc.get_current_font_size ())
-
     (** find a term by id from stored CIC infos @return either `Hyp if the id
      * correspond to an hypothesis or `Term (cic, hyp) if the id correspond to a
      * term. In the latter case hyp is either None (if the term is a subterm of
@@ -600,7 +645,7 @@ object (self)
     let sequent = List.assoc metano metasenv in
     let txt =
      ApplyTransformation.ntxt_of_cic_sequent
-      ~map_unicode_to_tex:false 80 status metasenv subst (metano,sequent)
+      ~map_unicode_to_tex:false 80 status ~metasenv ~subst (metano,sequent)
     in
     (* MATITA 1.0 if BuildTimeConf.debug then begin
       let name =
@@ -625,7 +670,7 @@ object (self)
         self#thaw
     |  _ ->
 *)
-        (* MATITA1.0 if BuildTimeConf.debug then begin
+        (* MATITA 1.0 if BuildTimeConf.debug then begin
           let name =
            "/tmp/cic_browser_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
           HLog.debug ("cic_browser: dumping MathML to ./" ^ name);