X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=e76c659a4cb42ab194754060e36ca392fb76192e;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=277dbe8f1d0361eafdbebff1a34270bd7ef27799;hpb=9e7df95a820cb91d075f1a20d703175da874596c;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 277dbe8f1..e76c659a4 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,11 +802,11 @@ 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 - { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack } - = + method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit + = fun status -> + let _,_,metasenv,subst,_ = status#obj in _metasenv <- `New (metasenv,subst); pages <- 0; let win goal_switch = @@ -825,7 +831,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = w#coerce in assert ( - let stack_goals = Stack.open_goals stack in + let stack_goals = Stack.open_goals status#stack in let proof_goals = List.map fst metasenv in if HExtlib.list_uniq (List.sort Pervasives.compare stack_goals) @@ -863,27 +869,31 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = match depth, pos with | 0, 0 -> `Current (render_switch sw) | 0, _ -> `Shift (pos, `Current (render_switch sw)) - | 1, pos when Stack.head_tag stack = `BranchTag -> + | 1, pos when Stack.head_tag status#stack = `BranchTag -> `Shift (pos, render_switch sw) | _ -> render_switch sw in add_tab markup sw) ~cont:add_switch ~todo:add_switch - stack; + status#stack; switch_page_callback <- Some (notebook#connect#switch_page ~callback:(fun page -> let goal_switch = 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); @@ -892,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 @@ -901,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 @@ -933,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 ] @@ -1023,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) @@ -1233,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)) -> @@ -1294,6 +1344,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"; @@ -1335,7 +1389,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private home () = self#_showMath; - match self#script#grafite_status.proof_status with + match self#script#grafite_status#proof_status with | Proof (uri, metasenv, _subst, bo, ty, attrs) -> let name = UriManager.name_of_uri (HExtlib.unopt uri) in let obj = @@ -1349,10 +1403,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) in self#_loadObj obj | _ -> - match self#script#grafite_status.ng_status with - ProofMode tstatus -> - let nobj = tstatus.NTacStatus.istatus.NTacStatus.pstatus in - self#_loadNObj nobj + 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 @@ -1364,7 +1418,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 @@ -1406,12 +1460,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 @@ -1420,6 +1474,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,(None,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; @@ -1538,6 +1599,56 @@ 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 + ignore(Sys.command (Printf.sprintf + "convert %s +append %s" + (String.concat (" '(' -gravity center -size 10x10 xc: ')' ") items) + (Filename.quote (ofn ^ ".png")))); + List.iter (fun x,_ -> Sys.remove x) filenames; + List.iter Sys.remove items; + w#destroy (); end let refresh_all_browsers () =