SIGNATURE ReadLine

-- Command line edtior with history and completion functionality
-- based on the GNU readline library

-- Version 1.0

IMPORT  Nat             ONLY nat
        Seq[denotation] ONLY seq
        Com[denotation] ONLY com
        Com[seq]        ONLY com ans

FUN readLine : denotation -> com[denotation]
    -- prompt string and read a line, supplying sophisticated line
    -- editing and history functionality. the read line
    -- is added to the history provided it is not empty.
    -- typing ^D at the beginning of the input line
    -- lets the command fail (thats the only source of failure). 
    -- see the GNU readline user
    -- documentation how key bindings may be configured by
    -- the users ~/.inputrc

FUN readLine : denotation **
               (denotation ** denotation ** nat ** nat -> com[seq[denotation]])
               -> com[denotation]
    -- version of readLine with a completer function. 
    -- the completer gets passed the word to be completed,
    -- the line read so far, and the start and end position
    -- of the word to be completed in the line. 
    -- if the completer fails, a standard completion mechanism for
    -- file names take over (so don't let the completer fail if
    -- you don't want this behaviour).
    

/* NB. direct access to the GNU readLine's command extension and
   history management currently not supported */