diff --git a/driver.html b/driver.html
index 1f374fbef0e98dad1b60d69ad9ca44a1461e6239..1f8e49db12b62fe93a174af13e0d5ce22f34d3a3 100644
--- a/driver.html
+++ b/driver.html
@@ -135,18 +135,19 @@ Reach condition:
 </div>
 
 <script src="tools.js"></script> 
+<script src="generator/tests/jsref/displayed_sources.js"></script> 
 <script src="generator/tests/jsref/lineof.js"></script> 
 <script src="generator/tests/jsref/assembly.js"></script> 
 <script src="navig-driver.js"></script> 
 
 
-<!--
+<!---
 <script language="javascript">
 $(function() {
 	$('.scroll-pane').jScrollPane();
 });
 </script>
--->
+--->
 
 <!--
 
@@ -166,19 +167,18 @@ $(function() {
 </html>
 
 
+<!--
+/*
+   $timeout(function() {codeMirror.refresh();});
 
-<!---
-$timeout(function() {codeMirror.refresh();});
-
-this.codeMirrorInstance.setValue(content);
-var that = this;
-setTimeout(function() {
-    that.codeMirrorInstance.refresh();
-},1);
-
-http://codemirror.net/demo/buffers.html
+   this.codeMirrorInstance.setValue(content);
+   var that = this;
+   setTimeout(function() {
+       that.codeMirrorInstance.refresh();
+   },1);
 
-//CodeMirror.Doc(text
+   http://codemirror.net/demo/buffers.html
+*/
 ---->
 
 
diff --git a/generator/Makefile b/generator/Makefile
index c263d08052829c53e476d4b598d82ba7f2007e36..58de204d76a2312697e278f115b613859bc66afd 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -59,9 +59,11 @@ ASSEMBLY_JS := $(STDLIB_DIR)/stdlib.js $(addprefix tests/jsref/,$(ASSEMBLY_JS_FI
 
 ###############################################################
 
-# --> todo arthur include src files
-#	JsPreliminary.log.js \
-#	JsInterpreter.log.js
+DISPLAYED_JS_FILES := \
+	JsPreliminary.unlog.js \
+	JsInterpreter.unlog.js
+
+DISPLAYED_JS := $(addprefix tests/jsref/,$(DISPLAYED_JS_FILES));
 
 
 ###############################################################
@@ -146,7 +148,13 @@ $(JSREF_PATH)/assembly.js: assembly.byte $(ASSEMBLY_JS)
 	./assembly.byte -o $@ $(ASSEMBLY_JS)
 # -stdlib $(STDLIB_DIR)/stdlib.js 
 
-# maybe useful
+##### Rule for displayed_sources.js
+
+$(JSREF_PATH)/displayed_sources.js: displayed_sources.byte $(DISPLAYED_JS)
+	./displayed_sources.byte -o $@ $(DISPLAYED_JS)
+
+
+#### maybe useful ??
 
 tests/jsref/%.log.js: tests/jsref/%.ml 
 
@@ -170,6 +178,8 @@ lineof: $(JSREF_PATH)/lineof.js
 
 assembly: $(JSREF_PATH)/assembly.js
 
+display: $(JSREF_PATH)/displayed_sources.js
+
 stdlib: $(STDLIB_DIR)/stdlib.cmi
 
 
diff --git a/generator/assembly.ml b/generator/assembly.ml
index 183fcaafa6190629413e386e63096d30c06a1c9f..da6b63d4e454668bac99163aa244cf1bae7d7cff 100644
--- a/generator/assembly.ml
+++ b/generator/assembly.ml
@@ -1,4 +1,5 @@
 
+
 (*#########################################################################*)
 
 (* Section COPIED FROM /home/charguer/pbench/xlib/XBase.ml *)
@@ -75,6 +76,14 @@ let hashtbl_keys t =
 (*#########################################################################*)
 
 
+
+(** DOCUMENTATION
+  
+    takes as argument a list of javascript filenames,
+    and catenate them into a target file.
+
+ *)
+
 let files = ref ([]:string list)
 let outputfile = ref None
 (*let stdlibfile = ref None*)
@@ -118,28 +127,6 @@ let _ =
     let puts lines =
        List.iter put lines in
 
-   (*---------------------------------------------------*)
-   (* include of the source code of logged unsource files *)
-
-   (* TODO *)
-
-   (*---------------------------------------------------*)
-   (* include of stdlib source *)
-
-(*
-   begin match !stdlibfile with
-   | None -> ()
-   | Some filename ->
-      let lines = XFile.get_lines filename in
-      put "\n/* --------------------- stdlib --------------------- */\n";
-      puts lines;
-   end;
-*)
-
-(*  LATER, for escaping sources
-        if Filename.check_suffix filename ".log.js" 
-*)
-
    (*---------------------------------------------------*)
    (* include of logged js files *)
 
diff --git a/generator/displayed_sources.ml b/generator/displayed_sources.ml
new file mode 100644
index 0000000000000000000000000000000000000000..cb84bb16842a3daca4473e5e9d273da3752ca94f
--- /dev/null
+++ b/generator/displayed_sources.ml
@@ -0,0 +1,170 @@
+
+(*#########################################################################*)
+
+(* Section COPIED FROM /home/charguer/pbench/xlib/XBase.ml *)
+
+(** A generic operator for swapping the order of the two first arguments 
+    of a function *)
+
+let ( ~~ ) = fun f x y -> f y x 
+
+module XBase = struct
+  exception Break
+end
+
+(* Section COPIED FROM /home/charguer/pbench/xlib/XList.ml *)
+
+module XList = struct
+
+  let rev_not_rec l =
+     let res = ref [] in
+     let cur = ref l in
+     begin try while true do
+        match !cur with
+        | [] -> raise XBase.Break
+        | x::xs ->
+           res := x::!res;
+           cur := xs
+     done with XBase.Break -> () end;
+     !res
+end
+
+
+(* Section COPIED FROM /home/charguer/pbench/xlib/XFile.ml *)
+
+module XFile = struct
+
+  (** Write the string [str] into a file of given name *)
+
+  let put_contents filename str =
+    let channel = open_out filename in
+    output_string channel str;
+    close_out channel    
+
+  (** Write a list of lines into a file of given name *)
+
+  let put_lines filename ?(sep="\n") lines =
+     put_contents filename (String.concat sep (lines @ [""]))
+
+  (** Read the lines of a file; raise FileNotFound if no such file *)
+
+  exception FileNotFound of string
+
+  let get_lines file = 
+     if not (Sys.file_exists file)
+        then raise (FileNotFound file);
+     let lines = ref [] in
+     let f = 
+        try open_in file with End_of_file -> raise (FileNotFound file);
+        in
+     begin try while true do
+        lines := input_line f :: !lines 
+     done with End_of_file -> () end;
+     close_in f;
+     XList.rev_not_rec !lines
+
+
+end
+
+(* Extra *)
+
+let hashtbl_keys t =
+  Hashtbl.fold (fun key value acc -> key::acc) t []
+
+
+(*#########################################################################*)
+
+
+(** DOCUMENTATION
+  
+    takes as argument a list of javascript filenames,
+    and create a javascript file with a definition of
+    an array called "tracer_files", storing objects with
+    two fields: a filename, and a contents, with newline
+    and quotes properly escaped.
+
+
+   var tracer_files = [
+      { 
+         file: 'calc.js', 
+         contents: 'var Stack = {\n  is_empty: function (s) {\n    return s === {type: "N"};\n  },\n\n  push: function (x, stack) {\n    return {type: "C", value: x, stack: stack};\n  },\n\n ;\n};\n'
+      }
+   ];
+
+ *)
+
+
+
+
+
+let files = ref ([]:string list)
+let outputfile = ref None
+(*let stdlibfile = ref None*)
+
+(* TODO: might be useful to take "basename" from the command line *)
+
+let _ =
+   (*---------------------------------------------------*)
+   (* parsing of command line *)
+
+   let files = ref [] in
+   Arg.parse
+     [ (* ("-I", Arg.String (fun i -> Clflags.include_dirs := i :: !Clflags.include_dirs),
+                      "includes a directory where to look for interface files"); *)
+       (* ("-stdlib", Arg.String (fun s -> stdlibfile := Some s), "set the stdlib file name"); *)
+       ("-o", Arg.String (fun s -> outputfile := Some s), "set the output file name");
+       (* ("-debug", Arg.Set debug, "trace the various steps"); *)
+       (* ("-mode", Arg.String (fun s -> set_current_mode s), "current mode: unlog, log, or token")*)
+     ]
+     (fun f -> files := f :: !files)
+     ("usage: [..other options..] -o sources.js file1.js file2.js ...");
+     (* -stdlib file.js *)
+   if !files = [] then
+     failwith "No input file provided";
+   files := List.rev !files;
+   let input_filename1 = List.hd !files in
+   let dirname = Filename.dirname input_filename1 in
+   let output_filename = 
+     match !outputfile with
+     | None -> Filename.concat dirname "displayed_sources.js"
+     | Some f -> f
+   in
+
+   (*---------------------------------------------------*)
+   (* open output file for writing *)
+
+    let outchannel = open_out output_filename in
+    let put_no_endline str =
+       output_string outchannel str in
+    let put str =
+       output_string outchannel str;
+       output_string outchannel "\n" in
+
+
+   (*---------------------------------------------------*)
+   (* include of logged js files *)
+
+   put "var tracer_files = [";
+
+   ~~ List.iter !files (fun filename ->
+      let lines = XFile.get_lines filename in
+      let short_filename = Filename.chop_suffix (Filename.basename filename) ".unlog.js" in
+      put (Printf.sprintf "\n/* --------------------- %s --------------------- */" short_filename);
+      put_no_endline (Printf.sprintf "  { file: '%s', contents: '" short_filename);
+      ~~ List.iter lines (fun line ->
+         let line = Str.global_replace (Str.regexp "'") "\\'" line in
+         put_no_endline line;
+         put_no_endline "\\n";
+      );
+      put "'},";
+      );
+
+   put "];";
+
+   (*---------------------------------------------------*)
+   (* generating output file *)
+
+   close_out outchannel;
+   Printf.printf "Wrote file: %s\n" output_filename;
+
+
diff --git a/generator/lineof.ml b/generator/lineof.ml
index 3a9b947cb4326159e22f6a41ffdbe7a0d63a0625..2c9fb3dbc8277d213f694badecbcf1833f454ec1 100644
--- a/generator/lineof.ml
+++ b/generator/lineof.ml
@@ -159,7 +159,7 @@ let generate_lineof_function put =
                key pos_start.pos_line pos_start.pos_col  
                    pos_stop.pos_line  pos_stop.pos_col);
      );
-     put (Printf.sprintf "lineof_data[\"%s\"] = lineof_temp;" filename);
+     put (Printf.sprintf "lineof_data[\"%s\"] = lineof_temp;" basename);
   )
  
 
diff --git a/navig-driver.js b/navig-driver.js
index 16158ae8f0205dd2d87da2dec51b0a784e6238da..53ac4c04311853b727960f9fb8faabf28431e12e 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -68,12 +68,14 @@ var tracer_length = 0;
 var tracer_pos = 0;
 
 // Core Mirror objects
-var source = null;
+var source = "";
 var interpreter = null;
 
+
 // --------------- Initialization ----------------
 
-// file displayed initially
+// WARNING: do not move this initialization further down in the file
+// source code displayed initially
 $("#source_code").val(source_file);
 
 
@@ -250,14 +252,18 @@ function finish() { shared_next(+1, -1); }
 // load files in CodeMirror view
 var docs = {};
 for (var i = 0; i < tracer_files.length; i++) {
- var file = tracer_files[i].file;
- var txt = tracer_files[i].contents;
- docs[file] = CodeMirror.Doc(txt, 'js');
+  var file = tracer_files[i].file;
+  var txt = tracer_files[i].contents;
+  docs[file] = CodeMirror.Doc(txt, 'js');
 }
 
 function viewFile(file) {
  if (curfile !== file) {
    curfile = file;
+   if (docs[curfile] == undefined) {
+     console.log("Cannot view file " + curfile);
+     return;
+   }
    interpreter.swapDoc(docs[curfile]);
    interpreter.focus();
    updateFileList();
@@ -355,12 +361,12 @@ function updateContext(targetid, heap, env) {
 
 // --------------- Selection view ----------------
 
-function updateSelection(codeMirrorObj, loc) {
+function updateSelectionInCodeMirror(codeMirrorObj, loc) {
  if (loc === undefined) {
    return; 
  }
- var anchor = {line: loc.start.line-1 , ch: loc.start.column };
- var head = {line: loc.stop.line-1, ch: loc.stop.column };
+ var anchor = {line: loc.start.line-1 , ch: loc.start.col };
+ var head = {line: loc.stop.line-1, ch: loc.stop.col };
  codeMirrorObj.setSelection(anchor, head);
 }
 
@@ -371,30 +377,33 @@ function updateSelection() {
  if (item !== undefined) {
    // console.log(item);
    // $("#disp_infos").html();
-   if (item.line === undefined)
-     alert("missing line in log event");
+   if (item.source_loc === undefined) {
+     console.log("Error: missing line in log event");
+
+   } else {
 
-   // source panel
-   source_loc_selected = item.source_loc;
-   updateSelection(source, source_loc_selected);
-   // console.log(source_loc_selected);
+     // source panel
+     source_loc_selected = item.source_loc;
+     updateSelectionInCodeMirror(source, source_loc_selected);
+     // console.log(source_loc_selected);
 
-   // source heap/env panel
-   updateContext("#disp_env", item.heap, item.env);
+     // source heap/env panel
+     updateContext("#disp_env", item.heap, item.env);
 
-   // interpreter ctx panel
-   updateContext("#disp_ctx", item.heap, item.ctx);
+     // interpreter ctx panel
+     updateContext("#disp_ctx", item.heap, item.ctx);
 
-   // interpreter code panel
-   viewFile(item.file);
-   //console.log("pos: " + tracer_pos);
+     // interpreter code panel
+     viewFile(item.loc.file);
+     //console.log("pos: " + tracer_pos);
 
-   var color = '#F3F781';
-      // possible to use different colors depending on event type
-      // var color = (item.type === 'enter') ? '#F3F781' : '#CCCCCC';
-   $('.CodeMirror-selected').css({ background: color });
-   $('.CodeMirror-focused .CodeMirror-selected').css({ background: color });
-   updateSelection(interpreter, item.loc);
+     var color = '#F3F781';
+        // possible to use different colors depending on event type
+        // var color = (item.type === 'enter') ? '#F3F781' : '#CCCCCC';
+     $('.CodeMirror-selected').css({ background: color });
+     $('.CodeMirror-focused .CodeMirror-selected').css({ background: color });
+     updateSelectionInCodeMirror(interpreter, item.loc);
+   }
 
    // navig panel
    $("#navigation_step").val(tracer_pos);
@@ -456,32 +465,35 @@ interpreter.focus();
 
 // --------------- Main run method ----------------
 
-function assignSourceLocInTrace(items) {
- var last = undefined;
+// Functions run_prog, run_expr and run_stat have a last argument
+// called "_term_"; we try to find items in the trace that correspond
+// to the binding of this argument in the context, so as to extract
+// the corresponding location from the piece of AST that corresponds.
+// These locations are used for source highlighting.
+function assignSourceLocInTrace() {
+ var last = { start: { line: 1, col: 0}, stop: { line: 1, col: 0 } };
  for (var k = 0; k < tracer_items.length; k++) {
    var item = tracer_items[k];
-   item.source_loc = last;
-   if (item.ctx !== undefined) {
-     var ctx_as_array = array_of_env(item.ctx);
-     // only considers _term_ as top of ctx
-     if (ctx_as_array.length > 0 && ctx_as_array[0].key === "_term_") {
-       var t = ctx_as_array[0].val;
-       if (! (t === undefined || t.loc === undefined)) {
-         item.source_loc = t.loc;
-         // t.loc = {start : int, end : int}
-         last = t;
+   if (item.ctx !== undefined && item.ctx.bindings !== undefined) {
+     var bindings = item.ctx.bindings;
+     var binding = bindings[bindings.length-1];
+     if (binding !== undefined && binding.key === "_term_") {
+       var t = binding.val;
+       if (t.loc != undefined) {
+         last = t.loc;
        }
      }
    }
+   item.source_loc = last;
  }
 }
 
 function run() {
-  // TODO:parse
+ reset_datalog();
  JsInterpreter.run_javascript(JsInterpreter.runs, program);
- assignSourceLocInTrace(datalog);
  tracer_items = datalog;
  tracer_length = tracer_items.length;
+ assignSourceLocInTrace();
  $("#navigation_total").html(tracer_length - 1);
  stepTo(0); // calls updateSelection(); 
 }
@@ -498,6 +510,18 @@ function readSourceParseAndRun() {
    run();
 }
 
+
+// --------------- Initialization, continuted ----------------
+
+
+// interpreter file displayed initially
+viewFile(tracer_files[0].file);
+
+//$timeout(function() {codeMirror.refresh();});
+
+
+
+
 // -------------- Testing ----------------
 
 // usage: testParse("var x = 3");
diff --git a/tools.js b/tools.js
index 726e001ae76f6bd4d3fb4601ecaf74426b4766eb..c87b9d36be3ea18b6987898bfe02b4c5afd9dee2 100644
--- a/tools.js
+++ b/tools.js
@@ -14,6 +14,10 @@ function lineof(filename, token) {
 
 var datalog = [];
 
+function reset_datalog() {
+  datalog = [];
+}
+
 function log_event(loc, ctx, type) {
   // TODO populate state with object_heap, env_record_heap, fresh_locations, and populate env
   var event = {loc : loc, ctx : ctx, type : type, state: {}, env: {}};