proper positions for inlined command messages, e.g. for completion within theory header;