feat(emacs/lean-dev): add lean-diff-test-file command for development

doc/fixing_tests.md

@@ -30,6 +30,8 @@ When the `yes` option is provided, `meld` is automatically invoked
 whenever there is discrepancy between the produced and expected
 outputs. `meld` can also be used to repair the problems.
 
+In Emacs, we can also execute `M-x lean-diff-test-file` to check/diff the file of the current buffer.
+
 Here is the list of directories where produced output is compared with
 the expected output (stored in a `*.expected.out` file).
 
@@ -37,5 +39,5 @@ the expected output (stored in a `*.expected.out` file).
 - [`tests/lean/interactive`](../tests/lean/interactive)
 
 Remark: in the directory `tests/lean/interactive`, the input test files have extension `.input`.
-They simulate commands sent from Emacs to Lean.
-The `.lean` files in this directory are used to simulate files opened by the user.
+They simulate commands sent from editors to Lean.
+The `.lean` files in this directory are used to simulate files opened by the user.

src/emacs/lean-dev.el

@@ -0,0 +1,16 @@
+;;  -*- lexical-binding: t -*-
+;;
+;; Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+;; Author: Sebastian Ullrich
+;;
+
+(defun lean-diff-test-file ()
+  "Use interactive ./test_input.sh on file of current buffer"
+  (interactive)
+  (message (shell-command-to-string (format "./test_single.sh \"%s\" \"%s\" yes"
+                                            (lean-get-executable "lean")
+                                            (buffer-name)))))
+
+(provide 'lean-dev)

src/emacs/lean-mode.el

@@ -33,6 +33,7 @@
 (require 'lean-type)
 (require 'lean-message-boxes)
 (require 'lean-right-click)
+(require 'lean-dev)
 
 (defun lean-compile-string (exe-name args file-name)
   "Concatenate exe-name, args, and file-name"