Some clean-up here and there in dama (coercions removed, implicits added, etc.)

[helm.git] / matita / matitaMathView.ml

diff --git a/matita/matitaMathView.ml b/matita/matitaMathView.ml
index c235a9f4354402669ac495ea0f500f2064945504..5ae8baab6ea2f6ee0943bdf723d275be0d3e8c4c 100644 (file)
--- a/matita/matitaMathView.ml
+++ b/matita/matitaMathView.ml
@@ -550,7 +550,8 @@ object (self)
         ids_to_terms, ids_to_hypotheses, ids_to_father_ids,
         Hashtbl.create 1, None));
     if BuildTimeConf.debug then begin
-      let name = "sequent_viewer.xml" in
+      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;
@@ -572,7 +573,8 @@ object (self)
         self#thaw
     |  _ ->
         if BuildTimeConf.debug then begin
-          let name = "cic_browser.xml" in
+          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;
@@ -797,7 +799,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in
   let gui = get_gui () in
   let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in
-  let gviz = LablGraphviz.gDot ~packing:win#graphScrolledWin#add () in
+  let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in
   let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
   let combo,_ = GEdit.combo_box_text ~strings:queries () in
   let activate_combo_query input q =
@@ -923,6 +925,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 =
@@ -998,8 +1004,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 _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
@@ -1025,7 +1033,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `About `Coercions -> self#coerchgraph ()
           | `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
@@ -1053,7 +1063,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let fmt = Format.formatter_of_out_channel oc in
       MetadataDeps.DepGraph.render fmt gviz_graph;
       close_out oc;
-      gviz#load_graph_from_file tmpfile;
+      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));
@@ -1067,11 +1077,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         | `Back -> MetadataDeps.DepGraph.inverse_deps ~dbd uri in
       gviz_graph <- graph;  (** XXX check this for memory consuption *)
       self#redraw_gviz ~center_on:uri ();
-      win#mathOrListNotebook#goto_page 3
+      self#_showGviz
 
     method private coerchgraph () =
       load_coerchgraph ();
-      win#mathOrListNotebook#goto_page 3
+      self#_showGviz
 
     method private home () =
       self#_showMath;
@@ -1107,10 +1117,23 @@ 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
 
+    method private _showDevelDeps d =
+      match MatitamakeLib.development_for_name d with
+      | None -> ()
+      | Some devel ->
+          (match MatitamakeLib.dot_for_development devel with
+          | None -> ()
+          | Some fname ->
+              gviz#load_graph_from_file ~gviz_cmd:"tred | dot" fname;
+              self#_showGviz)
+
     method private _loadObj obj =
       (* showMath must be done _before_ loading the document, since if the
        * widget is not mapped (hidden by the notebook) the document is not
@@ -1162,6 +1185,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