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 *)
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 =
nmacro: [
[ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
+ | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
]
];
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
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 \
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
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:
lablGraphviz.mli \
matitaTypes.mli \
matitaMisc.mli \
+ applyTransformation.mli \
matitaEngine.mli \
matitaExcPp.mli \
- applyTransformation.mli \
matitacLib.mli \
matitaInit.mli \
matitaGtkMisc.mli \
CMLI = \
matitaTypes.mli \
matitaMisc.mli \
+ applyTransformation.mli \
matitaEngine.mli \
matitaExcPp.mli \
- applyTransformation.mli \
matitacLib.mli \
matitaInit.mli \
matitaWiki.mli \
<block-comment _name = "Commented Code" style = "Comment">
<start-regex>\(\*\*[^\)]</start-regex>
- <end-regex>[^\(]\*\*\)</end-regex>
+ <end-regex>[^\(]\*\)</end-regex>
</block-comment>
<block-comment _name = "Block Comment" style = "Comment">
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
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 () =
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
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
| (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
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
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
--- /dev/null
+
+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 >> $@
+
--- /dev/null
+BEGIN { p = 1; indent = ""; }
+/DOCBEGIN/ { indent = ""; NF = 0; }
+/DOCEND/ { indent = " "; NF = 0; }
+/HIDE/ { p = 0; }
+{ if (p == 1) print indent $0; }
+/UNHIDE/ { p = 1; }
+(*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 }.
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.
(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;
naxiom setoidification :
∀A:nAx.∀a,b:A.∀U.a=b → b ∈ U → a ∈ U.
+(*DOCBEGIN
+
+Bla Bla,
+
+<div id="figure1" class="img" ><img src="figure1.png"/>foo</div>
+
+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;
--- /dev/null
+ </body>
+</html>
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+<html>
+ <head>
+ <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+ <style type="text/css">
+ pre, code {
+ font-family: Sans;
+ font-size: 1em;
+ background-color:#efee79; }
+ pre { margin-right: 5em;}
+ img { display: block; margin-bottom: 1em; }
+ .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>
+ <body>
projects / helm.git / commitdiff