X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaMathView.ml;h=71e7cb55334540bbbf61640ecf5b2f2d4b5fcec7;hb=2c38e6a237e6a0e263abccf8d8ef3e7a31272443;hp=a6aa89e8190cb62a2a0414241d113d21bbdecf5b;hpb=442f3a15d7c6afc480da02602d4d4c8db4f44c10;p=helm.git diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index a6aa89e81..71e7cb553 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -186,11 +186,8 @@ object (self) method set_href_callback f = href_callback <- f val mutable _cic_info = None - val mutable _ncic_info = None method private set_cic_info info = _cic_info <- info method private cic_info = _cic_info - method private set_ncic_info info = _ncic_info <- info - method private ncic_info = _ncic_info val normal_cursor = Gdk.Cursor.create `LEFT_PTR val href_cursor = Gdk.Cursor.create `HAND2 @@ -514,11 +511,6 @@ object (self) info, (~-1, [], t) (* dummy sequent for obj *) | None -> assert false - method private get_ncic_info id = - match self#ncic_info with - | Some info -> info - | None -> assert false - method private sequent_of_id ~(paste_kind:paste_kind) id = let cic_info, unsh_sequent = self#get_cic_info id in let cic_sequent = @@ -601,12 +593,15 @@ 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,ids_to_father_ids = - ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent) + let mathml = + ApplyTransformation.nmml_of_cic_sequent status metasenv subst + (metano,sequent) in - self#set_ncic_info (Some ids_to_father_ids); if BuildTimeConf.debug then begin let name = "/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in @@ -639,10 +634,13 @@ object (self) self#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); - method load_nobject obj = - let mathml,ids_to_father_ids = ApplyTransformation.nmml_of_cic_object obj in - self#set_ncic_info (Some ids_to_father_ids); + 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)); (match current_mathml with | Some current_mathml when use_diff -> self#freeze; @@ -726,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 = @@ -804,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 = @@ -833,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) @@ -871,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); @@ -900,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 @@ -909,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 @@ -941,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 ] @@ -977,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); @@ -1031,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) @@ -1241,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)) -> @@ -1302,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"; @@ -1343,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 = @@ -1357,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 @@ -1372,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 @@ -1414,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 @@ -1428,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,([],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; @@ -1546,6 +1599,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 () =