From: Enrico Tassi Date: Wed, 23 Sep 2009 12:55:05 +0000 (+0000) Subject: more on screenshot X-Git-Tag: make_still_working~3446 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4286d368b6d902a4b54c4cf8590c387f2cdb90ea;p=helm.git more on screenshot --- diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 492aece49..ad0a66294 100644 --- 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 dcddf7b2c..21450e5e7 100644 --- 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 74648f75c..c9135d827 100644 --- 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 d9c9b91e9..68bcf8a62 100644 --- 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 87aca5dcf..50a62bff4 100644 --- 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 ffb7483ec..bbba386e1 100644 --- 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; }