diff --git a/_drafts/idris-testing.md b/_drafts/idris-testing.md
index 58325145..104bceed 100644
--- a/_drafts/idris-testing.md
+++ b/_drafts/idris-testing.md
@@ -42,7 +42,7 @@ axiom3 : (x : PNat) -> (N x) = O -> Void
 axiom3 _ Refl impossible
 
 axiom4 : Nat -> Nat
-axiom4 x = if True then x else x
+axiom4 x = ?easdfasdf
 ```
 
 No path:
diff --git a/nonsite/deps/idris-runner/function/file-processing.js b/nonsite/deps/idris-runner/function/file-processing.js
index e99b97a6..00258bcb 100644
--- a/nonsite/deps/idris-runner/function/file-processing.js
+++ b/nonsite/deps/idris-runner/function/file-processing.js
@@ -23,6 +23,16 @@ function processUploads(uploads, tmpdir, command, callback) {
             idrisCommand = `${command.file}`;
             replCommand = `:t ${command.expr}`;
         }
+    } else if (command.action == "addclause") {
+        if(command.file !== undefined && command.f !== undefined && command.n !== undefined) {
+            idrisCommand = `${command.file}`;
+            replCommand = `:ac ${command.n} ${command.f}`;
+        }
+    } else if (command.action == "casesplit") {
+        if(command.file !== undefined && command.x !== undefined && command.n !== undefined) {
+            idrisCommand = `${command.file}`;
+            replCommand = `:cs ${command.n} ${command.x}`;
+        }
     }
 
     if(idrisCommand === null) {
@@ -39,9 +49,28 @@ function processUploads(uploads, tmpdir, command, callback) {
     exec(cmd, function(error, stdout, stderr) {
         // command output is in stdout
         // res.status(200).send(stdout);
-        var res = {
-            idrisOutput: stdout
-        };
+        stdout = stdout.trim();
+        let numLines = stdout.split("\n").length;
+        
+        if(command.action == "addclause" && numLines == 1) {
+            var res = {
+                displayAction: "insert",
+                toInsert: stdout,
+                line: command.n
+            };
+        } else if(command.action == "casesplit") {
+            var res = {
+                displayAction: "replace",
+                toReplace: stdout,
+                line: command.n
+            };
+        } else {
+            var res = {
+                displayAction: "showtext",
+                text: stdout
+            };
+        }
+        
         callback(JSON.stringify(res));
     });
 
diff --git a/nonsite/deps/idris-runner/function/test_bad.idr b/nonsite/deps/idris-runner/function/test_bad.idr
index 8c86706e..4e41f6ff 100644
--- a/nonsite/deps/idris-runner/function/test_bad.idr
+++ b/nonsite/deps/idris-runner/function/test_bad.idr
@@ -1,7 +1,6 @@
 module Main
 
 test : List Nat -> List Nat
-test xs = map (\x => x + 3) xs
 
 test_main : List Nat
 test_main = test [4, 3, "cat"]
diff --git a/nonsite/deps/idris-runner/function/test_p.idr b/nonsite/deps/idris-runner/function/test_p.idr
index 0c894dfd..5d6bdeb3 100644
--- a/nonsite/deps/idris-runner/function/test_p.idr
+++ b/nonsite/deps/idris-runner/function/test_p.idr
@@ -3,8 +3,8 @@ module Main
 test : List Nat -> List Nat
 test xs = map (\x => x + 3) xs
 
-test_main : List Nat
-test_main = test [4, 3, 8]
+test_main : List Nat -> List Nat
+test_main xs = ?test_main_rhs
 
-main : IO ()
-main = putStrLn (show test_main)
\ No newline at end of file
+-- main : IO ()
+-- main = putStrLn (show test_main)
diff --git a/public/js/code-snippets.js b/public/js/code-snippets.js
index 0d4b59b9..2e8d651e 100644
--- a/public/js/code-snippets.js
+++ b/public/js/code-snippets.js
@@ -204,39 +204,98 @@ function playpen_get_lang(playpen) {
 
 
     function get_idris_token(editor) {
+        let sess = editor.getSession();
         let cursor = editor.getCursorPosition();
-        let token = editor.getSession().getTokenAt(cursor.row, cursor.column);
-        if(token.type == "entity.name.function.idris" 
-            || token.type == "support.constant.prelude.idris" 
-            || token.type == "support.type.prelude.idris" 
-            || token.type == "text" 
-            || token.type == "meta.parameter.named.idris"
-            || token.type == "meta.function.type-signature.idris"
-            || token.type == "constant.language.bottom.idris") {
-            return token.value.trim();
-        } else {
-            return null;
+        let line = sess.getLine(cursor.row);
+
+        function isLeftWord(c) {
+            return (65 <= c && c <= 90)     // A-Z
+                || (97 <= c && c <= 122)    // a-z
+                || (48 <= c && c <= 57)     // 0-9
+                || c == 95;                 // _
+        }
+        function isRightWord(c) {
+            return isLeftWord(c);
         }
+
+        // var start = Math.max(cursor.column - 1, 0);
+        var start = cursor.column;
+        while (start > 0 && isLeftWord(line.charCodeAt(start-1))) {
+            start--;
+        }
+
+        var endInc = cursor.column - 1;
+        while (endInc < line.length - 1 && isRightWord(line.charCodeAt(endInc+1))) {
+            endInc++;
+        }
+
+        let tok = line.substring(start, endInc + 1);
+        // alert(`"${tok}"`);
+
+        return tok;
+
+        // let token = editor.getSession().getTokenAt(cursor.row, cursor.column);
+        // if(token.type == "entity.name.function.idris" 
+        //     || token.type == "support.constant.prelude.idris" 
+        //     || token.type == "support.type.prelude.idris" 
+        //     || token.type == "text" 
+        //     || token.type == "meta.parameter.named.idris"
+        //     || token.type == "meta.function.type-signature.idris"
+        //     || token.type == "constant.language.bottom.idris") {
+        //     return token.value.trim();
+        // } else {
+        //     return null;
+        // }
     }
 
+//     var res = {
+//         displayAction: "showtext",
+//         text: stdout
+//     };
+// } else {
+//     var res = {
+//         displayAction: "insert",
+//         toInsert: stdout,
+//         line: command.n
+//     };
+
+    function handle_idris_result(code_block, result_block, editor, result) {
+        if(result == null || result.displayAction == null) {
+            result_block.innerText = "Communication error.";
+            return;
+        }
 
-    function handle_idris_result(code_block, result_block, result) {
-        if(result == null || result.idrisOutput == null || result.idrisOutput == "") {
-            // result_block.style.display = 'none';
-            result_block.innerText = 'No type errors.';
+        if(result.displayAction == "insert") {
+            let sess = editor.getSession();
+            sess.insert({row: result.line, column: 0}, result.toInsert);
+
+            result_block.style.display = 'none';
+        } else if(result.displayAction == "replace") {
+            let sess = editor.getSession();
+            let line = sess.getLine(result.line - 1);
+            let replaceRange = new ace.Range(result.line - 1, 0, result.line - 1, line.length);
+            sess.replace(replaceRange, result.toReplace);
+
+            result_block.style.display = 'none';
+        } else if(result.displayAction == "showtext") {
+            if(result.text == null || result.text == "") {
+                result_block.innerText = 'No type errors.';
+            } else {
+                result_block.innerText = result.text;
+            }
         } else {
-            result_block.innerText = result.idrisOutput;
+            result_block.innerText = "Unknown display action: " + result.displayAction;
         }
     }
 
-    function idris_action(code_block, editor, actionFn) {
+    function idris_action(code_block, editor, waiting_text, actionFn) {
         var result_block = get_result_block(code_block);
 
-        // result_block.style.display = 'block';
-        result_block.innerText = "Typechecking...";
+        result_block.style.display = 'block';
+        result_block.innerText = waiting_text;
 
         actionFn(code_block, editor)
-            .then(result => handle_idris_result(code_block, result_block, result))
+            .then(result => handle_idris_result(code_block, result_block, editor, result))
             .catch(error => result_block.innerText = "Playground Communication: " + error.message);
     }
 
@@ -269,6 +328,32 @@ function playpen_get_lang(playpen) {
         return run_idris_files(files, {action: "typeof", file: pkg.activeFilename, expr: token});
     }
 
+    function idris_add_def(block, editor) {
+        let pkg = package_idris_files(block);
+        let files = pkg.files;
+
+        let token = get_idris_token(editor);
+        if(token == null) {
+            return;
+        }
+
+        let lineNumber = editor.getCursorPosition().row + 1;
+        return run_idris_files(files, {action: "addclause", file: pkg.activeFilename, n: lineNumber, f: token});
+    }
+
+    function idris_case_split(block, editor) {
+        let pkg = package_idris_files(block);
+        let files = pkg.files;
+
+        let token = get_idris_token(editor);
+        if(token == null) {
+            return;
+        }
+
+        let lineNumber = editor.getCursorPosition().row + 1;
+        return run_idris_files(files, {action: "casesplit", file: pkg.activeFilename, n: lineNumber, x: token});
+    }
+
     
 
     
@@ -282,7 +367,7 @@ function playpen_get_lang(playpen) {
         var runFunc = language_dispatch_table[lang];
         if(lang == "language-idris") {
             let editor = get_editor(code_block);
-            idris_action(editor.container.parentNode, editor, idris_typecheck);  
+            idris_action(editor.container.parentNode, editor, "Typechecking...", idris_typecheck);  
         } else if(runFunc !== undefined) {
             runFunc(code_block)
                 .then(result => result_block.innerText = result)
@@ -297,8 +382,7 @@ function playpen_get_lang(playpen) {
             name: 'typecheck',
             bindKey: {win: 'Ctrl-Alt-R', mac: 'Ctrl-Alt-R'},
             exec: function(editor) {
-                idris_action(editor.container.parentNode, editor, idris_typecheck);
-                // idris_typecheck(editor.container.parentNode, editor);
+                idris_action(editor.container.parentNode, editor, "Typechecking...", idris_typecheck);
             },
             readOnly: true,
         });
@@ -307,11 +391,28 @@ function playpen_get_lang(playpen) {
             name: 'typeof',
             bindKey: {win: 'Ctrl-Alt-T', mac: 'Ctrl-Alt-T'},
             exec: function(editor) {
-                idris_action(editor.container.parentNode, editor, idris_typeof);
-                // idris_typeof(editor.container.parentNode, editor);
+                idris_action(editor.container.parentNode, editor, "Finding type...", idris_typeof);
             },
             readOnly: true,
         });
+
+        editor.commands.addCommand({
+            name: 'addclause',
+            bindKey: {win: 'Ctrl-Alt-A', mac: 'Ctrl-Alt-A'},
+            exec: function(editor) {
+                idris_action(editor.container.parentNode, editor, "Adding clause...", idris_add_def);
+            },
+            readOnly: false,
+        });
+
+        editor.commands.addCommand({
+            name: 'casesplit',
+            bindKey: {win: 'Ctrl-Alt-C', mac: 'Ctrl-Alt-C'},
+            exec: function(editor) {
+                idris_action(editor.container.parentNode, editor, "Splitting case...", idris_case_split);
+            },
+            readOnly: false,
+        });
     }
 
     // Syntax highlighting Configuration