Currently UTop directly passes an input string to UTop.parse_toplevel_phrase which in turn calls Parse.toplevel_phrase.
This implies that even if a user installs a custom preprocessor using camlp5, the input text isn't preprocessed using this.
For example, in HOL Light, a special quotation `x` means an expression called 'term' type, and its camlp5 preprocesses it as parse_term "x". However, this is not being successfully treated:
Rather than finding a solution for fully supporting camlp5, there seems to be a quick possible workaround. If I store `1 + 2 = 3`;; as a temporary file, say tmp.ml, and load it using the #use command, this works great.
A downside of this solution is that UTop cannot track the history of parsed phrases, but this cost is okay to take I believe.
As a possible solution for supporting camlp5, I would like to discuss about adding this as an option to UTop.
Hello all,
Currently UTop directly passes an input string to
UTop.parse_toplevel_phrase
which in turn callsParse.toplevel_phrase
.This implies that even if a user installs a custom preprocessor using camlp5, the input text isn't preprocessed using this.
For example, in HOL Light, a special quotation
`x`
means an expression called 'term' type, and its camlp5 preprocesses it asparse_term "x"
. However, this is not being successfully treated:Rather than finding a solution for fully supporting camlp5, there seems to be a quick possible workaround. If I store
`1 + 2 = 3`;;
as a temporary file, saytmp.ml
, and load it using the#use
command, this works great.A downside of this solution is that UTop cannot track the history of parsed phrases, but this cost is okay to take I believe. As a possible solution for supporting camlp5, I would like to discuss about adding this as an option to UTop.