Description
Hello all,
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:
─( 11:13:52 )─< command 0 >───────────{ counter: 0 }─
utop # `1 + 2 = 3`;;
Error: Syntax error
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.
─( 13:09:39 )─< command 1 >────────────{ counter: 0 }─
utop # #use "tmp.ml";;
- : term = `1 + 2 = 3`
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.
Activity