X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=255998c4f436884ab1e105136577bcb79528cf0c;hb=c83721701dbbd44d3d547fdec6c4a5658322f424;hp=7cb2aa7cbec948ef3cdfbad183f8e959eedd0fb8;hpb=fc15ad45208cc2e649fa435e547ecc757fe28481;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 7cb2aa7cb..255998c4f 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -65,9 +65,11 @@ let near (x1, y1) (x2, y2) =
   let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in
   (distance < 4.)
 
+let mathml_ns = Gdome.domString "http://www.w3.org/1998/Math/MathML"
 let xlink_ns = Gdome.domString "http://www.w3.org/1999/xlink"
 let helm_ns = Gdome.domString "http://www.cs.unibo.it/helm"
 let href_ds = Gdome.domString "href"
+let maction_ds = Gdome.domString "maction"
 let xref_ds = Gdome.domString "xref"
 
 let domImpl = Gdome.domImplementation ()
@@ -163,6 +165,18 @@ let hrefs_of_elt elt =
   else
     None
 
+let rec has_maction (elt :Gdome.element) = 
+  (* fix this comparison *)
+  if elt#get_tagName#to_string = "m:maction" ||
+   elt#get_tagName#to_string = "b:action" then
+    true
+  else 
+    match elt#get_parentNode with
+    | Some node when node#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE -> 
+        has_maction (new Gdome.element_of_node node)
+    | _ -> false
+;;
+
 class clickableMathView obj =
 let text_width = 80 in
 object (self)
@@ -176,7 +190,8 @@ object (self)
   method private cic_info = _cic_info
 
   val normal_cursor = Gdk.Cursor.create `LEFT_PTR
-  val href_cursor = Gdk.Cursor.create `HAND1
+  val href_cursor = Gdk.Cursor.create `HAND2
+  val maction_cursor = Gdk.Cursor.create `QUESTION_ARROW
 
   initializer
     self#set_font_size !current_font_size;
@@ -221,7 +236,11 @@ object (self)
       button_press_y <- GdkEvent.Button.y gdk_button;
       selection_changed <- false
     end else if button = right_button then
-      self#popup_contextual_menu (GdkEvent.Button.time gdk_button);
+      self#popup_contextual_menu 
+        (self#get_element_at 
+          (int_of_float (GdkEvent.Button.x gdk_button)) 
+          (int_of_float (GdkEvent.Button.y gdk_button)))  
+        (GdkEvent.Button.time gdk_button);
     false
 
   method private element_over_cb (elt_opt, _, _, _) =
@@ -233,6 +252,9 @@ object (self)
     in
     match elt_opt with
     | Some elt ->
