Applied Twitter Bootstrap layout

src/frontend/css/editor.css

@@ -1,147 +1,65 @@
-html {
-    background-color: #ccddef;
-    margin: 0;
-    padding: 0;
-}
-
 body {
-    margin: 0;
-    padding: 20px;
-    font: 16px/24px Verdana, Arial, sans;
+    padding-top: 40px;
+    background-color: #f9f9f9;
 }
 
-#loader {
-    background: url(/static/img/load.gif) no-repeat scroll 0 0 transparent;
-    height: 31px;
-    width: 31px;
+.alert {
     display: none;
-    position: absolute;
-    margin-top: -5px;
-    margin-left: 16px;
-}
-
-.panel {
-    background-color: #fff;
-    border: 3px solid #bbb;
-    cursor: text;
-    min-height: 400px;
-    padding-bottom: 10px;
-    position: absolute;
-    top: 58px;
-    width: 47%;
-}
-
-#error {
-    /*display: none;*/
-    font-size: 12px;
-    clear: both;
-    margin-top: 20px;
-    position: absolute;
+    margin: 10px 0 0;
 }
-
-#input {
-    float: left;
-    left: 2%;
-}
-
-#input textarea {
-    width: 100%;
-    border: 0;
-    margin: 0;
-    padding: 0;
-    height: 388px;
-    overflow-y: visible;
-    font: 16px/24px Verdana, Arial, sans;
-    outline: 0;
-}
-
-.box {
-    padding: 10px 15px 0 15px;
-}
-
-#math {
-    float:right;
-    right: 2%;
+.alert strong {
+    margin-right: 8px;
 }
 
-#math .box {
-    padding: 10px 15px 0 40px;
-    background: no-repeat scroll 15px 13px transparent;
+.math-input {
+    width: 436px !important;
+    min-height: 314px;
+    padding: 7px 11px;
+    line-height: 26px;
+    overflow: hidden;
 }
 
-#math .box.correct {
-    background-image: url(/static/img/tick.png);
-}
-
-#math .box.wrong {
-    background-image: url(/static/img/cross.png);
-}
-
-#math .box.no-progress {
-    background-image: url(/static/img/error.png);
-}
-
-#math .hint {
-    padding: 10px 15px 0 40px;
-    background: url(/static/img/info.png) no-repeat scroll 15px 13px transparent;
-    color: #666;
-    font-size: 14px;
-    line-height: 20px;
+.pretty-print {
+    background-color: #fff;
+    border-color: #ccc;
+    min-height: 300px;
+    padding: 14px 19px;
 }
 
-#math .hint .MathJax {
-    color: #000;
+.box, .hint {
+    position: relative;
+    margin: 5px 0;
+    padding-left: 20px;
 }
 
-#control-buttons {
-    height: 21px;
-    left: 2%;
-    line-height: 0;
-    margin-bottom: 16px;
+.label, .icon {
     position: absolute;
-    vertical-align: top;
+    top: 50%;
 }
