X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=5b8540875124cf5841b6facce09037c7864d3cc8;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=492aece49cf3b3a322fdad5065ef7909f45ab615;hpb=bee436af0c6ceb1c83259c94036df8b12f901f2d;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 492aece49..5b8540875 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -959,7 +959,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" in let metadata_RE = Pcre.regexp "^metadata:/(deps)/(forward|backward)/(.*)$" in let whelp_query_RE = Pcre.regexp - "^\\s*whelp\\s+([^\\s]+)\\s+(\"|\\()(.*)(\\)|\")$" + "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in let is_metadata txt = Pcre.pmatch ~rex:metadata_RE txt in let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in @@ -981,7 +981,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) combo#set_active (aux 0 queries); in let searchText = - GSourceView.source_view ~auto_indent:false ~editable:false () + GSourceView2.source_view ~auto_indent:false ~editable:false () in let _ = win#scrolledwinContent#add (searchText :> GObj.widget); @@ -1035,6 +1035,25 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 @@ -1261,6 +1280,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `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 @@ -1275,7 +1295,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `NRef nref -> self#_loadNReference nref | `Univs uri -> self#_loadUnivs uri | `Whelp (query, results) -> - set_whelp_query query; self#_loadList (List.map (fun r -> "obj", UriManager.string_of_uri r) results)); self#setEntry entry @@ -1324,6 +1343,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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"; @@ -1452,7 +1475,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 @@ -1576,23 +1599,64 @@ 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 + method screenshot status sequents metasenv subst (filename as ofn) = let w = GWindow.window ~title:"screenshot" () in + let width = 500 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 - GdkPixbuf.get_from_drawable ~dest:pixbuf pixmap; - let filename = filename ^ ".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 %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