severe bug found in parallel zeta

[helm.git] / helm / software / matita / matitaMathView.ml

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index f772a84ed4b85e44eb835013d8270979ecff20fc..5b8540875124cf5841b6facce09037c7864d3cc8 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -959,7 +959,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in
   let metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in
   let whelp_query_RE = Pcre.regexp
-    "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" 
+    "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" 
   in
   let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt in
   let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in
@@ -981,7 +981,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     combo#set_active (aux 0 queries);
   in
   let searchText = 
-    GSourceView.source_view ~auto_indent:false ~editable:false ()
+    GSourceView2.source_view ~auto_indent:false ~editable:false ()
   in
   let _ =
      win#scrolledwinContent#add (searchText :> GObj.widget);
@@ -1035,6 +1035,25 @@ 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_hints () =
+      let module Pp = GraphvizPp.Dot in
+      let filename, oc = Filename.open_temp_file "matita" ".dot" in
+      let fmt = Format.formatter_of_out_channel oc in
+      let status = (MatitaScript.current ())#grafite_status in
+      Pp.header 
+        ~name:"Hints"
+        ~graph_type:"graph"
+        ~graph_attrs:["overlap", "false"]
+        ~node_attrs:["fontsize", "9"; "width", ".4"; 
+            "height", ".4"; "shape", "box"]
+        ~edge_attrs:["fontsize", "10"; "len", "2"] fmt;
+      NCicUnifHint.generate_dot_file status fmt;
+      Pp.trailer fmt;
+      Pp.raw "@." fmt;
+      close_out oc;
+      gviz#load_graph_from_file ~gviz_cmd:"neato -Tpng" filename;
+      (*HExtlib.safe_remove filename*)
+  in
   let load_coerchgraph tred () = 
       let module Pp = GraphvizPp.Dot in
       let filename, oc = Filename.open_temp_file "matita" ".dot" in
@@ -1261,6 +1280,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `About `Us -> self#egg ()
           | `About `CoercionsFull -> self#coerchgraph false ()
           | `About `Coercions -> self#coerchgraph true ()
+          | `About `Hints -> self#hints ()
           | `About `TeX -> self#tex ()
           | `About `Grammar -> self#grammar () 
           | `Check term -> self#_loadCheck term
@@ -1275,7 +1295,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           | `NRef nref -> self#_loadNReference nref
           | `Univs uri -> self#_loadUnivs uri
           | `Whelp (query, results) -> 
-              set_whelp_query query;
               self#_loadList (List.map (fun r -> "obj",
                 UriManager.string_of_uri r) results));
           self#setEntry entry
@@ -1324,6 +1343,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       load_coerchgraph tred ();
       self#_showGviz
 
+    method private hints () =
+      load_hints ();
+      self#_showGviz
+
     method private tex () =
       let b = Buffer.create 1000 in
       Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
@@ -1452,7 +1475,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private _loadTermNCic term m s c =
       let d = 0 in
-      let m = (0,(None,c,term))::m in
+      let m = (0,([],c,term))::m in
       let status = (MatitaScript.current ())#grafite_status in
       mathView#nload_sequent status m s d;
       self#_showMath
@@ -1578,7 +1601,7 @@ let mathViewer () =
 
     method screenshot status sequents metasenv subst (filename as ofn) =
        let w = GWindow.window ~title:"screenshot" () in
-       let width = 600 in
+       let width = 500 in
        let height = 2000 in
        let m = GMathView.math_view 
           ~font_size:!current_font_size ~width ~height
@@ -1588,7 +1611,7 @@ let mathViewer () =
        w#show ();
        let filenames = 
         HExtlib.list_mapi
-         (fun sequent i ->
+         (fun (mno,_ as sequent) i ->
             let mathml = 
               ApplyTransformation.nmml_of_cic_sequent 
                 status metasenv subst sequent
@@ -1601,24 +1624,39 @@ let mathViewer () =
               filename ^ "-raw" ^ string_of_int i ^ ".png" 
             in
             GdkPixbuf.save ~filename ~typ:"png" pixbuf;
-            filename)
+            filename,mno)
          sequents
        in
        let items = 
-         List.map (fun x -> 
-           Printf.sprintf 
-             " '(' -trim -border 3 -bordercolor white %s ')' "
-             (Filename.quote x))
+         List.map (fun (x,mno) -> 
+           ignore(Sys.command
+             (Printf.sprintf
+              ("convert "^^
+              " '(' -gravity west -bordercolor grey -border 1 label:%d ')' "^^
+              " '(' -trim -bordercolor white -border 5 "^^
+                " -bordercolor grey -border 1 %s ')' -append %s ")
+              mno
+              (Filename.quote x)
+              (Filename.quote (x ^ ".label.png"))));
+             x ^ ".label.png")
          filenames
        in
+       let rec div2 = function 
+         | [] -> []
+         | [x] -> [[x]]
+         | x::y::tl -> [x;y] :: div2 tl
+       in
+       let items = div2 items in
        ignore(Sys.command (Printf.sprintf 
-         "convert %s +append  %s" 
-         (String.concat (" '(' -gravity center -size 9x150 xc: "^
-         "-draw \"line 5,0 5,48\" "^
-         "-draw \"line 5,52 5,98\" " ^
-         "-draw \"line 5,102 5,150\" " ^ " ')'") items)
+         "convert %s -append  %s" 
+          (String.concat ""
+            (List.map (fun items ->
+              Printf.sprintf " '(' %s +append ')' "
+                (String.concat 
+                   (" '(' -gravity center -size 10x10 xc: ')' ") items)) items))
          (Filename.quote (ofn ^ ".png")))); 
-       List.iter Sys.remove filenames;
+       List.iter (fun x,_ -> Sys.remove x) filenames;
+       List.iter Sys.remove (List.flatten items);
        w#destroy ();
   end