Add /add rule/ feature and help file

ndt93 · Sep 11, 2013 · a6b6e07 · a6b6e07
1 parent 4deb5e7
commit a6b6e07
Show file tree

Hide file tree

Showing 8 changed files with 194 additions and 3 deletions.
diff --git a/README.md b/README.md
@@ -1,2  1,28 @@
 Proof-Editor
 ============
 A Fitch's Style Proof Editor for Natural Deduction
 The application is written entirely in Javascript and can be used offline without any server-side code
 
 How to Use
 ------------
 Type in proposition in Proposition Box. Logical Connectives: &, v, ~, => are allowed.
 Variables can be any combination of characters and parentheses except characters reserved for
 logical connectives. Some mismatched and invalid syntax can be resolved by the application but
 not all cases are guaranteed
 
 Press "Premise" or "Assumption" button to add the proposition to the editing area
 
 Select relevant propositions in the editing area and press targeted rule in the rule box.
 A conclusion will be generated in the proposition box according to the rule and propositions selected.
 Make changes to the conclusion if any and press Conclude Button to add conclusion to the editing area
 or Clear Button to remove it.
 
 Any error in matching or parsing process will be displayed above editing area. Hovering mouse over a rule
 button will also display a summary of the corresponding rule in the summary box
 
 Press Clear Button to clear the Proposition box and remove any error message
 Press Undo Button to remove last added proposition
 Press Printable Button to generate a text formatted version of the current proof
 
 Click "Add Rule" Button to add new Rule. Enter required information accordingly. These added rules
 are not permanent. Refreshing the page will remove any custom rule.
diff --git a/app_style.css b/app_style.css
@@ -133,3  133,32 @@ ul#rules_box input[type="button"] {
     color: #858283;
     font-size: small;
 }
 
 #add_rule_box {
     position: absolute;
     top: 35%;
     left: 27.5%;
     margin: 0 auto;
     border: solid thin black;   
     padding: 20px;
     padding-right: 10px;
     padding-bottom: 5px;
     -webkit-box-shadow: 3px 3px 3px #888888;
     box-shadow: 3px 3px 3px #888888;
     visibility: hidden;
 }
 
 .new_input {
     width: 300px;
 }
 
 .note {
     font-size: small;
     color: #858283;
     padding: 0px;
     margin: 0px;
 }
 
 .right {
     text-align: right;
 }
