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 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*.

[ < ]

[ > ]

[ << ]

[ Up ]

[ >> ]

[Top]

[Contents]

[Index]

[ ? ]

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.