From e92ed86ef80add294c5b7fa84b1ea7d0d88c9bbd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 18 Apr 2002 17:03:22 +0000 Subject: [PATCH] Scratch window is now also raised (= hide + show ;-| when updated. --- helm/gTopLevel/gTopLevel.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 800e69aa0..93924b9ad 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -784,7 +784,7 @@ class scratch_window () = GMathView.math_view ~packing:(window#add) ~width:400 ~height:280 () in object(self) method display = mmlwidget#load_tree - method show = window#show + method show () = window#misc#hide () ; window#show () initializer ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) end;; @@ -888,7 +888,7 @@ object(self) method inputt = inputt method output = (output : GMathView.math_view) method proofw = (proofw : GMathView.math_view) - method show () = window#show () + method show = window#show initializer button_export_to_postscript#misc#set_sensitive false ; -- 2.39.2