+        if has_maction elt then
+          Gdk.Window.set_cursor (win ()) maction_cursor
+        else
         (match hrefs_of_elt elt with
         | Some ((_ :: _) as hrefs) ->
             Gdk.Window.set_cursor (win ()) href_cursor;
@@ -274,22 +296,36 @@ object (self)
     | [] -> assert false (* this method is invoked only if there's a sel. *)
     | node :: _ -> self#tactic_text_pattern_of_node node
 
-  method private popup_contextual_menu time =
+  method private popup_contextual_menu element time =
     let menu = GMenu.menu () in
     let add_menu_item ?(menu = menu) ?stock ?label () =
       GMenu.image_menu_item ?stock ?label ~packing:menu#append () in
     let check = add_menu_item ~label:"Check" () in
     let reductions_menu_item = GMenu.menu_item ~label:"βδιζ-reduce" () in
     let tactics_menu_item = GMenu.menu_item ~label:"Apply tactic" () in
+    let hyperlinks_menu_item = GMenu.menu_item ~label:"Hyperlinks" () in
     menu#append reductions_menu_item;
     menu#append tactics_menu_item;
+    menu#append hyperlinks_menu_item;
     let reductions = GMenu.menu () in
     let tactics = GMenu.menu () in
+    let hyperlinks = GMenu.menu () in
     reductions_menu_item#set_submenu reductions;
     tactics_menu_item#set_submenu tactics;
+    hyperlinks_menu_item#set_submenu hyperlinks;
     let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in
     let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in
     let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in
+    (match element with 
+    | None -> hyperlinks_menu_item#misc#set_sensitive false
+    | Some elt -> 
+        match hrefs_of_elt elt, href_callback with
+        | Some l, Some f ->
+            List.iter 
+              (fun h ->
+                let item = add_menu_item ~menu:hyperlinks ~label:h () in
+                connect_menu_item item (fun () -> f h)) l
+        | _ -> hyperlinks_menu_item#misc#set_sensitive false);
     menu#append (GMenu.separator_item ());
     let copy = add_menu_item ~stock:`COPY () in
     let gui = get_gui () in
@@ -329,9 +365,10 @@ object (self)
           (match self#get_element_at x y with
           | None -> ()
           | Some elt ->
+              if has_maction elt then ignore(self#action_toggle elt) else
               (match hrefs_of_elt elt with
               | Some hrefs -> self#invoke_href_callback hrefs gdk_button
-              | None -> ignore (self#action_toggle elt)))
+              | None -> ()))
     end;
     false
 
@@ -556,6 +593,23 @@ object (self)
     end;
     self#load_root ~root:mathml#get_documentElement
 
+  method nload_sequent:
+   'status. #NCicCoercion.status as 'status -> NCic.metasenv ->
+     NCic.substitution -> int -> unit
+   = fun status metasenv subst metano ->
+    let sequent = List.assoc metano metasenv in
+    let mathml =
+     ApplyTransformation.nmml_of_cic_sequent status metasenv subst
+      (metano,sequent)
+    in
+    if BuildTimeConf.debug then begin
+      let name =
+       "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
+      HLog.debug ("load_sequent: dumping MathML to ./" ^ name);
+      ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
+    end;
+    self#load_root ~root:mathml#get_documentElement
+
   method load_object obj =
     let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *)
     let (mathml,
@@ -579,6 +633,29 @@ object (self)
         end;
         self#load_root ~root:mathml#get_documentElement;
         current_mathml <- Some mathml);
+
+  method load_nobject :
+   'status. #NCicCoercion.status as 'status -> NCic.obj -> unit
+   = fun status obj ->
+    let mathml = ApplyTransformation.nmml_of_cic_object status obj in
+(*
+    self#set_cic_info
+      (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
+    (match current_mathml with
+    | Some current_mathml when use_diff ->
+        self#freeze;
+        XmlDiff.update_dom ~from:current_mathml mathml;
+        self#thaw
+    |  _ ->
+*)
+        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);
+          ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
+        end;
+        self#load_root ~root:mathml#get_documentElement;
+        (*current_mathml <- Some mathml*)(*)*);
 end
 
 let tab_label meta_markup =
@@ -605,7 +682,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     val mutable page2goal = []  (* associative list: page no -> goal no *)
     val mutable goal2page = []  (* the other way round *)
     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
-    val mutable _metasenv = []
+    val mutable _metasenv = `Old []
     val mutable scrolledWin: GBin.scrolled_window option = None
       (* scrolled window to which the sequentViewer is currently attached *)
     val logo = (GMisc.image
@@ -644,13 +721,13 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       page2goal <- [];
       goal2page <- [];
       goal2win <- [];
-      _metasenv <- []; 
+      _metasenv <- `Old []; 
       self#script#setGoal None
 
-    method load_sequents 
-      { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } 
-    =
-      _metasenv <- metasenv;
+    method load_sequents : 'status. #NCicCoercion.status as 'status -> 'a
+     = fun status { proof= (_,metasenv,_subst,_,_, _) as proof; stack = stack } 
+     ->
+      _metasenv <- `Old metasenv;
       pages <- 0;
       let win goal_switch =
         let w =
@@ -725,11 +802,98 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
             try List.assoc page page2goal with Not_found -> assert false
           in
           self#script#setGoal (Some (goal_of_switch goal_switch));
-          self#render_page ~page ~goal_switch))
+          self#render_page status ~page ~goal_switch))
 
-    method private render_page ~page ~goal_switch =
+    method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
+    = fun status ->
+     let _,_,metasenv,subst,_ = status#obj in
+      _metasenv <- `New (metasenv,subst);
+      pages <- 0;
+      let win goal_switch =
+        let w =
+          GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
+            ~shadow_type:`IN ~show:true ()
+        in
+        let reparent () =
+          scrolledWin <- Some w;
+          match cicMathView#misc#parent with
+          | None -> w#add cicMathView#coerce
+          | Some parent ->
+             let parent =
+              match cicMathView#misc#parent with
+                 None -> assert false
+               | Some p -> GContainer.cast_container p
+             in
+              parent#remove cicMathView#coerce;
+              w#add cicMathView#coerce
+        in
+        goal2win <- (goal_switch, reparent) :: goal2win;
+        w#coerce
+      in
+      assert (
+        let stack_goals = Stack.open_goals status#stack in
+        let proof_goals = List.map fst metasenv in
+        if
+          HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
+          <> List.sort Pervasives.compare proof_goals
+        then begin
+          prerr_endline ("STACK GOALS = " ^ String.concat " " (List.map string_of_int stack_goals));
+          prerr_endline ("PROOF GOALS = " ^ String.concat " " (List.map string_of_int proof_goals));
+          false
+        end
+        else true
+      );
+      let render_switch =
+        function Stack.Open i ->`Meta i | Stack.Closed i ->`Closed (`Meta i)
+      in
+      let page = ref 0 in
+      let added_goals = ref [] in
+        (* goals can be duplicated on the tack due to focus, but we should avoid
+         * multiple labels in the user interface *)
+      let add_tab markup goal_switch =
+        let goal = Stack.goal_of_switch goal_switch in
+        if not (List.mem goal !added_goals) then begin
+          ignore(notebook#append_page 
+            ~tab_label:(tab_label markup) (win goal_switch));
+          page2goal <- (!page, goal_switch) :: page2goal;
+          goal2page <- (goal_switch, !page) :: goal2page;
+          incr page;
+          pages <- pages + 1;
+          added_goals := goal :: !added_goals
+        end
+      in
+      let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
+      Stack.iter  (** populate notebook with tabs *)
+        ~env:(fun depth tag (pos, sw) ->
+          let markup =
+            match depth, pos with
+            | 0, 0 -> `Current (render_switch sw)
+            | 0, _ -> `Shift (pos, `Current (render_switch sw))
+            | 1, pos when Stack.head_tag status#stack = `BranchTag ->
+                `Shift (pos, render_switch sw)
+            | _ -> render_switch sw
+          in
+          add_tab markup sw)
+        ~cont:add_switch ~todo:add_switch
+        status#stack;
+      switch_page_callback <-
+        Some (notebook#connect#switch_page ~callback:(fun page ->
+          let goal_switch =
+            try List.assoc page page2goal with Not_found -> assert false
+          in
+          self#script#setGoal (Some (goal_of_switch goal_switch));
+          self#render_page status ~page ~goal_switch))
+
+    method private render_page:
+     'status. #NCicCoercion.status as 'status -> page:int ->
+       goal_switch:Stack.switch -> unit
+     = fun status ~page ~goal_switch ->
       (match goal_switch with
-      | Stack.Open goal -> cicMathView#load_sequent _metasenv goal
+      | Stack.Open goal ->
+         (match _metasenv with
+             `Old menv -> cicMathView#load_sequent menv goal
+           | `New (menv,subst) ->
+               cicMathView#nload_sequent status menv subst goal)
       | Stack.Closed goal ->
           let doc = Lazy.force closed_goal_mathml in
           cicMathView#load_root ~root:doc#get_documentElement);
@@ -738,7 +902,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         List.assoc goal_switch goal2win ()
       with Not_found -> assert false)
 
-    method goto_sequent goal =
+    method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit
+     = fun status goal ->
       let goal_switch, page =
         try
           List.find
@@ -747,7 +912,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         with Not_found -> assert false
       in
       notebook#goto_page page;
-      self#render_page page goal_switch
+      self#render_page status ~page ~goal_switch
 
   end
 
@@ -931,7 +1096,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           handle_error (fun () -> self#loadInput (self#_getSelectedUri ()))));
       mathView#set_href_callback (Some (fun uri ->
         handle_error (fun () ->
-          self#load (`Uri (UriManager.uri_of_string uri)))));
+         let uri =
+          try
+           `Uri (UriManager.uri_of_string uri)
+          with
+           UriManager.IllFormedUri _ ->
+            `NRef (NReference.reference_of_string uri)
+         in
+          self#load uri)));
       gviz#connect_href (fun button_ev attrs ->
         let time = GdkEvent.Button.time button_ev in
         let uri = List.assoc "href" attrs in
