10. MML Query

C-c C-q

query-start-entry

MML Query is a semantic search tool and browser for the MML, written by Grzegorz Bancerek. You can find it at http://megrez.mizar.org/mmlquery/.

In Mizar Mode, you can either ask MML Query for a meaning of a constructor, See section 9.3 Using Constructor explanations, or you can use it to send arbitrary queries to MML Query.

User Option: mizar-query-browser

Browser for MML Query, we allow 'w3 or default.

The default value is nil.

Variable: query-text-output

If non-nil, text output is required from MML Query.

Command: query-start-entry

Start a new query in buffer *MML Query input*.

10.1 Asking arbitrary queries

Once you are in the buffer *MML Query Input* (usually by running C-c C-q (query-start-entry)), you can create and edit an arbitrary query, and send it to MML Query.

Following special bindings are available in that buffer:

C-c C-c

query-send-entry

M-p

query-previous-squery

M-n

query-next-squery

M-s

query-squery-search-forward

M-r

query-squery-search-reverse

Command: query-send-entry

Send the contents of the current buffer to MML Query.

Command: query-previous-squery arg

Cycle backwards through query-squery history.
With a numeric prefix arg, go back arg queries.

Command: query-next-squery arg

Cycle forward through comment history.
With a numeric prefix arg, go forward arg queries.

Command: query-squery-search-forward str

Search forwards through squery history for substring match of str.

Command: query-squery-search-reverse str

Search backward through squery history for substring match of str.