¹Printing a meta-term into a list of quoted identifiers, with various printing options is supported by the printTerm operator:
op printTerm : Oid Oid Qid Term PrintOptionSet QidSet -> Msg [ctor msg format (b o)] .
Here the PrintOptionSet argument takes the same set of options supported by metaPrettyPrint(), and the QidSet argument indicates which operators should have the arguments concealed. The reply is:
op printedTerm : Oid Oid QidList -> Msg [ctor msg format (m o)] .
The printTermToString/printedTermToString pair of messages provide similar functionality but taking a string. The meta-interpreter has a new pair of messages
op printTermToString : Oid Oid Qid VariableSet Term PrintOptionSet QidSet -> Msg
[ctor msg format (b o)] .
op printedTermToString : Oid Oid String -> Msg [ctor msg format (m o)] .