let win goal_switch =
let w =
GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
- ~shadow_type:`IN ~show:true ()
- in
+ ~shadow_type:`IN ~show:true () 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
in
goal2win <- (goal_switch, reparent) :: goal2win;
w#coerce
cicMathView#load_root ~root);
(try
cicMathView#set_selection None;
- List.assoc goal_switch goal2win ()
+ List.assoc goal_switch goal2win ();
+ (match cicMathView#misc#parent with
+ None -> assert false
+ | Some p ->
+ (* The text widget dinamycally inserts the text in a separate
+ thread. We need to wait for it to terminate before we can
+ move the scrollbar to the end *)
+ while Glib.Main.pending()do ignore(Glib.Main.iteration false); done;
+ let w =
+ new GBin.scrolled_window
+ (Gobject.try_cast p#as_widget "GtkScrolledWindow") in
+ (* The double change upper/lower is to trigger the emission of
+ changed :-( *)
+ w#hadjustment#set_value w#hadjustment#upper;
+ w#hadjustment#set_value w#hadjustment#lower;
+ w#vadjustment#set_value w#vadjustment#lower;
+ w#vadjustment#set_value
+ (w#vadjustment#upper -. w#vadjustment#page_size));
with Not_found -> assert false)
method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
in
notebook#goto_page page;
self#render_page status ~page ~goal_switch
-
end
let blank_uri = BuildTimeConf.blank_uri
HExtlib.safe_remove filename
in
object (self)
- val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec";
+ val mutable gviz_uri =
+ let uri = NUri.uri_of_string "cic:/dummy/dec.con" in
+ NReference.reference_of_spec uri NReference.Decl;
val dep_contextual_menu = GMenu.menu ()
| _ -> self#blank ()
method private _loadNReference (NReference.Ref (uri,_)) =
- let obj = NCicEnvironment.get_checked_obj uri in
- self#_loadNObj (get_matita_script_current ())#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
=
(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
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 =
let default_sequentsViewer notebook =
let cicMathView = cicMathView_instance () in
sequentsViewer ~notebook ~cicMathView ()
+
let sequentsViewer_instance =
let already_used = ref false in
fun notebook ->
(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