From 1eba57d6ae8c7cb8adab81cf50674adaaa55eccc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 28 Dec 2010 21:51:28 +0000 Subject: [PATCH] Interface reduction; code clean up. --- matita/matita/matitaGui.ml | 18 +++++----------- matita/matita/matitaGuiTypes.mli | 5 ----- matita/matita/matitaMathView.ml | 35 ++++++++++++++++---------------- matita/matita/matitaMathView.mli | 9 ++------ matita/matita/matitaScript.ml | 2 +- 5 files changed, 26 insertions(+), 43 deletions(-) diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml index 236d32f68..d8916f7fa 100644 --- a/matita/matita/matitaGui.ml +++ b/matita/matita/matitaGui.ml @@ -825,21 +825,13 @@ class gui () = connect_menu_item main#newMenuItem self#newScript; connect_menu_item main#closeMenuItem self#closeCurrentScript; connect_menu_item main#showCoercionsGraphMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Coercions)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions))); connect_menu_item main#showHintsDbMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Hints)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints))); connect_menu_item main#showTermGrammarMenuItem - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `Grammar)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar))); connect_menu_item main#showUnicodeTable - (fun _ -> - let c = MatitaMathView.cicBrowser () in - c#load (`About `TeX)); + (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX))); (* debug menu *) main#debugMenu#misc#hide (); (* HBUGS *) @@ -862,7 +854,7 @@ class gui () = main#hpaneScriptSequent#set_position script_w; (* math view handling *) connect_menu_item main#newCicBrowserMenuItem (fun () -> - ignore(MatitaMathView.cicBrowser ())); + ignore(MatitaMathView.cicBrowser None)); connect_menu_item main#increaseFontSizeMenuItem MatitaMisc.increase_font_size; connect_menu_item main#decreaseFontSizeMenuItem diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index fa2583d06..f75769fb0 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -43,8 +43,3 @@ object method goto_sequent: #ApplyTransformation.status -> int -> unit (* to be called _after_ load_sequents *) end - -class type cicBrowser = -object - method load: MatitaTypes.mathViewer_entry -> unit -end diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index df8b5359d..a970c569f 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -633,7 +633,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 @@ -651,17 +651,31 @@ 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 = @@ -670,6 +684,7 @@ let cicMathView_instance = let default_sequentsViewer notebook = let cicMathView = cicMathView_instance () in sequentsViewer ~notebook ~cicMathView () + let sequentsViewer_instance = let already_used = ref false in fun notebook -> @@ -678,20 +693,6 @@ let sequentsViewer_instance = (already_used := true; default_sequentsViewer notebook) -(** @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 diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli index 8e323ddc4..dd1e18955 100644 --- a/matita/matita/matitaMathView.mli +++ b/matita/matita/matitaMathView.mli @@ -23,21 +23,16 @@ * http://helm.cs.unibo.it/ *) -(** {2 Instances} *) -val cicBrowser: unit -> MatitaGuiTypes.cicBrowser - (** {2 To be called just once} *) -val sequentsViewer_instance: GPack.notebook -> MatitaGuiTypes.sequentsViewer +val sequentsViewer_instance: GPack.notebook -> MatitaGuiTypes.sequentsViewer (** {2 Global changes} *) - val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *) (** {2 Rendering in a browser} *) - (** @param reuse if set reused last opened cic browser otherwise * opens a new one. default is false *) -val show_entry: ?reuse:bool -> MatitaTypes.mathViewer_entry -> unit +val cicBrowser: ?reuse:bool -> MatitaTypes.mathViewer_entry option -> unit (** {2 Clipboard & Selection handling} *) diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml index 37e0f9239..f1b20efe5 100644 --- a/matita/matita/matitaScript.ml +++ b/matita/matita/matitaScript.ml @@ -125,7 +125,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse NotationPt.Cast (t,NotationPt.Implicit `JustOne)) (* XXX use the metasenv, if possible *) in - MatitaMathView.show_entry (`NCic (t,ctx,m,s)); + MatitaMathView.cicBrowser (Some (`NCic (t,ctx,m,s))); [status, parsed_text], "", parsed_text_length | TA.NIntroGuess _loc -> let names_ref = ref [] in -- 2.39.2