Parcourir la source

[display] don't overwrite import positions if they already exist

Simon Krajewski il y a 7 ans
Parent
commit
73e571451a
1 fichiers modifiés avec 3 ajouts et 1 suppressions
  1. 3 1
      src/context/display/importHandling.ml

+ 3 - 1
src/context/display/importHandling.ml

@@ -44,7 +44,9 @@ let convert_import_to_something_usable pt path =
 	loop [] None None path
 
 let add_import_position com p path =
-	com.shared.shared_display_information.import_positions <- PMap.add p (ref false,path) com.shared.shared_display_information.import_positions
+	let infos = com.shared.shared_display_information in
+	if not (PMap.mem p infos.import_positions) then
+		infos.import_positions <- PMap.add p (ref false,path) infos.import_positions
 
 let mark_import_position com p =
 	try