migrate to mdbook

Author: Aurel300

.github/workflows/build.yaml

@@ -11,56 +11,29 @@ jobs:
       with:
         path: "tutorial"
 
-    - name: Checkout generator
-      uses: actions/checkout@v2
-      with:
-        repository: "viperproject/viperonline-tutorial-generator"
-        token: ${{ secrets.GH_PAT }}
-        path: "generator"
-
     - name: Checkout build branch
       uses: actions/checkout@v2
       with:
         ref: "build"
-        path: "generator/build"
-
-    - name: Create directory structure
-      run: |
-        cd generator
-        rm -rf build/css build/images build/js
-        cp -r assets/css build/css
-        cp -r assets/images build/images
-        cp -r assets/js build/js
+        path: "tutorial/book"
 
-    - name: Install node packages
-      run: |
-        cd generator
-        npm install
+    - name: Setup mdBook
+      uses: peaceiris/actions-mdbook@v1
+      with:
+        mdbook-version: "latest"
 
     - name: Generate tutorial
       run: |
-        cd generator
-        node index.js \
-          ../tutorial/tutorial/introduction.md \
-          ../tutorial/tutorial/structure.md \
-          ../tutorial/tutorial/permissions.md \
-          ../tutorial/tutorial/predicates.md \
-          ../tutorial/tutorial/functions.md \
-          ../tutorial/tutorial/quantifiers.md \
-          ../tutorial/tutorial/quantified-permissions.md \
-          ../tutorial/tutorial/magic-wands.md \
-          ../tutorial/tutorial/statements.md \
-          ../tutorial/tutorial/expressions-and-assertions.md \
-          ../tutorial/tutorial/domains.md \
-          ../tutorial/tutorial/termination.md \
-          ../tutorial/tutorial/further-info.md
+        cd tutorial
+        mdbook build
 
     - name: Create build commit
+      if: github.ref == 'refs/heads/master' && github.event_name != 'pull_request'
       run: |
-        cd generator/build
+        cd tutorial/book
         git config --local user.email "41898282+github-actions[bot]@users.noreply.github.com"
         git config --local user.name "github-actions[bot]"
-        git add css images js index.html
+        git add css FontAwesome fonts *.html *.js *.css
         git commit -m "Deploy $(date +'%Y-%m-%d %H:%M:%S')"
 
     - name: Push tutorial to build branch
@@ -69,4 +42,4 @@ jobs:
       with:
         branch: build
         force: true
-        directory: generator/build
+        directory: tutorial/book

.gitignore

@@ -1 +1 @@
-tutorial/tutorial.md
+book

README.md

@@ -6,34 +6,40 @@ Feel free to submit your fixes and additions via pull requests.
 
 Please report technical issues via the issue tracker.
 
-# Editing 
+## Building
 
-## Interactive Viper code snippets
+The tutorial uses [`mdbook`](https://rust-lang.github.io/mdBook/) to generate HTML pages. To build, run (from the repository root):
 
-In order to create an interacative code snippet (which can be verified directly in the web browser), inser the code in the following way: 
+```bash
+mdbook build
+```
+
+This creates a folder called `book`. To watch for changes and automatically rebuild files when the source content updates:
+
+```bash
+mdbook serve
+```
+
+## Editing
 
+### Interactive Viper code snippets
 
-````Markdown
+In order to create an interacative code snippet (which can be verified directly in the web browser), insert the code in the following way: 
 
-```silver {.runnable }
+````md
+```viper,editable,playground
 method foobar() 
 {
 	assert false
 }
 ```
 ````
 
-## Including exercises
+### Including exercises
 
 Use the following syntax in order to include an exercise to the tutorial: 
 
-```Markdown
-
-//exercise//
-
-* Sub-task A
-* Sub-task B
-* Sub-task C
-
-///
-```
+```md
+> **Exercise**
+> * ...
+```

book.toml

@@ -0,0 +1,15 @@
+[book]
+authors = ["ETH Zurich"]
+language = "en"
+src = "src"
+title = "Viper Tutorial"
+
+[output.html.playpen]
+editable = true
+
+[output.html]
+additional-js = [
+    "editor.js",
+    "mode-viper.js",
+]
+# additional-js = ["highlight.viper.js"]

editor.js

@@ -0,0 +1,31 @@
+"use strict";
+window.editors = [];
+(function(editors) {
+    if (typeof(ace) === 'undefined' || !ace) {
+        return;
+    }
+
+    Array.from(document.querySelectorAll('.editable')).forEach(function(editable) {
+        let display_line_numbers = window.playground_line_numbers || false;
+
+        let editor = ace.edit(editable);
+        editor.setOptions({
+            highlightActiveLine: false,
+            showPrintMargin: false,
+            showLineNumbers: display_line_numbers,
+            showGutter: true, // display_line_numbers,
+            maxLines: Infinity,
+            fontSize: "0.875em", // please adjust the font size of the code in general.css
+            useSoftTabs: true,
+            tabSize: 2,
+        });
+
+        editor.$blockScrolling = Infinity;
+
+        editor.getSession().setMode("ace/mode/viper");
+
+        editor.originalCode = editor.getValue();
+
+        editors.push(editor);
+    });
+})(window.editors);