mirror of
https://github.com/jupyter/notebook.git
synced 2024-12-27 04:20:22 +08:00
67 lines
1.9 KiB
Python
67 lines
1.9 KiB
Python
"""Notebook related utilities
|
|
|
|
Authors:
|
|
|
|
* Brian Granger
|
|
"""
|
|
|
|
#-----------------------------------------------------------------------------
|
|
# Copyright (C) 2011 The IPython Development Team
|
|
#
|
|
# Distributed under the terms of the BSD License. The full license is in
|
|
# the file COPYING, distributed as part of this software.
|
|
#-----------------------------------------------------------------------------
|
|
|
|
import os
|
|
from urllib import quote, unquote
|
|
|
|
#-----------------------------------------------------------------------------
|
|
# Imports
|
|
#-----------------------------------------------------------------------------
|
|
|
|
def url_path_join(*pieces):
|
|
"""Join components of url into a relative url
|
|
|
|
Use to prevent double slash when joining subpath. This will leave the
|
|
initial and final / in place
|
|
"""
|
|
initial = pieces[0].startswith('/')
|
|
final = pieces[-1].endswith('/')
|
|
stripped = [s.strip('/') for s in pieces]
|
|
result = '/'.join(s for s in stripped if s)
|
|
if initial: result = '/' + result
|
|
if final: result = result + '/'
|
|
if result == '//': result = '/'
|
|
return result
|
|
|
|
def path2url(path):
|
|
"""Convert a local file path to a URL"""
|
|
pieces = [ quote(p) for p in path.split(os.path.sep) ]
|
|
# preserve trailing /
|
|
if pieces[-1] == '':
|
|
pieces[-1] = '/'
|
|
url = url_path_join(*pieces)
|
|
return url
|
|
|
|
def url2path(url):
|
|
"""Convert a URL to a local file path"""
|
|
pieces = [ unquote(p) for p in url.split('/') ]
|
|
path = os.path.join(*pieces)
|
|
return path
|
|
|
|
def url_escape(path):
|
|
"""Escape special characters in a URL path
|
|
|
|
Turns '/foo bar/' into '/foo%20bar/'
|
|
"""
|
|
parts = path.split('/')
|
|
return '/'.join([quote(p) for p in parts])
|
|
|
|
def url_unescape(path):
|
|
"""Unescape special characters in a URL path
|
|
|
|
Turns '/foo%20bar/' into '/foo bar/'
|
|
"""
|
|
return '/'.join([unquote(p) for p in path.split('/')])
|
|
|