let load_easter_egg = lazy (
win#browserImage#set_file (MatitaMisc.image_path "meegg.png"))
in
+ let load_hints () =
+ let module Pp = GraphvizPp.Dot in
+ let filename, oc = Filename.open_temp_file "matita" ".dot" in
+ let fmt = Format.formatter_of_out_channel oc in
+ let status = (MatitaScript.current ())#grafite_status in
+ Pp.header
+ ~name:"Hints"
+ ~graph_type:"graph"
+ ~graph_attrs:["overlap", "false"]
+ ~node_attrs:["fontsize", "9"; "width", ".4";
+ "height", ".4"; "shape", "box"]
+ ~edge_attrs:["fontsize", "10"; "len", "2"] fmt;
+ NCicUnifHint.generate_dot_file status fmt;
+ Pp.trailer fmt;
+ Pp.raw "@." fmt;
+ close_out oc;
+ gviz#load_graph_from_file ~gviz_cmd:"neato -Tpng" filename;
+ (*HExtlib.safe_remove filename*)
+ in
let load_coerchgraph tred () =
let module Pp = GraphvizPp.Dot in
let filename, oc = Filename.open_temp_file "matita" ".dot" in
| `About `Us -> self#egg ()
| `About `CoercionsFull -> self#coerchgraph false ()
| `About `Coercions -> self#coerchgraph true ()
+ | `About `Hints -> self#hints ()
| `About `TeX -> self#tex ()
| `About `Grammar -> self#grammar ()
| `Check term -> self#_loadCheck term
load_coerchgraph tred ();
self#_showGviz
+ method private hints () =
+ load_hints ();
+ self#_showGviz
+
method private tex () =
let b = Buffer.create 1000 in
Printf.bprintf b "UTF-8 equivalence classes (rotate with ALT-L):\n\n";
method private _loadTermNCic term m s c =
let d = 0 in
- let m = (0,(None,c,term))::m in
+ let m = (0,([],c,term))::m in
let status = (MatitaScript.current ())#grafite_status in
mathView#nload_sequent status m s d;
self#_showMath
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 width = 500 in
let height = 2000 in
let m = GMathView.math_view
~font_size:!current_font_size ~width ~height
~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 (mno,_ as 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,mno)
+ sequents
+ in
+ let items =
+ List.map (fun (x,mno) ->
+ ignore(Sys.command
+ (Printf.sprintf
+ ("convert "^^
+ " '(' -gravity west -bordercolor grey -border 1 label:%d ')' "^^
+ " '(' -trim -bordercolor white -border 5 "^^
+ " -bordercolor grey -border 1 %s ')' -append %s ")
+ mno
+ (Filename.quote x)
+ (Filename.quote (x ^ ".label.png"))));
+ x ^ ".label.png")
+ filenames
+ in
+ let rec div2 = function
+ | [] -> []
+ | [x] -> [[x]]
+ | x::y::tl -> [x;y] :: div2 tl
+ in
+ let items = div2 items in
ignore(Sys.command (Printf.sprintf
- "convert -trim -border 3 -bordercolor white %s %s"
- (Filename.quote filename)
+ "convert %s -append %s"
+ (String.concat ""
+ (List.map (fun items ->
+ Printf.sprintf " '(' %s +append ')' "
+ (String.concat
+ (" '(' -gravity center -size 10x10 xc: ')' ") items)) items))
(Filename.quote (ofn ^ ".png"))));
+ List.iter (fun x,_ -> Sys.remove x) filenames;
+ List.iter Sys.remove (List.flatten items);
w#destroy ();
end