Add support for providing a markdown toc for external HTML. Use it fo…

…r the Tour of Rocq.

data/tutorials/getting-started/1_01_a_tour_of_rocq.html

@@ -3,7 +3,7 @@
 <p>The Rocq Prover is an interactive theorem prover. It means that it is designed to develop mathematical proofs, and especially to write formal specifications, programs and proofs that programs comply to their specifications. An interesting additional feature of Rocq is that it can automatically extract executable programs from specifications, as either OCaml or Haskell source code.</p>
 <p>Properties, programs and proofs are formalized in the same language called the Calculus of Inductive Constructions (CIC). Then, all logical judgments in Rocq are typing judgments: the very heart of Rocq is in fact a type-checking algorithm.</p>
 <div class="section" id="the-language-of-rocq">
-<h1>The language of Rocq</h1>
+<h2>The language of Rocq</h2>
 <p>Rocq objects are sorted into three categories: the Prop sort, the SProp sort and the Type sort:</p>
 <ul class="simple">
 <li><code class="highlight coq"><span class="kt">Prop</span></code> is the sort for propositions, i.e. well-formed propositions are of type <code class="highlight coq"><span class="kt">Prop</span></code>. Typical propositions are:</li>
@@ -61,7 +61,7 @@ <h1>The language of Rocq</h1>
 </pre>
 </div>
 <div class="section" id="proving-in-rocq">
-<h1>Proving in Rocq</h1>
+<h2>Proving in Rocq</h2>
 <p>Proof development in Rocq is done through a language of tactics that allows a user-guided proof process. At the end, the curious user can check that tactics build lambda-terms. For example the tactic intro n, where n is of type nat, builds the term (with a hole):</p>
 <pre class="code coq literal-block">
 <span class="kr">fun</span> <span class="o">(</span><span class="nv">n</span><span class="o">:</span><span class="n">nat</span><span class="o">)</span> <span class="o">=&gt;</span> <span class="n">_</span> 

data/tutorials/getting-started/1_01_a_tour_of_rocq.md

@@ -7,3 +7,7 @@ category: "First Steps"
 external_html: tutorials/getting-started/1_01_a_tour_of_rocq.html
 recommended_next_tutorials:
 ---
+
+## The language of Rocq
+
+## Proving in Rocq

data/tutorials/getting-started/1_01_a_tour_of_rocq.md.orig

@@ -11,8 +11,11 @@ Instructions to generate 1_01_a_tour_of_rocq.md from 1_01_a_tour_of_rocq.md.orig
    $ alectryon --frontend md --backend webpage data/tutorials/getting-started/1_01_a_tour_of_rocq.md.orig -o data/tutorials/getting-started/1_01_a_tour_of_rocq.html
 4. Remove the untracked generated files:
    $ rm data/tutorials/getting-started/alectryon.css data/tutorials/getting-started/alectryon.js data/tutorials/getting-started/docutils_basic.css data/tutorials/getting-started/pygments.css
-5. Remove the `</body>`, and `</html>` closing tags at the end of the generated 1_01_a_tour_of_rocq.html file.
-6. Remove everything before the following in the generated 1_01_a_tour_of_rocq.html file (as well as the closing comment marker):
+5. Replace all `<h1>` tags with `<h2>` tags in the generated 1_01_a_tour_of_rocq.html file (e.g. using `sed`):
+   $ sed -i 's/<h1>/<h2>/g' data/tutorials/getting-started/1_01_a_tour_of_rocq.html
+   $ sed -i 's/<\/h1>/<\/h2>/g' data/tutorials/getting-started/1_01_a_tour_of_rocq.html
+6. Remove the `</body>`, and `</html>` closing tags at the end of the generated 1_01_a_tour_of_rocq.html file.
+7. Remove everything before the following in the generated 1_01_a_tour_of_rocq.html file (as well as the closing comment marker):
 <div class="document">
 <div class="alectryon-container docutils container">
 -->

tool/ood-gen/lib/tutorial.ml

@@ -60,17 +60,17 @@ let decode (fpath, (head, body_md)) =
     |> Result.get_ok ~error:(fun (`Msg msg) ->
            Exn.Decode_error (fpath ^ ":" ^ msg))
   in
+  let doc = Markdown.Content.of_string body_md in
+  let toc = Markdown.Toc.generate ~start_level:2 ~max_level:4 doc in
   Result.bind metadata (fun metadata ->
       match metadata.external_html with
       | Some path ->
           path |> Fpath.of_string |> Result.map Utils.read_file
           |> Result.map (fun body_html ->
-                 (of_metadata ~fpath ~section ~toc:[] ~body_md:""
+                 (of_metadata ~fpath ~section ~toc:(toc_toc toc) ~body_md:""
                     ~body_html:(Option.value ~default:"" body_html))
                    metadata)
       | None ->
-          let doc = Markdown.Content.of_string body_md in
-          let toc = Markdown.Toc.generate ~start_level:2 ~max_level:4 doc in
           let body_html =
             (* TODO plug in alectryon here *)
             Markdown.Content.render ~syntax_highlighting:true doc