From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 9 Nov 2000 12:32:49 +0000 (+0000)
Subject: Selection fixed
X-Git-Tag: nogzip~186
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=0ff06c9ed5e1f61dbf38c06ff0885cec794d7250;p=helm.git

Selection fixed
---

diff --git a/helm/interface/mmlinterface.ml b/helm/interface/mmlinterface.ml
index 2dfc5e4f9..dae8b8738 100755
--- a/helm/interface/mmlinterface.ml
+++ b/helm/interface/mmlinterface.ml
@@ -230,7 +230,7 @@ let jump rendering_window node =
 
 let choose_selection rendering_window node =
  let module M = Minidom in
- let rec aux ~first_time node =
+ let rec aux node =
   match M.node_get_attribute node (M.mDOMString_of_string "xref") with
      None ->
       let parent =
@@ -238,14 +238,12 @@ let choose_selection rendering_window node =
           None -> assert false
         | Some parent -> parent
       in
-       aux ~first_time:false parent
-   | Some s ->
-      if not first_time then
-       !(rendering_window#output)#set_selection (Some node)
+       aux parent
+   | Some s -> !(rendering_window#output)#set_selection (Some node)
  in
   match node with
-     None      -> () (* No element selected *)
-   | Some node -> aux ~first_time:true node
+     None      -> !(rendering_window#output)#set_selection None
+   | Some node -> aux node
 ;;