X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=5b8540875124cf5841b6facce09037c7864d3cc8;hb=f38fd769279794d0ca73c8945eac30e8b42e59be;hp=22ad1e4cf144c6e9ed8fe4fb037d94862b7fa540;hpb=290350836dd1727b3e3cdd4ee71e666a39cc4a09;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 22ad1e4cf..5b8540875 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -593,10 +593,14 @@ object (self) end; self#load_root ~root:mathml#get_documentElement - method nload_sequent metasenv subst metano = + method nload_sequent: + 'status. #NCicCoercion.status as 'status -> NCic.metasenv -> + NCic.substitution -> int -> unit + = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in let mathml = - ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent) + ApplyTransformation.nmml_of_cic_sequent status metasenv subst + (metano,sequent) in if BuildTimeConf.debug then begin let name = @@ -630,8 +634,10 @@ object (self) self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); - method load_nobject obj = - let mathml = ApplyTransformation.nmml_of_cic_object obj in + method load_nobject : + 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit + = fun status obj -> + let mathml = ApplyTransformation.nmml_of_cic_object status obj in (* self#set_cic_info (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj)); @@ -718,9 +724,9 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = _metasenv <- `Old []; self#script#setGoal None - method load_sequents - { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack } - = + method load_sequents : 'status. #NCicCoercion.status as 'status -> 'a + = fun status { proof= (_,metasenv,_subst,_,_, _) as proof; stack = stack } + -> _metasenv <- `Old metasenv; pages <- 0; let win goal_switch = @@ -796,9 +802,10 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = try List.assoc page page2goal with Not_found -> assert false in self#script#setGoal (Some (goal_of_switch goal_switch)); - self#render_page ~page ~goal_switch)) + self#render_page status ~page ~goal_switch)) - method nload_sequents (status : NTacStatus.tac_status) = + method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit + = fun status -> let _,_,metasenv,subst,_ = status#obj in _metasenv <- `New (metasenv,subst); pages <- 0; @@ -875,14 +882,18 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = try List.assoc page page2goal with Not_found -> assert false in self#script#setGoal (Some (goal_of_switch goal_switch)); - self#render_page ~page ~goal_switch)) + self#render_page status ~page ~goal_switch)) - method private render_page ~page ~goal_switch = + method private render_page: + 'status. #NCicCoercion.status as 'status -> page:int -> + goal_switch:Stack.switch -> unit + = fun status ~page ~goal_switch -> (match goal_switch with | Stack.Open goal -> (match _metasenv with `Old menv -> cicMathView#load_sequent menv goal - | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal) + | `New (menv,subst) -> + cicMathView#nload_sequent status menv subst goal) | Stack.Closed goal -> let doc = Lazy.force closed_goal_mathml in cicMathView#load_root ~root:doc#get_documentElement); @@ -891,7 +902,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = List.assoc goal_switch goal2win () with Not_found -> assert false) - method goto_sequent goal = + method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit + = fun status goal -> let goal_switch, page = try List.find @@ -900,7 +912,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = with Not_found -> assert false in notebook#goto_page page; - self#render_page page goal_switch + self#render_page status ~page ~goal_switch end @@ -932,6 +944,7 @@ let current_proof_uri = BuildTimeConf.current_proof_uri type term_source = [ `Ast of CicNotationPt.term | `Cic of Cic.term * Cic.metasenv + | `NCic of NCic.term * NCic.context * NCic.metasenv * NCic.substitution | `String of string ] @@ -946,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 @@ -968,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); @@ -1022,15 +1035,50 @@ 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 str = CoercGraph.generate_dot_file () in + let module Pp = GraphvizPp.Dot in let filename, oc = Filename.open_temp_file "matita" ".dot" in - output_string oc str; + let fmt = Format.formatter_of_out_channel oc in + Pp.header + ~name:"Coercions" + ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] + ~edge_attrs:["fontsize", "10"] fmt; + let status = (MatitaScript.current ())#grafite_status in + NCicCoercion.generate_dot_file status fmt; + Pp.trailer fmt; + Pp.header + ~name:"OLDCoercions" + ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] + ~edge_attrs:["fontsize", "10"] fmt; + CoercGraph.generate_dot_file fmt; + Pp.trailer fmt; + Pp.raw "@." fmt; close_out oc; if tred then - gviz#load_graph_from_file ~gviz_cmd:"tred|dot" filename + gviz#load_graph_from_file + ~gviz_cmd:"dot -Txdot | tred |gvpack -gv | dot" filename else - gviz#load_graph_from_file filename; + gviz#load_graph_from_file + ~gviz_cmd:"dot -Txdot | gvpack -gv | dot" filename; HExtlib.safe_remove filename in object (self) @@ -1232,10 +1280,13 @@ 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 | `Cic (term, metasenv) -> self#_loadTermCic term metasenv + | `NCic (term, ctx, metasenv, subst) -> + self#_loadTermNCic term metasenv subst ctx | `Dir dir -> self#_loadDir dir | `HBugs `Tutors -> self#_loadHBugsTutors | `Metadata (`Deps ((`Fwd | `Back) as dir, uri)) -> @@ -1244,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 @@ -1293,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"; @@ -1348,8 +1402,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in self#_loadObj obj | _ -> - match self#script#grafite_status#ng_status with - ProofMode tstatus -> self#_loadNObj tstatus#obj + match self#script#grafite_status#ng_mode with + `ProofMode -> + self#_loadNObj self#script#grafite_status + self#script#grafite_status#obj | _ -> self#blank () (** loads a cic uri from the environment @@ -1361,7 +1417,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadNReference (NReference.Ref (uri,_)) = let obj = NCicEnvironment.get_checked_obj uri in - self#_loadNObj obj + self#_loadNObj self#script#grafite_status obj method private _loadUnivs uri = let uri = UriManager.strip_xpointer uri in @@ -1403,12 +1459,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showMath; mathView#load_object obj - method private _loadNObj obj = + method private _loadNObj status obj = (* showMath must be done _before_ loading the document, since if the * widget is not mapped (hidden by the notebook) the document is not * rendered *) self#_showMath; - mathView#load_nobject obj + mathView#load_nobject status obj method private _loadTermCic term metasenv = let context = self#script#proofContext in @@ -1417,6 +1473,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) mathView#load_sequent (sequent :: metasenv) dummyno; self#_showMath + method private _loadTermNCic term m s c = + let d = 0 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 private _loadList l = model#list_store#clear (); List.iter (fun (tag, s) -> model#easy_append ~tag s) l; @@ -1535,6 +1598,66 @@ let mathViewer () = method show_uri_list ?(reuse=false) ~entry l = (self#get_browser reuse)#load entry + + 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 ~height + ~packing:w#add + ~show:true () + in + w#show (); + 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 let refresh_all_browsers () =