preamble for overriding default documents settings

[ericjohannesson]

In the AST, the preamble is just any string, and I think we should perhaps keep it that way. In any case, my current implementation interprets the preamble as follows.

First of all, I have the default settings (with mutable fields):

val doc_settings : t_doc_settings  = {
    doc_width           = 80;
    left_margin         = 12;
    title_indent        = 12;
    author_indent       = 12;
    abstract_indent     = 12;
    refs_indent         = 12;
    tab_length          = 6;
    abstract_prefix     = Some "ABSTRACT";
    refs_prefix         = Some "REFERENCES";
    ch_prefix           = Some "CHAPTER";
    sec_prefix          = Some "§";
    par_prefix          = Some "¶";
    expand_tag_singular = expand_tag_singular_default;
    expand_tag_plural   = expand_tag_plural_default;
}

where

val expand_tag_singular_default :  Doc_types.ts_tag -> string option = 
  match tag with
  |Cs_tag "DEF" -> Some "DEFINITION"
  |Cs_tag "PRF" -> Some "PROOF"
  |Cs_tag "FCT" -> Some "FACT"
  |Cs_tag "LMA" -> Some "LEMMA"
  |Cs_tag "THM" -> Some "THEOREM"
  | _  -> None

and

val expand_tag_plural_default : Doc_types.ts_tag -> (string * string) option =
  match tag with
  |Cs_tag "DEFS" -> Some ("DEFINITION", "DEFINITIONS")
  |Cs_tag "PRFS" -> Some ("PROOF", "PROOFS")
  |Cs_tag "FCTS" -> Some ("FACT", "FACTS")
  |Cs_tag "LMAS" -> Some ("LEMMA", "LEMMAS")
  |Cs_tag "THMS" -> Some ("THEOREM", "THEOREMS")
  | _  -> None

For changing the (mutable fields of) doc_settings depending on the preamble, I have a function doc_settings_of_tr_doc :

val doc_settings_of_tr_doc : Doc_types.tr_doc -> unit

where

doc_settings_of_tr_doc doc

first checks if doc contains any sections or paragraphs. If not, it sets doc_settings.left_margin to 0 and doc_width to 68.

Secondly, it checks if doc has a preamble. If so, it attempts to parse that preamble and adjusts doc_settings accordingly (possibly overriding the default settings).

(Prints a warning to stderr if parsing fails, and keeps the default value.)

A preamble Cs_preamble (preamble : string) is valid for parsing just in case the preamble has the following format:

PREAMBLE := KEY_VALUE [';' KEY_VALUE]*

KEY_VALUE := | 'doc_width=' INT
             | 'left_margin=' INT
             | 'title_indent=' INT
             | 'author_indent=' INT
             | 'abstract_indent=' INT
             | 'refs_indent=' INT
             | 'tab_length=' INT
             | 'abstract_prefix=' STRING
             | 'refs_prefix=' STRING
             | 'ch_prefix=' STRING
             | 'sec_prefix=' STRING
             | 'par_prefix=' STRING
             | 'singular_tag=' TAG '>' SINGULAR_FORM
             | 'plural_tag=' TAG '>' SINGULAR_FORM '>' PLURAL_FORM

SINGULAR_FORM := TAG

PLURAL_FORM := TAG

TAG := [! ';' '>']*

INT := ['0'-'9']+

STRING := [! ';']*

For instance, having preamble evaluating to

"singular_tag=TMY>TERMINOLOGY;plural_tag=RMKS>REMARK>REMARKS"

will result in tags Cs_tag "TMY" and Cs_tag "RMKS" also being treated like Cs_tag "PRF" and Cs_tag "PRFS", respectively.

Any suggestions/objections/thoughts/questions?

[anderslundstedt]

Let us discuss this IRL at some point.

[anderslundstedt]

I suggest we use, in the default semantics, an existing configuration language. There is for example YAML:

https://en.wikipedia.org/wiki/YAML

There are many more, and I believe we should spend some time evaluating the different alternatives.

[anderslundstedt]

Expanding on the above:

• Potential users are more likely to already be accustomed with an existing configuration language.
• Potential writers of custom semantics would probably prefer to use an existing configuration language for the preamble.

[anderslundstedt]

https://news.ycombinator.com/item?id=45952614