[c_selection.js] If safari_mobile, get current selection from a previously created global variable
[c_sync.js] ref where the safari_mobile global is used
[c_text_view_comments.js] if safari_mobile update selection also on selectionChange event
[text_view_comments.html] if safari_mobile store a clone of the current selection on each selectionChange
set layout width to 99% to improve display
factorize safari mobile detection code
def remove_extension(file_name):
"""
Remove 3 letters and 4 letters extension from filename
>>> remove_extension('my file.tex')
'my file'
>>> remove_extension('my file.html')
'my file'
>>> remove_extension('my file')
'my file'
"""
for point_loc in [3,4]:
if len(file_name)>point_loc and file_name[-point_loc-1] == '.':
return file_name[:-point_loc-1]
return file_name
if __name__ == "__main__":
import doctest
doctest.testmod()