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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 800e69aa07b485cd326638ad3b3f5ba33caee01c..93924b9ada6a71331a28f5cb7002844dc88659c6 100644 (file)
--- 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 ;