Clément Pit-Claudel <clement....@gmail.com> writes: > Yup, that's roughly how it works in F*-land: the IDE backend plugs in > two functions, and populates its own view of the completion > candidates.
Ah cool! I'll have a look again for sure to see how the API is; I recall looking at the trie itself, but not at the plug part. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
