Text.Literate

A simple module to process 'literate' documents.

The module uses a lexer to split the document into code blocks,
delineated by user-defined markers, and code lines that are
indicated be a line marker. The lexer returns a document stripped
of non-code elements but preserving the original document's line
count. Column numbering of code lines are not preserved.

The underlying tokeniser is greedy.

Once it identifies a line marker it reads a prettifying space then
consumes until the end of line. Once identifies a starting code
block marker, the lexer will consume input until the next
identifiable end block is encountered. Any other content is
treated as part of the original document.

Thus, the input literate files *must* be well-formed w.r.t
to code line markers and code blocks.

A further restriction is that literate documents cannot contain
the markers within the document's main text: This will confuse the
lexer.

Definitions

lines : String -> List1 String

Totality: total
Visibility: export

record LiterateError : Type

Totality: total
Visibility: public export
Constructor: 

MkLitErr : Int -> Int -> String -> LiterateError

Projections:

.column : LiterateError -> Int

.input : LiterateError -> String

.line : LiterateError -> Int

.line : LiterateError -> Int

Totality: total
Visibility: public export

line : LiterateError -> Int

Totality: total
Visibility: public export

.column : LiterateError -> Int

Totality: total
Visibility: public export

column : LiterateError -> Int

Totality: total
Visibility: public export

.input : LiterateError -> String

Totality: total
Visibility: public export

input : LiterateError -> String

Totality: total
Visibility: public export

record LiterateStyle : Type

  Description of literate styles.
  
  A 'literate' style comprises of
  
  + a list of code block deliminators (`deliminators`);
  + a list of code line markers (`line_markers`); and
  + a list of known file extensions `file_extensions`.
  
  Some example specifications:
  
  + Bird Style
  
  ```
  MkLitStyle Nil [">"] [".lidr"]
  ```
  
  + Literate Haskell (for LaTeX)
  
  ```
  MkLitStyle [("\\begin{code}", "\\end{code}"),("\\begin{spec}","\\end{spec}")]
            Nil
            [".lhs", ".tex"]
  ```
  
  + OrgMode
  
  ```
  MkLitStyle [("#+BEGIN_SRC idris","#+END_SRC"), ("#+COMMENT idris","#+END_COMMENT")]
            ["#+IDRIS:"]
            [".org"]
  ```
  
  + Common Mark
  
  ```
  MkLitStyle [("```idris","```"), ("<!-- idris","--!>")]
            Nil
            [".md", ".markdown"]
  ```
  

Totality: total
Visibility: public export
Constructor: 

MkLitStyle : List (String, String) -> List String -> List String -> LiterateStyle

Projections:

.deliminators : LiterateStyle -> List (String, String)

  The pairs of start and end tags for code blocks.

.file_extensions : LiterateStyle -> List String

  Recognised file extensions. Not used by the module, but will be
  of use when connecting to code that reads in the original source
  files.

.line_markers : LiterateStyle -> List String

  Line markers that indicate a line contains code.

.deliminators : LiterateStyle -> List (String, String)

  The pairs of start and end tags for code blocks.

Totality: total
Visibility: public export

deliminators : LiterateStyle -> List (String, String)

  The pairs of start and end tags for code blocks.

Totality: total
Visibility: public export

.line_markers : LiterateStyle -> List String

  Line markers that indicate a line contains code.

Totality: total
Visibility: public export

line_markers : LiterateStyle -> List String

  Line markers that indicate a line contains code.

Totality: total
Visibility: public export

.file_extensions : LiterateStyle -> List String

  Recognised file extensions. Not used by the module, but will be
  of use when connecting to code that reads in the original source
  files.

Totality: total
Visibility: public export

file_extensions : LiterateStyle -> List String

  Recognised file extensions. Not used by the module, but will be
  of use when connecting to code that reads in the original source
  files.

Totality: total
Visibility: public export

extractCode : LiterateStyle -> String -> Either LiterateError String

  Given a 'literate specification' extract the code from the
  literate source file (`litStr`) that follows the presented style.
  
  @specification The literate specification to use.
  @litStr  The literate source file.
  
  Returns a `LiterateError` if the literate file contains malformed
  code blocks or code lines.
  

Totality: total
Visibility: export

unlit : LiterateStyle -> String -> Either LiterateError String

  Synonym for `extractCode`.

Totality: total
Visibility: export

isLiterateLine : LiterateStyle -> String -> (Maybe String, String)

  Is the provided line marked up using a line marker?
  
  If the line is suffixed by any one of the style's set of line
  markers then return length of literate line marker, and the code stripped from the line
  marker. Otherwise, return Nothing and the unmarked line.

Totality: total
Visibility: export

embedCode : LiterateStyle -> String -> String

  Given a 'literate specification' embed the given code using the
  literate style provided.
  
  If the style uses deliminators to denote code blocks use the first
  pair of deliminators in the style. Otherwise use first linemarker
  in the style. If there is **no style** return the presented code
  string unembedded.
  
  
  @specification The literate specification to use.
  @code  The code to embed,
  
  

Totality: total
Visibility: export

relit : LiterateStyle -> String -> String

  Synonm for `embedCode`

Totality: total
Visibility: export