X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=2a17d938b9d74d0017776db845430ec5e1f5f73f;hb=4b3a9a15edbab7a3aa819155dc1ac1eec1ddb0a3;hp=e00e4fdc5107995bce576f8c0f030c6d524c5821;hpb=f3d0ba1e75bc3383d766f3a33a19352db19854df;p=helm.git diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index e00e4fdc5..2a17d938b 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -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: @@ -680,12 +678,16 @@ 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 - + 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) (** @param reuse if set reused last opened cic browser otherwise * opens a new one. default is false *)