X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=723170fa50812cc9b510b21c6e3ab0fc07348d72;hb=c8718cc46ab9aaca047366dfefe72bc7c9402e5a;hp=4b5a9fc1dd0ab4be0e710ce119b3c9898f898dec;hpb=ba53effd71fdfdc046dc39ea9dd7f07cf823a1b6;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index 4b5a9fc1d..723170fa5 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -34,12 +34,6 @@ open CicMathView module Stack = Continuationals.Stack -(** inherit from this class if you want to access current script *) -class scriptAccessor = -object (self) - method private script = MatitaScript.current () -end - let cicBrowsers = ref [] let tab_label meta_markup = @@ -57,8 +51,6 @@ let goal_of_switch = function Stack.Open g | Stack.Closed g -> g class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = object (self) - inherit scriptAccessor - method cicMathView = cicMathView (** clickableMathView accessor *) val mutable pages = 0 @@ -66,7 +58,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = val mutable page2goal = [] (* associative list: page no -> goal no *) val mutable goal2page = [] (* the other way round *) val mutable goal2win = [] (* associative list: goal no -> scrolled win *) - val mutable _metasenv = `Old [] + val mutable _metasenv = [],[] val mutable scrolledWin: GBin.scrolled_window option = None (* scrolled window to which the sequentViewer is currently attached *) val logo = (GMisc.image @@ -105,13 +97,12 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = page2goal <- []; goal2page <- []; goal2win <- []; - _metasenv <- `Old []; - self#script#setGoal None + _metasenv <- [],[] method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit = fun (status : #GrafiteTypes.status) -> let _,_,metasenv,subst,_ = status#obj in - _metasenv <- `New (metasenv,subst); + _metasenv <- metasenv,subst; pages <- 0; let win goal_switch = let w = @@ -120,16 +111,21 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = in let reparent () = scrolledWin <- Some w; - match cicMathView#misc#parent with - | None -> w#add cicMathView#coerce - | Some parent -> - let parent = - match cicMathView#misc#parent with - None -> assert false - | Some p -> GContainer.cast_container p - in - parent#remove cicMathView#coerce; - w#add cicMathView#coerce + (match cicMathView#misc#parent with + | None -> () + | Some parent -> + let parent = + match cicMathView#misc#parent with + None -> assert false + | Some p -> GContainer.cast_container p + in + parent#remove cicMathView#coerce); + w#add cicMathView#coerce; + ignore (w#vadjustment#set_value + (w#vadjustment#upper -. w#vadjustment#page_size)); + ignore (w#vadjustment#connect#changed (fun _ -> + w#vadjustment#set_value + (w#vadjustment#upper -. w#vadjustment#page_size))) in goal2win <- (goal_switch, reparent) :: goal2win; w#coerce @@ -185,7 +181,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: @@ -194,10 +189,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () = = fun status ~page ~goal_switch -> (match goal_switch with | Stack.Open goal -> - (match _metasenv with - `Old menv -> assert false (* MATITA 1.0 *) - | `New (menv,subst) -> - cicMathView#nload_sequent status menv subst goal) + let menv,subst = _metasenv in + cicMathView#nload_sequent status menv subst goal | Stack.Closed goal -> let root = Lazy.force closed_goal_mathml in cicMathView#load_root ~root); @@ -240,7 +233,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 +286,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 +309,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; @@ -329,8 +323,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) HExtlib.safe_remove filename in object (self) - inherit scriptAccessor - val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec"; val dep_contextual_menu = GMenu.menu () @@ -552,19 +544,20 @@ 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 (get_matita_script_current ())#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 - | _ -> self#blank () + let status = (get_matita_script_current ())#status in + match status#ng_mode with + `ProofMode -> self#_loadNObj status 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 + let status = (get_matita_script_current ())#status in + let obj = NCicEnvironment.get_checked_obj status uri in + self#_loadNObj status obj method private _loadDir dir = let content = Http_getter.ls ~local:false dir in @@ -594,7 +587,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 +625,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 @@ -650,7 +639,7 @@ let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) (): = (new sequentsViewer ~notebook ~cicMathView ():> MatitaGuiTypes.sequentsViewer) -let cicBrowser () = +let new_cicBrowser () = let size = BuildTimeConf.browser_history_size in let rec aux history = let browser = new cicBrowser_impl ~history () in @@ -668,49 +657,51 @@ let cicBrowser () = GdkKeysyms._W (fun () -> win#toplevel#destroy ()); *) cicBrowsers := browser :: !cicBrowsers; - (browser :> MatitaGuiTypes.cicBrowser) + browser in let history = new MatitaMisc.browser_history size (`About `Blank) in aux history +(** @param reuse if set reused last opened cic browser otherwise +* opens a new one. default is false *) +let cicBrowser ?(reuse=false) t = + let browser = + if reuse then + (match !cicBrowsers with [] -> new_cicBrowser () | b :: _ -> b) + else + new_cicBrowser () + in + match t with + None -> () + | Some t -> browser#load t +;; + let default_cicMathView () = let res = cicMathView ~show:true () in res#set_href_callback (Some (fun uri -> let uri = `NRef (NReference.reference_of_string uri) in - (cicBrowser ())#load uri)); + cicBrowser (Some uri))); res 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 ()) - - method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t - - end + 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) 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)