more on screenshot

diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml
index 492aece49cf3b3a322fdad5065ef7909f45ab615..ad0a66294db314ff2ac47be9c59e45b2ee9df6ea 100644 (file)
--- a/helm/software/matita/matitaMathView.ml
+++ b/helm/software/matita/matitaMathView.ml
@@ -1576,23 +1576,29 @@ let mathViewer () =
     method show_uri_list ?(reuse=false) ~entry l =
       (self#get_browser reuse)#load entry
 
-    method screenshot status sequent metasenv subst filename =
+    method screenshot status sequent metasenv subst (filename as ofn) =
        let mathml = 
          ApplyTransformation.nmml_of_cic_sequent status metasenv subst sequent
        in
        let w = GWindow.window ~title:"screenshot" () in
+       let width = 600 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
+       let pixbuf = GdkPixbuf.create ~width ~height () in
        GdkPixbuf.get_from_drawable ~dest:pixbuf pixmap;
-       let filename = filename ^ ".png" in
+       let filename = filename ^ "-raw.png" in
        GdkPixbuf.save ~filename ~typ:"png" pixbuf;
+       ignore(Sys.command (Printf.sprintf 
+         "convert -trim -border 3 -bordercolor white %s %s" 
+         (Filename.quote filename) 
+         (Filename.quote (ofn ^ ".png")))); 
        w#destroy ();
   end
 

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index dcddf7b2cc93cad40ef7f9bc63fef764ba2c9aff..21450e5e796e7d74c8f7549e156f079799e80646 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -372,6 +372,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
        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;
        [status, parsed_text], "", parsed_text_length
   | TA.NCheck (_,t) ->

diff --git a/helm/software/matita/nlibrary/topology/Makefile b/helm/software/matita/nlibrary/topology/Makefile
index 74648f75c0a3f01f83a1ab2ddc1ac49abdbf87c3..c9135d827634f21145e753741069fd2d358e6370 100644 (file)
--- a/helm/software/matita/nlibrary/topology/Makefile
+++ b/helm/software/matita/nlibrary/topology/Makefile
@@ -1,12 +1,13 @@
+SRC=$(wildcard *.ma)
 
-all:
-       for X in *.ma; do $(MAKE) $$X.html; done
+all: $(SRC:%.ma=%.html)
 
 clean:
        rm *.html *.png
 
-%.ma.html: %.ma convert.awk preamble.xml postamble.xml
+%.html: %.ma convert.awk preamble.xml postamble.xml
        cat preamble.xml > $@
-       awk -f convert.awk < $< | markdown >> $@
+       awk -f convert.awk < $< > $*.mdwn
+       markdown < $*.mdwn >> $@
        cat postamble.xml >> $@
 

diff --git a/helm/software/matita/nlibrary/topology/convert.awk b/helm/software/matita/nlibrary/topology/convert.awk
index d9c9b91e9cbac1117b8cce05e8ebd139d5dfc000..68bcf8a6260599bc629c02f7081213fbe93635ec 100644 (file)
--- a/helm/software/matita/nlibrary/topology/convert.awk
+++ b/helm/software/matita/nlibrary/topology/convert.awk
@@ -1,6 +1,31 @@
-BEGIN { p = 1; indent = ""; } 
-/DOCBEGIN/ { indent = ""; NF = 0; }
-/DOCEND/ { indent = "    "; NF = 0; } 
-/HIDE/ { p = 0; }
-{ if (p == 1) print indent $0; } 
-/UNHIDE/ { p = 1; }
+BEGIN { 
+       do_print = 1; 
+       indent = ""; 
+       refs["matita"] = "http://matita.cs.unibo.it";
+       } 
+
+# markdown mangling
+/screenshot *".*"/ { 
+       match($0, "screenshot *\"([^\"]+)\"", data);
+       key = data[1];
+       refs[key] = key ".png"; 
+       }
+
+# literate programming
+/DOCBEGIN/ { 
+       indent = ""; NF = 0; }
+/DOCEND/ { 
+       indent = "    "; NF = 0; } 
+/HIDE/ { 
+       do_print = 0; }
+{ 
+       if (do_print == 1) print indent $0; } 
+/UNHIDE/ { 
+       do_print = 1; }
+
+# closing
+END { 
+       for (i in refs) {
+               print "[" i "]: " refs[i];      
+       }
+} 

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 87aca5dcfacfb0a299c7a9debff86ca36aa18735..50a62bff4ec049e749c5429ef2b16707bb44ddfd 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -11,7 +11,7 @@ Initial setup
 The library, inclusion of `sets/sets.ma`, notation defined: Ω^A.
 Symbols (see menu: View ▹ TeX/UTF-8 Table):
 
-- `Ω` \Omega 
+- `Ω` can be typed \Omega 
 - `∀` \Forall
 - `λ` \lambda
 - `≝` \def
@@ -63,6 +63,8 @@ interpretation "C" 'C a i = (C ? a i).
 The first definition
 --------------------
 
+![bla bla][def-fish-rec]
+
 DOCEND*)
 
 ndefinition cover_set ≝ λc:∀A:Ax.Ω^A → A → CProp[0].λA,C,U.
@@ -105,7 +107,7 @@ nlet corec fish_rec (A:Ax) (U: Ω^A)
  (P: Ω^A) (H1: P ⊆ U)
   (H2: ∀a:A. a ∈ P → ∀j: 𝐈 a. 𝐂 a j ≬ P):
    ∀a:A. ∀p: a ∈ P. a ⋉ U ≝ ?.
-#a; #p; napply cfish; (** screenshot "topology/def-fish-rec". *)
+#a; #p; napply cfish; (** screenshot "def-fish-rec". *)
 ##[ napply H1; napply p;
 ##| #i; ncases (H2 a p i); #x; *; #xC; #xP; @; ##[napply x]
     @; ##[ napply xC ] napply (fish_rec ? U P); nassumption;

diff --git a/helm/software/matita/nlibrary/topology/preamble.xml b/helm/software/matita/nlibrary/topology/preamble.xml
index ffb7483ec3b73ea14a78ec9c535686c241dbbc77..bbba386e1034260d79ac403e174b9db59069ba3f 100644 (file)
--- a/helm/software/matita/nlibrary/topology/preamble.xml
+++ b/helm/software/matita/nlibrary/topology/preamble.xml
@@ -6,20 +6,15 @@
          pre, code { 
            font-family: Sans; 
            font-size: 1em; 
-           background-color:#efee79; } 
-         pre { margin-right: 5em;}
-         img { display: block; margin-bottom: 1em; }
-         .img { 
+           background-color:#fafaaf; } 
+         pre { margin-right: 5em; margin-left: 2em; }
+         img { 
            margin-left: auto; 
            margin-right: auto; 
            display: block;
            border-style: solid;
            border-width: 2px;
            border-color: grey;
-           background: grey;
-           text-align:center;
-           color: white;
-           width: 200px;
          }
   </style>
  </head>