Type printed as such, CProp printed as such

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

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 492aece49cf3b3a322fdad5065ef7909f45ab615..c666a34f7d7fe5f06efe5827e3660a5900e7bfc2 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -1576,23 +1576,54 @@ let mathViewer () =
     method show_uri_list ?(reuse=false) ~entry l =
       (self#get_browser reuse)#load entry
 
-    method screenshot status sequent metasenv subst filename =
-       let mathml = 
-         ApplyTransformation.nmml_of_cic_sequent status metasenv subst sequent
-       in
+    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:500 ~height:400 
+          ~font_size:!current_font_size ~width ~height
           ~packing:w#add
           ~show:true ()
        in
        w#show ();
-       m#load_root ~root:mathml#get_documentElement;
-       let pixmap = m#get_buffer in
-       let pixbuf = GdkPixbuf.create ~width:500 ~height:400 () in
-       GdkPixbuf.get_from_drawable ~dest:pixbuf pixmap;
-       let filename = filename ^ ".png" in
-       GdkPixbuf.save ~filename ~typ:"png" pixbuf;
+       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
+       ignore(Sys.command (Printf.sprintf 
+         "convert %s +append  %s" 
+         (String.concat (" '(' -gravity center -size 10x10 xc: ')' ") items)
+         (Filename.quote (ofn ^ ".png")))); 
+       List.iter (fun x,_ -> Sys.remove x) filenames;
+       List.iter Sys.remove items;
        w#destroy ();
   end