-
-.separator {
-    border-right: 1px solid #999;
-    display: inline-block;
-    width: 0;
-    height: 21px;
-    margin: 1px 5px;
-    vertical-align: top;
+.label {
+    margin-top: -9px;
+    left: -8px;
 }
-
-.panel .label {
-    background-color: #fff;
-    border: 1px solid #ccc;
-    clear: both;
-    float: left;
-    font-size: 10px;
-    line-height: 14px;
-    margin-left: 4px;
-    margin-top: -12px;
-    padding: 2px;
+.icon {
+    margin-top: -8px;
+    left: 0;
 }
 
-/* Codemirror should not resize the input area. */
-/*
-.CodeMirror-scroll {
-    height: auto;
-    overflow: visible;
+.current-line {
+    border-right: 3px solid #ddd;
 }
 
-.CodeMirror-lines {
-    padding: 0 !important;
+.credits {
+    text-align: center;
 }
-*/
 
-#credits {
-    clear both;
-    left: 0;
-    right: 0;
-    bottom: 0;
-    position: fixed;
-    font-size: 10px;
-    color: #666;
-    text-align: center;
+#loader {
+    display: inline-block;
+    visibility: hidden;
+    position: relative;
+    background: url(/static/img/load.gif) no-repeat;
+    height: 16px;
+    width: 16px;
+    top: 8px;
+    margin-left: 10px;
 }

src/frontend/js/editor.js

@@ -1,21 +1,90 @@
-(function ($) {
+(function($, undefined) {
+    // http://stackoverflow.com/questions/1891444/how-can-i-get-cursor-position-in-a-textarea
+    $.fn.getCursorPosition = function() {
+        var el = $(this).get(0);
+        var pos = 0;
+
+        if ('selectionStart' in el) {
+            pos = el.selectionStart;
+        } else if ('selection' in document) {
+            el.focus();
+            var Sel = document.selection.createRange();
+            var SelLength = document.selection.createRange().text.length;
+            Sel.moveStart('character', -el.value.length);
+            pos = Sel.text.length - SelLength;
+        }
+
+        return pos;
+    };
+
     var QUEUE = MathJax.Hub.queue;  // shorthand for the queue
     var math = null; // the element jax for the math output
 
     var trigger_update = true;
-    var input_textarea = $('#MathInput');
+    var input_textarea = $('#math-input');
+    var pretty_print = $('#pretty-print');
 
     // Set the requested query as input value if a query string is given.
     if (location.search.substr(0, 3) == '?q=')
         input_textarea.val(decodeURIComponent(location.search.substr(3)));
 
-    input_textarea.change(function(){ trigger_update = true; })
-        .keyup(function(){ trigger_update = true; });
+    input_textarea.bind('change keyup click', function() {
+        trigger_update = true;
+    });
 
-    $('#input').click(function(){
+    input_textarea.closest('div').click(function() {
         input_textarea.focus();
     });
 
+    var STATUS_FAILURE = 0,
+        STATUS_NOPROGRESS = 1,
+        STATUS_SUCCESS = 2,
+        STATUS_ERROR = 3;
+
+    var status_icons = ['thumbs-down', 'thumbs-up', 'thumbs-up', 'remove'];
+    var status_labels = ['important', 'warning', 'success', 'important'];
+    var status_titles = ['Incorrect', 'No progress', 'Correct', 'Error'];
+    var status_messages = [
+        'This step is incorrect.',
+        'This step leads to the correct answer, but not in a lower number of '
+        + 'steps than the previous step.',
+        'This step is correct.',
+        'An error occurred while validating this step.'
+    ];
+
+    function set_status(elem, stat) {
+        elem = $(elem);
+        elem.find('.label').remove();
+
+        if (stat !== undefined) {
+            var label = $('<span class="label label-'
+                          + status_labels[stat] + '"/>');
+            label.append('<i class="icon-white icon-'
+                         + status_icons[stat] + '"/>');
+            //label.tooltip({placement: 'left', title: status_messages[stat]});
+            label.popover({
+                placement: 'left',
+                trigger: 'hover',
+                title: status_titles[stat],
+                content: status_messages[stat]
+            });
+            elem.append(label);
+        }
+    }
+
+    function get_current_line() {
+        var input = input_textarea.val(),
+            caret = input_textarea.getCursorPosition(),
+            lines = 0;
+
+        for (var i = 0; i < caret; i++) {
+            if (input.charAt(i) == '\n')
+                lines++;
+        }
+
+        return lines;
+    }
+
     // Get the element jax when MathJax has produced it.
     QUEUE.Push(function() {
         // The onchange event handler that typesets the math entered
@@ -23,13 +92,14 @@
         // so we don't see a flash as the math is cleared and replaced.
         var update_math = function(tex) {
             var parts = tex.split('\n');
+            var math_lines = pretty_print.find('div.box script');
 
-            var math_container = $('#math'),
-                math_lines = math_container.find('div.box script');
+            // Stretch textarea size with number of input lines
+            input_textarea.attr('rows', parts.length);
 
             // Select all mathjax instances which are inside a div.box element
             var mathjax_instances = [];
-            var all_instances = MathJax.Hub.getAllJax('math');
+            var all_instances = MathJax.Hub.getAllJax('pretty-print');
 
             for (var i = 0; i < all_instances.length; i++) {
                 var elem = all_instances[i];
@@ -39,7 +109,8 @@
             }
 
             var real_lines = 0,
-                updated_line = -1;
+                updated_line = -1,
+                current_line = get_current_line();
 
             for (var p = 0; p < parts.length; p++) {
                 if (!parts[p])
@@ -56,22 +127,26 @@
                         QUEUE.Push(['Text', elem, parts[p]]);
                     }
 
+                    elem = $(math_lines[real_lines]).parent();
+
                     if (updated_line > -1) {
                         // Remove the out-of-date status information. This will
                         // be done from now on for all remaining lines, whether
                         // they are up-to-date or not.
-                        $(math_lines[real_lines]).parent()
-                            .removeClass('wrong').removeClass('correct');
+                        set_status(elem);
                     }
                 } else {
                     var line = '`' + parts[p] + '`',
                         elem = $('<div class="box"/>').text(line);
 
-                    math_container.append(elem);
+                    pretty_print.append(elem);
 
                     QUEUE.Push(['Typeset', MathJax.Hub, elem[0]]);
                 }
 
+                // Highlight current line.
+                $(elem).toggleClass('current-line', p == current_line);
+
                 real_lines++;
             }
 
@@ -85,7 +160,7 @@
                 // and remove all following hint nodes.  Note that if there is
                 // no line updated, all hints not directly following the last
                 // line are removed.
-                var elems = $('#math div');
+                var elems = pretty_print.find('div');
 
                 if(updated_line == -1)
                     updated_line = real_lines;
@@ -112,21 +187,25 @@
                 var input = input_textarea.val();
 
                 // Make sure that xx is not displayed as a cross.
-                while(/xx/.test(input))
-                    input = input.replace(/xx/, 'x x');
+                input = input.replace(/xx/g, 'x x');
 
                 update_math(input);
             }
         };
 
+        window.update_math();
         setInterval(window.update_math, 100);
     });
 
-    var loader = $('#loader');
+    var error = $('#error'),
+        loader = $('#loader');
+
+    error.find('.close').click(function() {
+        error.hide();
+    });
 
-    window.report_error = function(e) {
-        $('.panel').css({top: 74});
-        $('#error').text('error: ' + e.error).show();
+    function report_error(e) {
+        error.show().find('.text').text(e.error);
 
         if (console && console.log)
             console.log('error:', e);
@@ -134,95 +213,77 @@
         loader.hide();
     };
 
-    window.clear_error = function() {
-        $('#error').hide();
-        $('.panel').css({top: 58});
+    function clear_error() {
+        error.hide();
     };
 
-    window.show_loader = function() {
-        loader.show().css('display', 'inline-block');
+    function show_loader() {
+        loader.css('visibility', 'visible');
     };
 
-    window.hide_loader = function() {
-        loader.hide();
+    function hide_loader() {
+        loader.css('visibility', 'hidden');
         clear_error();
     };
 
-    window.append_hint = function(hint) {
-        $('#math div').last().filter('.hint').remove();
+    function append_hint(hint) {
+        pretty_print.find('div').last().filter('.hint').remove();
 
-        var elem = $('<div class=hint/>');
+        var elem = $('<div class="hint"/>');
         elem.text(hint);
-        $('#math').append(elem);
+        elem.append('<div class="icon icon-info-sign"/>');
+        pretty_print.append(elem);
         QUEUE.Push(['Typeset', MathJax.Hub, elem[0]]);
     };
 
-    window.append_input = function(input) {
+    function append_input(input) {
         input_textarea.val(input_textarea.val() + '\n' + input);
     };
 
-    window.answer_input = function() {
-        show_loader();
-
-        // TODO: disable input box and enable it when this ajax request is done
-        // (on failure and success).
-        $.post('/answer', {data: input_textarea.val()}, function(response) {
-            if (!response)
-                return;
-
-            if ('error' in response)
-                return report_error(response);
-
-            if ('steps' in response) {
-                for(i = 0; i < response.steps.length; i++) {
-                    cur = response.steps[i];
-
-                    if ('step' in cur)
-                        window.append_input(cur.step);
-
-                    if('hint' in cur)
-                        window.append_hint(cur.hint);
-
-                    trigger_update = true;
-                    window.update_math();
-                }
-            }
-
-            if('hint' in response)
-                window.append_hint(response.hint);
+    $('#btn-clear').click(function() {
+        input_textarea.val('');
+        pretty_print.find('.box,.hint').remove();
+        trigger_update = true;
+        clear_error();
+        hide_loader();
+    });
 
-            input_textarea.focus();
+    $('#btn-hint').click(function() {
+        var input = input_textarea.val();
 
-            hide_loader();
-        }, 'json').error(report_error);
-    };
+        if (!$.trim(input).length)
+            return;
 
-    window.hint_input = function() {
         show_loader();
 
         // TODO: disable input box and enable it when this ajax request is done
         // (on failure and success).
-        $.post('/hint', {data: input_textarea.val()}, function(response) {
+        $.post('/hint', {data: input}, function(response) {
             if (!response)
                 return;
 
             if ('error' in response)
                 return report_error(response);
 
-            window.append_hint(response.hint);
+            append_hint(response.hint);
 
             input_textarea.focus();
 
             hide_loader();
         }, 'json').error(report_error);
-    };
+    });
+
+    $('#btn-step').click(function() {
+        var input = input_textarea.val();
+
+        if (!$.trim(input).length)
+            return;
 
-    window.step_input = function() {
         show_loader();
 
         // TODO: disable input box and enable it when this ajax request is done
         // (on failure and success).
-        $.post('/step', {data: input_textarea.val()}, function(response) {
+        $.post('/step', {data: input}, function(response) {
             if (!response)
                 return;
 
@@ -230,75 +291,103 @@
                 return report_error(response);
 
             if ('step' in response) {
-                window.append_input(response.step);
+                append_input(response.step);
                 trigger_update = true;
             }
 
             if('hint' in response)
-                window.append_hint(response.hint);
+                append_hint(response.hint);
 
             input_textarea.focus();
 
             hide_loader();
         }, 'json').error(report_error);
-    };
+    });
+
+    $('#btn-validate').click(function() {
+        var input = input_textarea.val();
+
+        if (!$.trim(input).length)
+            return;
 
-    window.validate_input = function() {
         show_loader();
 
         // TODO: disable input box and enable it when this ajax request is done
         // (on failure and success).
-        $.post('/validate', {data: input_textarea.val()}, function(response) {
+        $.post('/validate', {data: input}, function(response) {
             if (!response)
                 return;
 
             if ('error' in response)
                 return report_error(response);
 
-            var math_container = $('#math'),
-                math_lines = math_container.find('div.box');
-
+            var math_lines = pretty_print.find('div.box');
             var i = 0;
 
             // Remove the status indicator from all remaining lines.
-            for(; i < math_lines.length; i++) {
-                $(math_lines[i])
-                    .removeClass('correct')
-                    .removeClass('wrong')
-                    .removeClass('no-progress');
-            }
+            for(; i < math_lines.length; i++)
+                set_status(math_lines[i]);
 
             i = 0;
 
             // Check if the first line has a correct syntax, since there is
             // nothing to validate here.
             if (i < math_lines.length && i <= response.validated) {
-                $(math_lines[i]).addClass('correct');
+                set_status(math_lines[i], STATUS_SUCCESS);
                 i++;
             }
 
-            var status_classes = ['wrong', 'no-progress', 'correct', 'error'];
-
             // Mark every line as {wrong,no-progress,correct,error}.
-            for (; i < math_lines.length && i <= response.validated; i++) {
-                var status_class = status_classes[response.status[i - 1]];
-                $(math_lines[i]).addClass(status_class);
-            }
+            for (; i < math_lines.length && i <= response.validated; i++)
+                set_status(math_lines[i], response.status[i - 1]);
 
             if (i < math_lines.length) {
                 // Mark the current line as wrong.
-                $(math_lines[i]).addClass('wrong');
+                set_status(math_lines[i], STATUS_FAILURE);
             }
 
             hide_loader();
         }, 'json').error(report_error);
-    };
+    });
 
-    window.clear_input = function() {
-        input_textarea.val('');
-        $('#math .box,#math .hint').remove();
-        trigger_update = true;
-        clear_error();
-        hide_loader();
-    };
+    $('#btn-answer').click(function() {
+        var input = input_textarea.val();
+
+        if (!$.trim(input).length)
+            return;
+
+        show_loader();
+
+        // TODO: disable input box and enable it when this ajax request is done
+        // (on failure and success).
+        $.post('/answer', {data: input}, function(response) {
+            if (!response)
+                return;
+
+            if ('error' in response)
+                return report_error(response);
+
+            if ('steps' in response) {
+                for(i = 0; i < response.steps.length; i++) {
+                    cur = response.steps[i];
+
+                    if ('step' in cur)
+                        append_input(cur.step);
+
+                    if('hint' in cur)
+                        append_hint(cur.hint);
+
+                    trigger_update = true;
+                    window.update_math();
+                }
+            }
+
+            if('hint' in response)
+                append_hint(response.hint);
+
+            input_textarea.focus();
+
+            hide_loader();
+        }, 'json').error(report_error);
+    });
 })(jQuery);

src/frontend/tpl/editor.html

@@ -3,33 +3,63 @@
     <head>
         <meta http-equiv="content-type" content="text/html; charset=utf-8">
         <title>Mathematical term rewriting frontend</title>
-        <script type="text/javascript" src="/static/js/jquery-1.8.2.min.js"></script>
-        <script type="text/javascript"
-            src="/static/external/mathjax/MathJax.js?config=AM_HTMLorMML-full"></script>
+        <link rel="stylesheet" href="/static/bootstrap/css/bootstrap.min.css">
         <link rel="stylesheet" href="/static/frontend/css/editor.css">
     </head>
     <body>
-        <div id="control-buttons"><button onclick=window.clear_input()>clear</button><div class="separator"></div><button onclick=window.validate_input()>validate</button><button onclick=window.hint_input()>hint</button><button onclick=window.step_input()>step</button><button onclick=window.answer_input()>answer</button><div id="loader"></div></div>
+        <div class="navbar navbar-inverse navbar-fixed-top">
+            <div class="navbar-inner">
+                <div class="container">
+                    <a class="brand" href="">Mathematical Term Rewriting</a>
+                    <ul class="nav">
+                        <li class="active"><a href="index.html">Editor</a></li>
+                        <li><a href="tutorial.html">Tutorial</a></li>
+                    </ul>
+                </div>
+            </div>
+        </div>
 
-        <div id="error"></div>
+        <div class="container">
+            <div id="error" class="alert alert-error">
+                <button type="button" class="close">&times;</button>
+                <strong>Error</strong> <span class="text"></span>
+            </div>
 
-        <div id="input" class="panel">
-            <div class="label">Input view</div>
-            <div class="box">
-                <textarea id="MathInput"></textarea>
+            <div class="row">
+                <div class="span12">
+                    <div class="btn-toolbar">
+                        <button id="btn-clear" class="btn">clear</button>
+                        <div class="btn-group">
+                            <button id="btn-validate" class="btn btn-info">validate</button>
+                            <button id="btn-hint" class="btn btn-info">hint</button>
+                            <button id="btn-step" class="btn btn-info">step</button>
+                        </div>
+                        <button id="btn-answer" class="btn">answer</button>
+                        <div id="loader"></div>
+                    </div>
+                </div>
             </div>
-        </div>
 
-        <div id="math" class="panel">
-            <div class="label">Math view</div>
-        </div>
+            <div class="row">
+                <div class="span6">
+                    <textarea id="math-input" class="span6 math-input"></textarea>
+                </div>
+                <div class="span6">
+                    <div id="pretty-print" class="well pretty-print"></div>
+                </div>
+            </div>
 
-        <div id="credits">Idea and feedback by <a
-                href="http://homepages.cwi.nl/~apt/" target=_window>Prof.dr.
-                K.R. Apt</a>, implementation by Taddeüs Kroes and <a
-                href="http://smvv.kompiler.org" target=_window>Sander van
-                Veen</a>. </div>
+            <div class="row">
+                <div class="span12 credits">
+                    Idea and feedback by <a href="http://homepages.cwi.nl/~apt/" target="_blank">Prof.dr. K.R. Apt</a>,
+                    implementation by Taddeüs Kroes and <a href="http://smvv.kompiler.org" target="_blank">Sander van Veen</a>.
+                </div>
+            </div>
+        </div>
 
+        <script type="text/javascript" src="/static/js/jquery-1.8.2.min.js"></script>
+        <script type="text/javascript" src="/static/bootstrap/js/bootstrap.min.js"></script>
+        <script type="text/javascript" src="/static/external/mathjax/MathJax.js?config=AM_HTMLorMML-full"></script>
         <script type="text/javascript" src="/static/frontend/js/editor.js"></script>
     </body>
 </html>