X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=277dbe8f1d0361eafdbebff1a34270bd7ef27799;hb=9e7df95a820cb91d075f1a20d703175da874596c;hp=63cf77a16e356352294078aa27e5651e7213e54c;hpb=45a9e84c12f57e5473eccc6f611cdbb343998d5d;p=helm.git

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 63cf77a16..277dbe8f1 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,19 @@ object (self)
     end;
     self#load_root ~root:mathml#get_documentElement
 
+  method nload_sequent metasenv subst metano =
+    let sequent = List.assoc metano metasenv in
+    let mathml =
+     ApplyTransformation.nmml_of_cic_sequent 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 +629,27 @@ object (self)
         end;
         self#load_root ~root:mathml#get_documentElement;
         current_mathml <- Some mathml);
+
+  method load_nobject obj =
+    let mathml = ApplyTransformation.nmml_of_cic_object 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 +676,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 +715,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;
+      _metasenv <- `Old metasenv;
       pages <- 0;
       let win goal_switch =
         let w =
@@ -727,9 +798,92 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           self#script#setGoal (Some (goal_of_switch goal_switch));
           self#render_page ~page ~goal_switch))
 
+    method nload_sequents 
+      { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack } 
+    =
+      _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 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 stack = `BranchTag ->
+                `Shift (pos, render_switch sw)
+            | _ -> render_switch sw
+          in
+          add_tab markup sw)
+        ~cont:add_switch ~todo:add_switch
+        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 ~page ~goal_switch))
+
     method private render_page ~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 menv subst goal)
       | Stack.Closed goal ->
           let doc = Lazy.force closed_goal_mathml in
           cicMathView#load_root ~root:doc#get_documentElement);
@@ -931,7 +1085,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 +1242,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;
@@ -1102,15 +1264,21 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       Lazy.force load_easter_egg
 
     method private redraw_gviz ?center_on () =
-      let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
-      let fmt = Format.formatter_of_out_channel oc in
-      MetadataDeps.DepGraph.render fmt gviz_graph;
-      close_out oc;
-      gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
-      (match center_on with
-      | None -> ()
-      | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
-      HExtlib.safe_remove tmpfile
+      if Sys.command "which dot" = 0 then
+       let tmpfile, oc = Filename.open_temp_file "matita" ".dot" in
+       let fmt = Format.formatter_of_out_channel oc in
+       MetadataDeps.DepGraph.render fmt gviz_graph;
+       close_out oc;
+       gviz#load_graph_from_file ~gviz_cmd:"tred | dot" tmpfile;
+       (match center_on with
+       | None -> ()
+       | Some uri -> gviz#center_on_href (UriManager.string_of_uri uri));
+       HExtlib.safe_remove tmpfile
+      else
+       MatitaGtkMisc.report_error ~title:"graphviz error"
+        ~message:("Graphviz is not installed but is necessary to render "^
+         "the graph of dependencies amoung objects. Please install it.")
+        ~parent:win#toplevel ()
 
     method private dependencies direction uri () =
       let dbd = LibraryDb.instance () in
@@ -1127,19 +1295,35 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showGviz
 
     method private tex () =
-      let text = String.concat "\n"
-        (List.map (fun (k,vs) -> 
-           let vs = 
-             List.sort (fun a b -> String.length a - String.length b) vs
-           in
-           let vs = 
-             if List.length vs < 4 then vs else 
-             let vs, _ = HExtlib.split_nth 4 vs in vs
-           in
-           k ^ "\t" ^ String.concat ", " vs)
-        (Utf8Macro.pp_table ())) 
-      in
-      self#_loadText text
+      let b = Buffer.create 1000 in
+      Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
+      List.iter 
+        (fun l ->
+           List.iter (fun sym ->
+             Printf.bprintf b "  %s" (Glib.Utf8.from_unichar sym) 
+           ) l;
+           Printf.bprintf b "\n";
+        )
+        (List.sort 
+          (fun l1 l2 -> compare (List.hd l1) (List.hd l2))
+          (Virtuals.get_all_eqclass ()));
+      Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
+      List.iter 
+        (fun tag, items -> 
+           Printf.bprintf b "  %s:\n" tag;
+           List.iter 
+             (fun names, symbol ->
+                Printf.bprintf b "  \t%s\t%s\n" 
+                  (Glib.Utf8.from_unichar symbol)
+                  (String.concat ", " names))
+             (List.sort 
+               (fun (_,a) (_,b) -> compare a b)
+               items);
+           Printf.bprintf b "\n")
+        (List.sort 
+          (fun (a,_) (b,_) -> compare a b)
+          (Virtuals.get_all_virtuals ()));
+      self#_loadText (Buffer.contents b)
 
     method private _loadText text =
       searchText#source_buffer#set_text text;
@@ -1153,14 +1337,23 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showMath;
       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_status with
+           ProofMode tstatus ->
+            let nobj = tstatus.NTacStatus.istatus.NTacStatus.pstatus in
+             self#_loadNObj nobj
+         | _ -> self#blank ()
 
       (** loads a cic uri from the environment
       * @param uri UriManager.uri *)
@@ -1169,6 +1362,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 obj
+
     method private _loadUnivs uri =
       let uri = UriManager.strip_xpointer uri in
       let (_, u) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -1209,6 +1406,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showMath;
       mathView#load_object obj
 
+    method private _loadNObj 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 obj
+
     method private _loadTermCic term metasenv =
       let context = self#script#proofContext in
       let dummyno = CicMkImplicit.new_meta metasenv [] in