@@ -1081,6 +1253,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
               self#dependencies dir uri ()
           | `Uri uri -> self#_loadUriManagerUri uri
+          | `NRef nref -> self#_loadNReference nref
           | `Univs uri -> self#_loadUnivs uri
           | `Whelp (query, results) -> 
               set_whelp_query query;
@@ -1173,16 +1346,25 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private home () =
       self#_showMath;
-      match self#script#grafite_status.proof_status with
+      match self#script#grafite_status#proof_status with
       | Proof  (uri, metasenv, _subst, bo, ty, attrs) ->
-          let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
+         let name = UriManager.name_of_uri (HExtlib.unopt uri) in
+         let obj =
+          Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs)
+         in
           self#_loadObj obj
       | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
-          let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
+         let name = UriManager.name_of_uri (HExtlib.unopt uri) in
+         let obj =
+          Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs)
+         in
           self#_loadObj obj
-      | _ -> self#blank ()
+      | _ ->
+        match self#script#grafite_status#ng_mode with
+           `ProofMode ->
+             self#_loadNObj self#script#grafite_status
+             self#script#grafite_status#obj
+         | _ -> self#blank ()
 
       (** loads a cic uri from the environment
       * @param uri UriManager.uri *)
@@ -1191,6 +1373,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
       self#_loadObj obj
 
+    method private _loadNReference (NReference.Ref (uri,_)) =
+      let obj = NCicEnvironment.get_checked_obj uri in
+      self#_loadNObj self#script#grafite_status obj
+
     method private _loadUnivs uri =
       let uri = UriManager.strip_xpointer uri in
       let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -1231,6 +1417,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showMath;
       mathView#load_object obj
 
+    method private _loadNObj status obj =
+      (* showMath must be done _before_ loading the document, since if the
+       * widget is not mapped (hidden by the notebook) the document is not
+       * rendered *)
+      self#_showMath;
+      mathView#load_nobject status obj
+
     method private _loadTermCic term metasenv =
       let context = self#script#proofContext in
       let dummyno = CicMkImplicit.new_meta metasenv [] in