diff --git a/core.js b/core.js
@@ -39,9  39,9 @@ function parse(s, depth) {
         if (c == '(') {
             var p = parse(s, depth   1);
             if (p.length > 1 &&
-                ( (depth && /[&^~]|(>)|(-)/.test(s[depth-1])) ||
                 ( (depth && /[&v~]|(>)|(-)/.test(s[depth-1])) ||
                   ( ((depth   p.length   2) < (s.length - 1)) &&
-                    /[&^~]|(>)|(-)/.test(s[depth   p.length   2]) )
                     /[&v~]|(>)|(-)/.test(s[depth   p.length   2]) )
                 )
                ) {
                 depth  = p.length   2;

diff --git a/data.js b/data.js
@@ -30,4  30,5 @@ var INVALID_MATCH_QUANTITY = 2;
 var INVALID_MATCH_QUALITY = 3;
 var ERROR_MESSAGE_SCOPE= "Some premises cannot be used under current scope";
 var ERROR_MESSAGE_MATCH_QUANTITY = "Invalid number of premises";
-var ERROR_MESSAGE_MATCH_QUALITY = "Premises cannot match selected rule pattern";
 var ERROR_MESSAGE_MATCH_QUALITY = "Premises cannot match selected rule pattern";
 var ERROR_RULE_ALREADY_EXISTS = "Rule identifier already exists";
diff --git a/help.html b/help.html
@@ -0,0  1,56 @@
 <html>
     <head>
         <meta charset="utf-8">
         <title>How to use</title>
         <style>
             li {
                 line-height: 1.5em;
                 padding-top: 1.5em;
                 text-align: justify;
             }
             h1 {
                 text-align: center;
             }
         </style>
     </head>
     <body>
         <div class="content" style="width: 800px; margin: 0 auto">
             <h1>How to use Proof Editor</h1>
             <hr>
             <ul>
                 <li>
                     Type in proposition in Proposition Box. Logical Connectives: &, v, ~, => are allowed.
                     Variables can be any combination of characters and parentheses except characters reserved for
                     logical connectives. Some mismatched and invalid syntax can be resolved by the application but
                     not all cases are guaranteed
                 </li>
                 <li>
                     Press "Premise" or "Assumption" button to add the proposition to the editing area
                 </li>
                 <li>
                     Select relevant propositions in the editing area and press targeted rule in the rule box.
                     A conclusion will be generated in the proposition box according to the rule and propositions selected.
                     Make changes to the conclusion if any and press Conclude Button to add conclusion to the editing area
                     or Clear Button to remove it.
                 </li>
                 <li>
                     Any error in matching or parsing process will be displayed above editing area. Hovering mouse over a rule
                     button will also display a summary of the corresponding rule in the summary box
                 </li>
                 <li>
                     Press Clear Button to clear the Proposition box and remove any error message
                 </li>
                 <li>
                     Press Undo Button to remove last added proposition
                 </li>
                 <li>
                     Press Printable Button to generate a text formatted version of the current proof
                 </li>
                 <li>
                     Click "Add Rule" Button to add new Rule. Enter required information accordingly. These added rules
                     are not permanent. Refreshing the page will remove any custom rule.
                 </li>
             </ul>
         </div>
     </body>
 </html>
diff --git a/helper.js b/helper.js
@@ -27,6  27,13 @@ function beautify(string) {
     return t_string;
 }
 
 function map(func, array) {
     for (var i = 0; i < array.length; i  ) {
         array[i] = func(array[i]);
     }
     return array;
 }
 
 
 function getPrefixedScopeId(scope) {
     return SCOPE_PREFIX   (cur_scope.join(".") || "0");

diff --git a/index.html b/index.html
@@ -1,6  1,7 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
     <meta charset="utf-8">
     <title>Fitch's Style Proof Editor</title>
     <link rel="stylesheet" href="app_style.css">
     <script src="helper.js"></script>
@@ -28,8  29,35 @@ <h3>Fitch's Style Proof Editor</h3>
 		<ol id="scope_0">
 
 		</ol>
 		<table id="add_rule_box">
 		    <tr>
 			<td class="right">Identifier</td>
 			<td><input type="text" id="new_id" class="new_input"></td>
 		    </tr>
 		    <tr>
 			<td class="right">Rule Name</td>
 			<td><input type="text" id="new_name" class="new_input"></td>
 		    </tr>
 		    <tr>
 			<td class="right">Premises</td>
 			<td><input type="text" id="new_premises" class="new_input"></td>
 		    </tr>
 		    <tr>
 			<td class="right">Conclusion</td>
 			<td><input type="text" id="new_conclusion" class="new_input"></td>
 		    </tr>
 		    <tr>
 			<td colspan="2" class="note">Use single alphabet except v for variable.
 			Separate premises by comma</td>
 		    </tr>
 		    <tr>
 			<td colspan="2" class="right"><input type="button" id="add" value="Add">
 			    <input type="button" id="cancel_add" value="Cancel"></td>
 		    </tr>
 		</table>
 	    </div>
 	    <div class="footer">
 		<a href="help.html">How to use</a>
 	    <input type="button" id="add_rule" value="Add Rule">
 	    <input type="button" id="printable" value="Printable">
 		<input type="button" id="undo" value="Undo" disabled="true">

diff --git a/main.js b/main.js
@@ -146,6  146,15 @@ function undo() {
     }
 }
 
 function addRule(id, rule) {
     var rule_box = document.getElementById("rules_box");
     builtin_rules[id] = builtin_rules[id] || rule;
     var rule_button = document.createElement("input");
     rule_button.type = "button"; rule_button.value = rule.name;
     rule_button.id = id;
     rule_box.appendChild(rule_button);
 }
 
 function init() {
     cur_area = document.getElementById("scope_0");
     var rule_box = document.getElementById("rules_box");
@@ -164,6  173,9 @@ function setupListeners() {
     var conclude_button = document.getElementById("conclude");
     undo_button = document.getElementById("undo");
     var print_button = document.getElementById("printable");
     var add_rule_button = document.getElementById("add_rule");
     var add_button = document.getElementById("add");
     var cancel_add_button = document.getElementById("cancel_add");
 
     var expression = document.getElementById("expression");
     var message = document.getElementById("message");
@@ -249,6  261,38 @@ function setupListeners() {
                                   <body><pre id='content'></pre></body></html>");
         proof_print.document.getElementById("content").innerHTML = exportPrintable(actionsStack);
     });
 
     add_rule_button.addEventListener("click", function () {
         var add_rule_box = document.getElementById("add_rule_box");
         add_rule_box.style.visibility = "visible";
     });
 
     cancel_add_button.addEventListener("click", function () {
         var add_rule_box = document.getElementById("add_rule_box");
         add_rule_box.style.visibility = "hidden";
     });
 
     add_button.addEventListener("click", function () {
         if (builtin_rules[id]) {
             message_box.innerHTML = ERROR_RULE_ALREADY_EXISTS;
         } else {
             var id = document.getElementById("new_id").value;
             var name = document.getElementById("new_name").value;
             var premises = document.getElementById("new_premises").value.split(",");
             var conclusion = document.getElementById("new_conclusion").value;
 
             premises = map(trim, premises);
             for (var i = 0; i < premises.length; i  ) {
                 premises[i] = beautify(parse(premises[i].split(""), 0));
             }
             conclusion = beautify(parse(trim(conclusion).split(""), 0));
             var new_rule = new Rule(name, premises, conclusion);
             addRule(id, new_rule);
 
             var add_rule_box = document.getElementById("add_rule_box");
             add_rule_box.style.visibility = "hidden";
         }
     });
 }
 
 function main() {