From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Apr 2002 17:03:22 +0000 (+0000)
Subject: Scratch window is now also raised (= hide + show ;-| when updated.
X-Git-Tag: V_0_3_0_debian_8~139
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e92ed86ef80add294c5b7fa84b1ea7d0d88c9bbd

Scratch window is now also raised (= hide + show ;-| when updated.
---

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 ;