From 030a836954800805f1a58808207a265d3be38383 Mon Sep 17 00:00:00 2001
From: Jan Wielemaker <J.Wielemaker@cs.vu.nl>
Date: Sun, 5 Jul 2015 13:53:00 +0200
Subject: [PATCH] Notebook activation makes first active or program the current
 source.

---
 web/js/editor.js   |  4 +++-
 web/js/notebook.js | 18 ++++++++++++++++++
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/web/js/editor.js b/web/js/editor.js
index 092377f05..6b690b4f5 100644
--- a/web/js/editor.js
+++ b/web/js/editor.js
@@ -55,6 +55,7 @@ define([ "cm/lib/codemirror",
       role: "source",
       placeholder: "Your Prolog rules and facts go here ...",
       lineNumbers: true,
+      autoCurrent: true,
       save: false,
       theme: "prolog",
       matchBrackets: true,
@@ -192,7 +193,8 @@ define([ "cm/lib/codemirror",
 
 	if ( options.mode == "prolog" && data.role == "source" ) {
 	  elem.on("activate-tab", function(ev) {
-	    elem.prologEditor('makeCurrent');
+	    if ( options.autoCurrent )
+	      elem.prologEditor('makeCurrent');
 	    data.cm.refresh();		/* needed if a tab has been opened */
 	  });
 
diff --git a/web/js/notebook.js b/web/js/notebook.js
index b2dab3da4..ac1e980c6 100644
--- a/web/js/notebook.js
+++ b/web/js/notebook.js
@@ -88,6 +88,23 @@ var cellTypes = {
 	  }
 	});
 
+	/* Activate the active source or first source.  If the active
+	 * cell is a query, we could activate the source of the query?
+	 */
+	elem.on("activate-tab", function(ev) {
+	  if ( ev.target == elem[0] ) {
+	    var eds = elem.find(".nb-content")
+                          .children(".nb-cell.program");
+	    var aeds = eds.filter(".active");
+	    var nc = aeds[0]||eds[0];
+
+	    if ( nc ) {
+	      $(nc).find(".prolog-editor").prologEditor('makeCurrent');
+	    }
+	    ev.stopPropagation();
+	  }
+	});
+
 	elem.data(pluginName, data);	/* store with element */
 
 					/* restore content */
@@ -640,6 +657,7 @@ var cellTypes = {
     var editor;
 
     options = options||{};
+    options.autoCurrent = false;
 
     this.html("");
     this.append(editor=$.el.div({class:"editor"}));