Store exercise notes and proof as HTML

[cjerdonek]

One easier thing that I think would improve the structure and maintainability of the code would be to store the HTML "notes" and "proof" for each exercise as HTML.

Currently, these HTML strings are stored as JS string literals (in docs/js/main.js), which isn't great for storing "data" and makes it a bit harder to edit and view the HTML. For example:

QED/docs/js/main.js

Lines 29 to 30 in 2978fc5

Exercise12.notes = '<UL> <LI> It is permissible to drag a statement onto itself.</LI> <LI> <Q>Each problem that I solved became a rule, which served afterwards to solve other problems</Q> - <A HREF="https://en.wikiquote.org/wiki/Ren%C3%A9_Descartes" target="_blank">René Descartes</A>. Each exercise solved in this text becomes a new deduction rule that you may use in subsequent exercises. The <B>Achievements</B> window lists all the rules of inference one has available, either through being unlocked by opening the appropriate exercise, or by proving that rule as one of the exercises.</LI><LI> One can also use the numbers \'1\' through \'9\' as hotkeys for the available eductions (or the first 9 of them, at any rate).</LI></UL>';

Exercise12.proof = '<li><span><em>A</em> AND <em>B</em>. <i>[given]</i></span></li><li><span>From <em>A</em> AND <em>B</em>: deduce <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (left)]</i></span></li><li><span>From <em>A</em> AND <em>B</em>: deduce <em>B</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_elimination" target="_blank">CONJUNCTION ELIMINATION</a> (right)]</i></span></li><li><span>From <em>B</em>, <em>A</em>: deduce <em>B</em> AND <em>A</em>. <i>[<a href="https://en.wikipedia.org/wiki/Conjunction_introduction" target=" _blank">CONJUNCTION INTRODUCTION</a>]</i></span></li><li><span>QED!</span></li>';

One idea is to store this information in the form of hidden (i.e. not seen when browsing) "data" divs in the main html file. The structure for each exercise could be something like--

<div id="exercise-3">
<div class="notes">...</div>
<div class="proof">...</div>
</div>

Then a load_exercise_data(exercise, id) JS function could be defined that populates an Exercise object from the HTML document, and this called from within main.js for each exercise. Over time, more of the exercise "data" could be transferred to a more structured form (e.g. the "unlocks" and "unlockedBy" information), until perhaps all of each exercise can be populated from data.

[teorth]

I like this suggestion. I managed to quickly write up some code for this and ported the first exercise HTML data over this way. Already it revealed that there were some typos etc. in the HTML. Porting the remaining 132 exercises will be a bit tedious but should be done before too long.

[cjerdonek]

Great! A few suggestions on this approach:

• Prefix the element id's with exercise- since id's should be globally unique within the document, and there could a priori be other types of objects.
• Use document.getElementById() to locate elements by id.
• Wrap the HTML to a shorter line length (e.g. 80-100 characters or so) to make it easier to read in the GitHub UI and text editors and so that diffs and merges, etc. will be easier.

You can also use JS selectors to more elegantly find the data within an HTML element (e.g. "find the first child with class attribute 'notes'," etc). So you would have code for each exercise attribute you want to set, instead of looping over every child with a switch statement on the class name. (This is more of a style judgement.)

[cjerdonek]

PS - If you’re not already doing this, it could also help to maintain in the JavaScript a dictionary of the exercises mapping the short name or ID to the corresponding Exercise object. This will be useful for e.g. storing the “unlocks” info as data. The unlocks info could then be stored as e.g. a space-delimited attribute value of the div for that exercise.

[teorth]

OK, I'm done for now; I've prefixed the id's and formatted some of the HTML (not the proofs though, as this would be rather tedious and I would expect them to be rarely edited by hand).

I have an exerciseList array that could be used for mapping ids to exercises if need be, but at present there isn't a need for it, so I haven't bothered to code a lookup routine yet.

Using a selector would indeed be more elegant, but it ain't broken right now, so I'm not fixing it.

[cjerdonek]

FYI, I added initial support for also storing the "unlockedBy" info in the HTML, and did this for the first couple exercises as an example.