From: Enrico Tassi Date: Wed, 23 Sep 2009 11:30:42 +0000 (+0000) Subject: new macro screenshot X-Git-Tag: make_still_working~3447 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bee436af0c6ceb1c83259c94036df8b12f901f2d;p=helm.git new macro screenshot --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 68350ac75..8fc37e4c5 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -193,10 +193,11 @@ type ('term,'lazy_term) macro = type nmacro = | NCheck of loc * CicNotationPt.term + | Screenshot of loc * string (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 27 +let magic = 28 type ('term,'obj) command = | Index of loc * 'term option (* key *) * UriManager.uri (* value *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 3d6b86492..76651753f 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -303,6 +303,7 @@ let pp_arg ~term_pp arg = let pp_nmacro = function | NCheck (_, term) -> Printf.sprintf "ncheck %s" (CicNotationPp.pp_term term) + | Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name ;; let pp_macro ~term_pp ~lazy_term_pp = diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index bf34fc283..52f151fc2 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -660,6 +660,7 @@ EXTEND nmacro: [ [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t) + | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname) ] ]; diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend index 28178ecfa..c9a27fc56 100644 --- a/helm/software/matita/.depend +++ b/helm/software/matita/.depend @@ -1,5 +1,7 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi +buildTimeConf.cmo: +buildTimeConf.cmx: dump_moo.cmo: buildTimeConf.cmo dump_moo.cmx: buildTimeConf.cmx lablGraphviz.cmo: lablGraphviz.cmi @@ -20,10 +22,12 @@ matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaWiki.cmx \ matitaMisc.cmx matitaInit.cmx matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi -matitaEngine.cmo: matitaEngine.cmi -matitaEngine.cmx: matitaEngine.cmi +matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi +matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi +matitaGeneratedGui.cmo: +matitaGeneratedGui.cmx: matitaGtkMisc.cmo: matitaTypes.cmi matitaGeneratedGui.cmo buildTimeConf.cmo \ matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \ @@ -52,10 +56,10 @@ matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ buildTimeConf.cmx applyTransformation.cmx -matitaScript.cmo: virtuals.cmi matitacLib.cmi matitaTypes.cmi matitaMisc.cmi \ +matitaScript.cmo: virtuals.cmi matitacLib.cmi matitaTypes.cmi \ matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo \ applyTransformation.cmi matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitacLib.cmx matitaTypes.cmx matitaMisc.cmx \ +matitaScript.cmx: virtuals.cmx matitacLib.cmx matitaTypes.cmx \ matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \ applyTransformation.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi @@ -68,8 +72,21 @@ predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi virtuals.cmo: virtuals.cmi virtuals.cmx: virtuals.cmi +applyTransformation.cmi: +lablGraphviz.cmi: +matitaAutoGui.cmi: +matitaclean.cmi: +matitacLib.cmi: +matitadep.cmi: +matitaEngine.cmi: +matitaExcPp.cmi: matitaGtkMisc.cmi: matitaGeneratedGui.cmo matitaGui.cmi: matitaGuiTypes.cmi matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo +matitaInit.cmi: matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi +matitaMisc.cmi: matitaScript.cmi: matitaTypes.cmi +matitaTypes.cmi: +predefined_virtuals.cmi: +virtuals.cmi: diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index d8d81bf37..bbe22f7d1 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -37,9 +37,9 @@ MLI = \ lablGraphviz.mli \ matitaTypes.mli \ matitaMisc.mli \ + applyTransformation.mli \ matitaEngine.mli \ matitaExcPp.mli \ - applyTransformation.mli \ matitacLib.mli \ matitaInit.mli \ matitaGtkMisc.mli \ @@ -53,9 +53,9 @@ MLI = \ CMLI = \ matitaTypes.mli \ matitaMisc.mli \ + applyTransformation.mli \ matitaEngine.mli \ matitaExcPp.mli \ - applyTransformation.mli \ matitacLib.mli \ matitaInit.mli \ matitaWiki.mli \ diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index 4e1024d5f..0d0703905 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -5,7 +5,7 @@ \(\*\*[^\)] - [^\(]\*\*\) + [^\(]\*\) diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml index a2effbe03..c13004c24 100644 --- a/helm/software/matita/matitaEngine.ml +++ b/helm/software/matita/matitaEngine.ml @@ -58,6 +58,25 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context = in GrafiteTypes.set_metasenv metasenv grafite_status,macro +let eval_macro_screenshot (status : GrafiteTypes.status) name = + let _,_,metasenv,subst,_ = status#obj in + let sequent = List.hd metasenv in + let mathml = + ApplyTransformation.nmml_of_cic_sequent + status metasenv subst sequent + in + let domImpl = Gdome.domImplementation () in + ignore(domImpl#saveDocumentToFile + ~name:(name^".xml") ~doc:mathml ()); + ignore(Sys.command ("mathmlsvg --verbose=1 --font-size=20 --cut-filename=no " ^ + Filename.quote (name^".xml"))); + ignore(Sys.command ("convert " ^ + Filename.quote (name^".svg") ^ " " ^ + Filename.quote (name^".png"))); + HLog.debug ("generated " ^ name ^ ".png"); + status, `New [] +;; + let eval_ast ?do_heavy_checks status (text,prefix_len,ast) = let dump = not (Helm_registry.get_bool "matita.moo") in let lexicon_status_ref = ref (status :> LexiconEngine.status) in diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 5f3f413bf..492aece49 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -1575,6 +1575,25 @@ 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 + let w = GWindow.window ~title:"screenshot" () in + let m = GMathView.math_view + ~font_size:!current_font_size ~width:500 ~height:400 + ~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; + w#destroy (); end let refresh_all_browsers () = diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 9874e7184..dcddf7b2c 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -368,6 +368,12 @@ let cic2grafite context menv t = let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac = let parsed_text_length = String.length parsed_text in match mac with + | TA.Screenshot (_,name) -> + let status = script#grafite_status in + let _,_,menv,subst,_ = status#obj in + let sequent = List.hd menv in + guistuff.mathviewer#screenshot status sequent menv subst name; + [status, parsed_text], "", parsed_text_length | TA.NCheck (_,t) -> let status = script#grafite_status in let ctx = [] in @@ -641,6 +647,15 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff let parsed_text, _, _, parsed_text_length = text_of_loc loc in [grafite_status,parsed_text],"", parsed_text_length + | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> + let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + eval_executable include_paths buffer guistuff + grafite_status user_goal unparsed_text skipped nonskipped script ex loc + | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex))) + (*when Helm_registry.get_bool "matita.literate" *) -> + let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in + eval_executable include_paths buffer guistuff + grafite_status user_goal unparsed_text skipped nonskipped script ex loc | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in let remain_len = String.length unparsed_text - parsed_text_length in @@ -663,12 +678,6 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff | (statuses,text)::tl -> (statuses,parsed_text ^ text)::tl,"",parsed_text_length + len | [] -> [], "", 0) - | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> - let _, nonskipped, skipped, parsed_text_length = - text_of_loc loc - in - eval_executable include_paths buffer guistuff - grafite_status user_goal unparsed_text skipped nonskipped script ex loc let fresh_script_id = let i = ref 0 in diff --git a/helm/software/matita/matitaTypes.ml b/helm/software/matita/matitaTypes.ml index 4f2d414ee..61f4bc306 100644 --- a/helm/software/matita/matitaTypes.ml +++ b/helm/software/matita/matitaTypes.ml @@ -102,4 +102,7 @@ class type mathViewer = method show_entry: ?reuse:bool -> mathViewer_entry -> unit method show_uri_list: ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit + method screenshot: + GrafiteTypes.status -> int * NCic.conjecture -> NCic.metasenv -> + NCic.substitution -> string -> unit end diff --git a/helm/software/matita/matitaTypes.mli b/helm/software/matita/matitaTypes.mli index ecc78a629..f220a848a 100644 --- a/helm/software/matita/matitaTypes.mli +++ b/helm/software/matita/matitaTypes.mli @@ -50,4 +50,7 @@ class type mathViewer = method show_entry : ?reuse:bool -> mathViewer_entry -> unit method show_uri_list : ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit + method screenshot: + GrafiteTypes.status -> int * NCic.conjecture -> NCic.metasenv -> + NCic.substitution -> string -> unit end diff --git a/helm/software/matita/nlibrary/topology/Makefile b/helm/software/matita/nlibrary/topology/Makefile new file mode 100644 index 000000000..74648f75c --- /dev/null +++ b/helm/software/matita/nlibrary/topology/Makefile @@ -0,0 +1,12 @@ + +all: + for X in *.ma; do $(MAKE) $$X.html; done + +clean: + rm *.html *.png + +%.ma.html: %.ma convert.awk preamble.xml postamble.xml + cat preamble.xml > $@ + awk -f convert.awk < $< | markdown >> $@ + cat postamble.xml >> $@ + diff --git a/helm/software/matita/nlibrary/topology/convert.awk b/helm/software/matita/nlibrary/topology/convert.awk new file mode 100644 index 000000000..d9c9b91e9 --- /dev/null +++ b/helm/software/matita/nlibrary/topology/convert.awk @@ -0,0 +1,6 @@ +BEGIN { p = 1; indent = ""; } +/DOCBEGIN/ { indent = ""; NF = 0; } +/DOCEND/ { indent = " "; NF = 0; } +/HIDE/ { p = 0; } +{ if (p == 1) print indent $0; } +/UNHIDE/ { p = 1; } diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 7f4f5e359..87aca5dcf 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -1,13 +1,56 @@ +(*DOCBEGIN + +Matita Tutorial: inductively generated formal topologies +======================================================== + +Small intro... + +Initial setup +------------- + +The library, inclusion of `sets/sets.ma`, notation defined: Ω^A. +Symbols (see menu: View ▹ TeX/UTF-8 Table): + +- `Ω` \Omega +- `∀` \Forall +- `λ` \lambda +- `≝` \def +- `→` -> + +Virtuals, ALT-L, for example I changes into 𝕀, finally 𝐈. + +DOCEND*) + include "sets/sets.ma". +(*DOCBEGIN + +Axiom set +--------- + +records, ... + +DOCEND*) + nrecord Ax : Type[1] ≝ { - S:> setoid; (* Type[0]; *) + S:> setoid; I: S → Type[0]; C: ∀a:S. I a → Ω ^ S }. +(*HIDE*) notation "𝐈 \sub( ❨a❩ )" non associative with precedence 70 for @{ 'I $a }. notation "𝐂 \sub ( ❨a,\emsp i❩ )" non associative with precedence 70 for @{ 'C $a $i }. +(*UNHIDE*) + +(*DOCBEGIN + +Notation for the axiom set +-------------------------- + +bla bla + +DOCEND*) notation > "𝐈 term 90 a" non associative with precedence 70 for @{ 'I $a }. notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ 'C $a $i }. @@ -15,6 +58,13 @@ notation > "𝐂 term 90 a term 90 i" non associative with precedence 70 for @{ interpretation "I" 'I a = (I ? a). interpretation "C" 'C a i = (C ? a i). +(*DOCBEGIN + +The first definition +-------------------- + +DOCEND*) + ndefinition cover_set ≝ λc:∀A:Ax.Ω^A → A → CProp[0].λA,C,U. ∀y.y ∈ C → c A U y. @@ -55,7 +105,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; +#a; #p; napply cfish; (** screenshot "topology/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; @@ -207,12 +257,25 @@ naxiom AC : ∀A,a,i,U.(∀j:𝐃 a i.∃x:Ord A.𝐝 a i j ∈ U⎽x) → (Σf. naxiom setoidification : ∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U. +(*DOCBEGIN + +Bla Bla, + +
foo
+ +DOCEND*) + +alias symbol "covers" = "new covers". +alias symbol "covers" = "new covers set". +alias symbol "covers" = "new covers". +alias symbol "covers" = "new covers set". alias symbol "covers" = "new covers". alias symbol "covers" = "new covers set". alias symbol "covers" = "new covers". ntheorem new_coverage_infinity: ∀A:nAx.∀U:Ω^A.∀a:A. (∃i:𝐈 a. 𝐈𝐦[𝐝 a i] ◃ U) → a ◃ U. -#A; #U; #a; *; #i; #H; nnormalize in H; +#A; #U; #a;(** screenshot "topology/figure1". *) +*; #i; #H; nnormalize in H; ncut (∀y:𝐃 a i.∃x:Ord A.𝐝 a i y ∈ U⎽x); ##[ #y; napply H; @ y; napply #; ##] #H'; ncases (AC … H'); #f; #Hf; diff --git a/helm/software/matita/nlibrary/topology/postamble.xml b/helm/software/matita/nlibrary/topology/postamble.xml new file mode 100644 index 000000000..70723d917 --- /dev/null +++ b/helm/software/matita/nlibrary/topology/postamble.xml @@ -0,0 +1,2 @@ + + diff --git a/helm/software/matita/nlibrary/topology/preamble.xml b/helm/software/matita/nlibrary/topology/preamble.xml new file mode 100644 index 000000000..ffb7483ec --- /dev/null +++ b/helm/software/matita/nlibrary/topology/preamble.xml @@ -0,0 +1,26 @@ + + + + + + +