Ver Fonte

Math expressions in hints are pretty printed using MathJax.

Sander Mathijs van Veen há 13 anos atrás
pai
commit
dbc158eb57
4 ficheiros alterados com 10 adições e 1 exclusões
  1. 4 0
      src/frontend/css/editor.css
  2. 1 0
      src/frontend/js/editor.js
  3. 1 1
      src/parser.py
  4. 4 0
      src/possibilities.py

+ 4 - 0
src/frontend/css/editor.css

@@ -77,6 +77,10 @@ body {
     line-height: 20px;
 }
 
+#math .hint .MathJax {
+    color: #000;
+}
+
 #control-buttons {
     height: 21px;
     left: 2%;

+ 1 - 0
src/frontend/js/editor.js

@@ -134,6 +134,7 @@
         var elem = $('<div class=hint/>');
         elem.text(hint);
         $('#math').append(elem);
+        QUEUE.Push(['Typeset', MathJax.Hub, elem[0]]);
     };
 
     window.append_input = function(input) {

+ 1 - 1
src/parser.py

@@ -262,7 +262,7 @@ class Parser(BisonParser):
         hint = self.give_hint()
 
         if hint:
-            print hint
+            print str(hint).replace('`', '')
         else:
             print 'No further reduction is possible.'
 

+ 4 - 0
src/possibilities.py

@@ -1,4 +1,5 @@
 from node import TYPE_OPERATOR
+import re
 
 
 # Each rule will append its hint message to the following dictionary. The
@@ -18,6 +19,9 @@ class Possibility(object):
         if self.handler in MESSAGES:
             msg = MESSAGES[self.handler]
 
+            # Surround math notation with backticks
+            msg = re.sub('({[^ ]+)', r'`\1`', msg)
+
             if callable(msg):
                 msg = msg(self.root, self.args)