code: def extract_from_text(text):
      
      return tools.remove_duplicates([i[0]
                                      for i in REGEX.findall(text) if i != ''])
docs: Extract HAL ids from a text.
  
      :param text: The text to extract HAL ids from.
      :returns: A list of matching HAL ids.
  
      >>> sorted(extract_from_text("hal-01258754 hal-01258754v2 foobar"))
      ['hal-01258754', 'hal-01258754v2']