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

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 255998c4f..71e7cb553 100644
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -944,6 +944,7 @@ let current_proof_uri = BuildTimeConf.current_proof_uri
 type term_source =
   [ `Ast of CicNotationPt.term
   | `Cic of Cic.term * Cic.metasenv
+  | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution
   | `String of string
   ]
 
@@ -980,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);
@@ -1034,15 +1035,50 @@ 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 str = CoercGraph.generate_dot_file () in
+      let module Pp = GraphvizPp.Dot in
       let filename, oc = Filename.open_temp_file "matita" ".dot" in
-      output_string oc str;
+      let fmt = Format.formatter_of_out_channel oc in
+      Pp.header 
+        ~name:"Coercions"
+        ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+        ~edge_attrs:["fontsize", "10"] fmt;
+      let status = (MatitaScript.current ())#grafite_status in
+      NCicCoercion.generate_dot_file status fmt;
+      Pp.trailer fmt;
+      Pp.header 
+        ~name:"OLDCoercions"
+        ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
+        ~edge_attrs:["fontsize", "10"] fmt;
+      CoercGraph.generate_dot_file fmt;
+      Pp.trailer fmt;
+      Pp.raw "@." fmt;
       close_out oc;
       if tred then
-        gviz#load_graph_from_file ~gviz_cmd:"tred|dot" filename
+        gviz#load_graph_from_file 
+          ~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename
       else
-        gviz#load_graph_from_file filename;
+        gviz#load_graph_from_file 
+          ~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename;
       HExtlib.safe_remove filename
   in
   object (self)
@@ -1244,10 +1280,13 @@ 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
           | `Cic (term, metasenv) -> self#_loadTermCic term metasenv
+          | `NCic (term, ctx, metasenv, subst) -> 
+               self#_loadTermNCic term metasenv subst ctx
           | `Dir dir -> self#_loadDir dir
           | `HBugs `Tutors -> self#_loadHBugsTutors
           | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) ->
@@ -1305,6 +1344,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";
@@ -1431,6 +1474,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       mathView#load_sequent (sequent :: metasenv) dummyno;
       self#_showMath
 
+    method private _loadTermNCic term m s c =
+      let d = 0 in
+      let m = (0,([],c,term))::m in
+      let status = (MatitaScript.current ())#grafite_status in
+      mathView#nload_sequent status m s d;
+      self#_showMath
+
     method private _loadList l =
       model#list_store#clear ();
       List.iter (fun (tag, s) -> model#easy_append ~tag s) l;
@@ -1549,6 +1599,66 @@ let mathViewer () =
       
     method show_uri_list ?(reuse=false) ~entry l =
       (self#get_browser reuse)#load entry
+
+    method screenshot status sequents metasenv subst (filename as ofn) =
+       let w = GWindow.window ~title:"screenshot" () in
+       let width = 500 in
+       let height = 2000 in
+       let m = GMathView.math_view 
+          ~font_size:!current_font_size ~width ~height
+          ~packing:w#add
+          ~show:true ()
+       in
+       w#show ();
+       let filenames = 
+        HExtlib.list_mapi
+         (fun (mno,_ as sequent) i ->
+            let mathml = 
+              ApplyTransformation.nmml_of_cic_sequent 
+                status metasenv subst sequent
+            in
+            m#load_root ~root:mathml#get_documentElement;
+            let pixmap = m#get_buffer in
+            let pixbuf = GdkPixbuf.create ~width ~height () in
+            GdkPixbuf.get_from_drawable ~dest:pixbuf pixmap;
+            let filename = 
+              filename ^ "-raw" ^ string_of_int i ^ ".png" 
+            in
+            GdkPixbuf.save ~filename ~typ:"png" pixbuf;
+            filename,mno)
+         sequents
+       in
+       let items = 
+         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 ""
+            (List.map (fun items ->
+              Printf.sprintf " '(' %s +append ')' "
+                (String.concat 
+                   (" '(' -gravity center -size 10x10 xc: ')' ") items)) items))
+         (Filename.quote (ofn ^ ".png")))); 
+       List.iter (fun x,_ -> Sys.remove x) filenames;
+       List.iter Sys.remove (List.flatten items);
+       w#destroy ();
   end
 
 let refresh_all_browsers () =