From 953bfdd18c71bcd6c486aac74fe145104c3b2a4d Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 7 Nov 2018 18:56:28 +0000
Subject: 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.
---
 src/util.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src/util.mli')

diff --git a/src/util.mli b/src/util.mli
index 1d80bc10..fd0242a3 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -57,8 +57,8 @@ val opt_colors : bool ref
 val butlast : 'a list -> 'a list
 
 (** Mixed useful things *)
-module Duplicate(S : Set.S) : sig 
-  type dups = 
+module Duplicate(S : Set.S) : sig
+  type dups =
     | No_dups of S.t
     | Has_dups of S.elt
   val duplicates : S.elt list -> dups
@@ -259,5 +259,7 @@ val warn : string -> unit
 val zencode_string : string -> string
 val zencode_upper_string : string -> string
 
+val file_encode_string : string -> string
+
 val log_line : string -> int -> string -> string
 val header : string -> int -> string
-- 
cgit v1.2.3