multi screenshot

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index ad0a66294db314ff2ac47be9c59e45b2ee9df6ea..f772a84ed4b85e44eb835013d8270979ecff20fc 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -1576,10 +1576,7 @@ let mathViewer () =
     method show_uri_list ?(reuse=false) ~entry l =
       (self#get_browser reuse)#load entry
 
-    method screenshot status sequent metasenv subst (filename as ofn) =
-       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 = 600 in
        let height = 2000 in
@@ -1589,16 +1586,39 @@ let mathViewer () =
           ~show:true ()
        in
        w#show ();
-       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.png" in
-       GdkPixbuf.save ~filename ~typ:"png" pixbuf;
+       let filenames = 
+        HExtlib.list_mapi
+         (fun 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)
+         sequents
+       in
+       let items = 
+         List.map (fun x -> 
+           Printf.sprintf 
+             " '(' -trim -border 3 -bordercolor white %s ')' "
+             (Filename.quote x))
+         filenames
+       in
        ignore(Sys.command (Printf.sprintf 
-         "convert -trim -border 3 -bordercolor white %s %s" 
-         (Filename.quote filename) 
+         "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)
          (Filename.quote (ofn ^ ".png")))); 
+       List.iter Sys.remove filenames;
        w#destroy ();
   end
 

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index e191ee7b31d6c09a01795c2b824297c0dfb534e3..d4ef4c6e019cdf7d51a6b0ae8c2b59be02b117e9 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -371,9 +371,8 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
   | TA.Screenshot (_,name) -> 
        let status = script#grafite_status in
        let _,_,menv,subst,_ = status#obj in
-       let sequent = List.hd menv in
        let name = Filename.dirname (script#filename) ^ "/" ^ name in
-       guistuff.mathviewer#screenshot status sequent menv subst name;
+       guistuff.mathviewer#screenshot status menv menv subst name;
        [status, parsed_text], "", parsed_text_length
   | TA.NCheck (_,t) ->
       let status = script#grafite_status in

diff --git a/helm/software/matita/matitaTypes.ml b/helm/software/matita/matitaTypes.ml
index 61f4bc306407ca6ac6facfefc117128912864da1..7468bedfadfaafe84ef7edb1bdb0cec7ae973f85 100644 (file)
--- a/helm/software/matita/matitaTypes.ml
+++ b/helm/software/matita/matitaTypes.ml
@@ -103,6 +103,6 @@ class type mathViewer =
     method show_uri_list:
       ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
     method screenshot: 
-      GrafiteTypes.status -> int * NCic.conjecture -> NCic.metasenv ->
+      GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv ->
         NCic.substitution -> string -> unit
   end

diff --git a/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli
index f220a848a7d0dfbcfbdea9a03f91f16f441e330a..a1e2fa9aab2844c06e54e084681413d5a7e05327 100644 (file)
--- a/helm/software/matita/matitaTypes.mli
+++ b/helm/software/matita/matitaTypes.mli
@@ -51,6 +51,6 @@ class type mathViewer =
     method show_uri_list :
       ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit
     method screenshot: 
-      GrafiteTypes.status -> int * NCic.conjecture -> NCic.metasenv ->
+      GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv ->
         NCic.substitution -> string -> unit
   end