X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaMathView.ml;h=c32c00f203c12c4fa99dad0730cdd3b79335bae0;hb=c55226c2a9536b1483f578192bc79d317f7b1971;hp=4b54f60ac1e7f36bdd355147166e9790f53476fa;hpb=2066e0e9fcd678b61fcf7911ea3976344d5a85ab;p=helm.git

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index 4b54f60ac..c32c00f20 100644
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -648,7 +648,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       _metasenv <- []; 
       self#script#setGoal None
 
-    method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
+    method load_sequents { proof = (_,metasenv,_,_, _) as proof; stack = stack } =
       _metasenv <- metasenv;
       pages <- 0;
       let win goal_switch =
@@ -844,12 +844,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let load_easter_egg = lazy (
     win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
   in
-  let load_coerchgraph () = 
+  let load_coerchgraph tred () = 
       let str = CoercGraph.generate_dot_file () in
       let filename, oc = Filename.open_temp_file "matita" ".dot" in
       output_string oc str;
       close_out oc;
-      gviz#load_graph_from_file filename;
+      if tred then
+        gviz#load_graph_from_file ~gviz_cmd:"tred|dot" filename
+      else
+        gviz#load_graph_from_file filename;
       HExtlib.safe_remove filename
   in
   object (self)
@@ -925,6 +928,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         match self#currentCicUri with
         | Some uri -> self#load (`Metadata (`Deps (`Back, uri)))
         | None -> ());
+      connect_menu_item win#hBugsTutorsMenuItem (fun () ->
+        self#load (`HBugs `Tutors));
+      connect_menu_item win#browserUrlMenuItem (fun () ->
+        win#browserUri#entry#misc#grab_focus ());
 
       (* fill dep graph contextual menu *)
       let go_menu_item =
@@ -1000,9 +1007,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
      * 
      * Use only these functions to switch between the tabs
      *)
-    method private _showMath = win#mathOrListNotebook#goto_page 0
-    method private _showList = win#mathOrListNotebook#goto_page 1
-    method private _showGviz = win#mathOrListNotebook#goto_page 3
+    method private _showMath = win#mathOrListNotebook#goto_page  0
+    method private _showList = win#mathOrListNotebook#goto_page  1
+    method private _showGviz = win#mathOrListNotebook#goto_page  3
+    method private _showHBugs = win#mathOrListNotebook#goto_page 4
 
     method private back () =
       try
@@ -1019,17 +1027,19 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _load ?(force=false) entry =
       handle_error (fun () ->
        if entry <> current_entry || entry = `About `Current_proof || entry =
-         `About `Coercions || force then
+         `About `Coercions || entry = `About `CoercionsFull || force then
         begin
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
           | `About `Us -> self#egg ()
-          | `About `Coercions -> self#coerchgraph ()
+          | `About `CoercionsFull -> self#coerchgraph false ()
+          | `About `Coercions -> self#coerchgraph true ()
           | `Check term -> self#_loadCheck term
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
           | `Development d -> self#_showDevelDeps d
           | `Dir dir -> self#_loadDir dir
+          | `HBugs `Tutors -> self#_loadHBugsTutors
           | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
               self#dependencies dir uri ()
           | `Uri uri -> self#_loadUriManagerUri uri
@@ -1073,20 +1083,20 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#redraw_gviz ~center_on:uri ();
       self#_showGviz
 
-    method private coerchgraph () =
-      load_coerchgraph ();
+    method private coerchgraph tred () =
+      load_coerchgraph tred ();
       self#_showGviz
 
     method private home () =
       self#_showMath;
       match self#script#grafite_status.proof_status with
-      | Proof  (uri, metasenv, bo, ty) ->
+      | Proof  (uri, metasenv, bo, ty, attrs) ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
-      | Incomplete_proof { proof = (uri, metasenv, bo, ty) } ->
+      | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } ->
           let name = UriManager.name_of_uri (HExtlib.unopt uri) in
-          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in
+          let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
           self#_loadObj obj
       | _ -> self#blank ()
 
@@ -1111,6 +1121,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       lastDir <- dir;
       self#_loadList l
 
+    method private _loadHBugsTutors =
+      self#_showHBugs
+
     method private setEntry entry =
       win#browserUri#entry#set_text (MatitaTypes.string_of_entry entry);
       current_entry <- entry
@@ -1176,6 +1189,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
               `Uri (UriManager.uri_of_string ((*fix_uri*) txt))
           | txt when is_dir txt -> `Dir (MatitaMisc.normalize_dir txt)
           | txt when is_metadata txt -> `Metadata (parse_metadata txt)
+          | "hbugs:/tutors/" -> `HBugs `Tutors
           | txt ->
              (try
                MatitaTypes.entry_of_string txt