Improvements to latex generation

The main changes so far are:

* Allow markdown formatting in doc comments. We parse the markdown
  using Omd, which is a OCaml library for parsing markdown. The nice
  thing about this library is it's pure OCaml and has no dependencies
  other the the stdlib. Incidentally it was also developed at OCaml
  labs. Using markdown keeps our doc-comments from becoming latex
  specfic, and having an actual parser is _much_ nicer than trying to
  hackily process latex in doc-comments using OCamls somewhat sub-par
  regex support.

* More sane conversion latex identifiers the main approach is to
  convert Sail identifiers to lowerCamelCase, replacing numbers with
  words, and then add a 'category' code based on the type of
  identifier, so for a function we'd have fnlowerCamelCase and for
  type synonym typelowerCamelCase etc. Because this transformation is
  non-injective we keep track of identifiers we've generated so we end
  up with identifierA, identifierB, identifierC when there are
  collisions.

* Because we parse markdown in doc comments doc comments can use Sail
  identifiers directly in hyperlinks, without having to care about how
  they are name-mangled down into TeX compatible things.

* Allow directives to be passed through the compiler to
  backends. There are various $latex directives that modify the latex
  output. Most usefully there's a

  $latex newcommand name markdown

  directive that uses the markdown parser to generate latex
  commands. An example of why this is useful is bellow. We can also use

  $latex noref id

  To suppress automatically inserting links to an identifier

* Refactor the latex generator to make the overall generation process
  cleaner

* Work around the fact that some operating systems consider
  case-sensitive file names to be a good thing

* Fix a bug where latex generation wouldn't occur unless the directory
  specified by -o didn't exist

This isn't quite all the requested features for good CHERI
documentation, but new features should be much easier to add now.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 897f3ec2..4dd72980 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -920,8 +920,8 @@ let to_ast_def (names, k_env, def_ord) partial_defs def : def_progress envs_out
      let kids = List.map to_ast_var kids in
      let nc = to_ast_nexp_constraint k_env nc in
      ((Finished (DEF_constraint (id, kids, nc))), envs), partial_defs
-  | Parse_ast.DEF_pragma (_, _, l) ->
-     typ_error l "Encountered preprocessor directive in initial check" None None None
+  | Parse_ast.DEF_pragma (pragma, arg, l) ->
+     ((Finished(DEF_pragma (pragma, arg, l))), envs), partial_defs
   | Parse_ast.DEF_internal_mutrec _ ->
      (* Should never occur because of remove_mutrec *)
      typ_error Parse_ast.Unknown "Internal mutual block found when processing scattered defs" None None None