X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=5b40bb4195ed2795b1dd6b2cbc563b34d38172e9;hb=364d23cb116e167d3b23f6ef0412830e816e5e92;hp=1b8d608c2e688c0505522d7a352d540313639951;hpb=ad3546bfc633935891d8c69ea704c86207c83f57;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 1b8d608c2..5b40bb419 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -37,7 +37,7 @@ module Stack = Continuationals.Stack (** inherit from this class if you want to access current script *) class scriptAccessor = object (self) - method private script = MatitaScript.current () + method private script = get_matita_script_current () end let cicBrowsers = ref [] @@ -105,8 +105,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = page2goal <- []; goal2page <- []; goal2win <- []; - _metasenv <- `Old []; - self#script#setGoal None + _metasenv <- `Old [] method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit = fun (status : #GrafiteTypes.status) -> @@ -185,7 +184,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = 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 status ~page ~goal_switch)) method private render_page: @@ -240,7 +238,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in let gui = MatitaMisc.get_gui () in - let (win: MatitaGuiTypes.browserWin) = gui#newBrowserWin () in + let win = new MatitaGeneratedGui.browserWin () in + let _ = win#browserUri#misc#grab_focus () in let gviz = LablGraphviz.graphviz ~packing:win#graphScrolledWin#add () in let searchText = GSourceView2.source_view ~auto_indent:false ~editable:false () @@ -292,7 +291,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 + let status = (get_matita_script_current ())#status in Pp.header ~name:"Hints" ~graph_type:"graph" @@ -315,7 +314,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ~name:"Coercions" ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"] ~edge_attrs:["fontsize", "10"] fmt; - let status = (MatitaScript.current ())#grafite_status in + let status = (get_matita_script_current ())#status in NCicCoercion.generate_dot_file status fmt; Pp.trailer fmt; Pp.raw "@." fmt; @@ -552,19 +551,17 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_showSearch method private grammar () = - self#_loadText (Print_grammar.ebnf_of_term self#script#grafite_status); + self#_loadText (Print_grammar.ebnf_of_term self#script#status); method private home () = self#_showMath; - match self#script#grafite_status#ng_mode with - `ProofMode -> - self#_loadNObj self#script#grafite_status - self#script#grafite_status#obj + match self#script#status#ng_mode with + `ProofMode -> self#_loadNObj self#script#status self#script#status#obj | _ -> self#blank () method private _loadNReference (NReference.Ref (uri,_)) = let obj = NCicEnvironment.get_checked_obj uri in - self#_loadNObj self#script#grafite_status obj + self#_loadNObj self#script#status obj method private _loadDir dir = let content = Http_getter.ls ~local:false dir in @@ -594,7 +591,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 + let status = (get_matita_script_current ())#status in mathView#nload_sequent status m s d; self#_showMath @@ -632,10 +629,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_load entry; self#_historyAdd entry - (** {2 methods accessing underlying GtkMathView} *) - - method updateFontSize = mathView#set_font_size (MatitaMisc.get_current_font_size ()) - (** {2 methods used by constructor only} *) method win = win @@ -684,94 +677,34 @@ let default_cicMathView () = let cicMathView_instance = MatitaMisc.singleton default_cicMathView -let default_sequentsViewer () = - let gui = MatitaMisc.get_gui () in +let default_sequentsViewer notebook = let cicMathView = cicMathView_instance () in - sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView () -let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer - -let mathViewer () = - object(self) - method private get_browser reuse = - if reuse then - (match !cicBrowsers with - | [] -> cicBrowser () - | b :: _ -> (b :> MatitaGuiTypes.cicBrowser)) - else - (cicBrowser ()) + sequentsViewer ~notebook ~cicMathView () +let sequentsViewer_instance = + let already_used = ref false in + fun notebook -> + if !already_used then assert false + else + (already_used := true; + default_sequentsViewer notebook) - method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t - - method screenshot status sequents metasenv subst (filename as ofn) = - () (*MATITA 1.0 - let w = GWindow.window ~title:"screenshot" () in - let width = 500 in - let height = 2000 in - let m = GMathView.math_view - ~font_size:(MatitaMisc.get_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 +(** @param reuse if set reused last opened cic browser otherwise +* opens a new one. default is false *) +let show_entry ?(reuse=false) t = + let browser = + if reuse then + (match !cicBrowsers with + [] -> cicBrowser () + | b :: _ -> (b :> MatitaGuiTypes.cicBrowser)) + else + cicBrowser () + in + browser#load t +;; let refresh_all_browsers () = List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers -let update_font_sizes () = - List.iter (fun b -> b#updateFontSize) !cicBrowsers; - (cicMathView_instance ())#update_font_size - let get_math_views () = (cicMathView_instance ()) :: (List.map (fun b -> b#mathView) !cicBrowsers)