From 68f76d204cbb561fc0682f8882d61180bfc03350 2014-11-23 05:58:02
From: Thomas Kluyver <takowl@gmail.com>
Date: 2014-11-23 05:58:02
Subject: [PATCH] Add filename to header area

---

diff --git a/IPython/html/templates/texteditor.html b/IPython/html/templates/texteditor.html
index bb34c91..da20cf0 100644
--- a/IPython/html/templates/texteditor.html
+++ b/IPython/html/templates/texteditor.html
@@ -9,6 +9,12 @@
 #texteditor-container {
     border-bottom: 1px solid #ccc;
 }
+
+#filename {
+    font-size: 16pt;
+    display: table;
+    padding: 0px 5px;
+}
 </style>
 
 {{super()}}
@@ -21,6 +27,12 @@ data-file-path="{{file_path}}"
 
 {% endblock %}
 
+{% block header %}
+
+<span id="filename">{{ basename }}</span>
+
+{% endblock %}
+
 {% block site %}
 
 <div id="menubar-container" class="container">
diff --git a/IPython/html/texteditor/handlers.py b/IPython/html/texteditor/handlers.py
index 5933c02..aa05457 100644
--- a/IPython/html/texteditor/handlers.py
+++ b/IPython/html/texteditor/handlers.py
@@ -16,9 +16,11 @@ class EditorHandler(IPythonHandler):
         if not self.contents_manager.file_exists(path):
             raise web.HTTPError(404, u'File does not exist: %s' % path)
 
+        basename = path.rsplit('/', 1)[-1]
         self.write(self.render_template('texteditor.html',
             file_path=url_escape(path),
-            page_title=path.rsplit('/', 1)[-1] + " (editing)",
+            basename=basename,
+            page_title=basename + " (editing)",
             )
         )