From 0ff06c9ed5e1f61dbf38c06ff0885cec794d7250 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 9 Nov 2000 12:32:49 +0000 Subject: [PATCH] Selection fixed --- helm/interface/mmlinterface.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) 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 ;; -- 2.39.2