History log of /seL4-l4v-master/HOL4/tools-poly/poly/quse.sig
Revision Date Author Comments
# a503c0af 18-Feb-2020 Michael Norrish <michael.norrish@data61.csiro.au>

Add a useScript entry point to QUse that forces "interactive" mode


# a844c1d4 01-May-2016 Michael Norrish <Michael.Norrish@nicta.com.au>

Rework Poly/ML quotation use to do in-process lexing

This changes from having to use a separate unquote process as part of
Holmake, and may help resolve github issue #340

The drawback at the moment is that the whole file is sucked into memory
before Poly/ML gets to see it. The way the filter code works
could (should?) be changed to lex things in a demand-driven way.