From: Claudio Sacerdoti Coen Date: Tue, 18 Mar 2003 16:27:00 +0000 (+0000) Subject: 1. internal links fixed X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77b3276d892fc037635fff6b1d0551252282a19f;p=helm.git 1. internal links fixed 2. title added --- diff --git a/helm/searchEngine/html/manual/index.html b/helm/searchEngine/html/manual/index.html index 0ffaa971d..8efa276fc 100644 --- a/helm/searchEngine/html/manual/index.html +++ b/helm/searchEngine/html/manual/index.html @@ -3,6 +3,7 @@ Search Engine Interface Online Manual +

Search Engine Interface Online Manual

Index

1. Roles of the frames
2. How to compose a low-level query
@@ -19,14 +20,14 @@ Each frame has its own role, in particular:

-

2. How to compose a low-level query

+

2. How to compose a low-level query

In order to compose a low-level query, you must click the "compose a query" button in the main page. Here's what you'll get:

Being "set" the main production of MathQL, at the beginning frame 1 is empty and frame 2 contains the menu for "set". You should choose one option by clicking on its radio button and then press "compose". The interface will perform a syntax check of what you entered and should something be wrong a message will appear, otherwise the query will be updated. Afterwards, the query will appear in frame 1 and in frame 3, and frame 2 will display the menu of the first production found in the new query string. For example, in the picture below you see the interface after the selection of the 10th production inserting "positions" as the requested identifier. As you can see, frame 2 now displays the "val" menu.



Now your options include following the instructions in frame 2, choosing a different production by clicking on a link in frame 1, or manually modifying the query by writing the changes in the textarea in frame 3 and then clicking "apply changes". Obviously "undo" and "redo" buttons will allow you to recover from mistakes; just DON'T use "back","forward" and "refresh" buttons on your browser since they will cause unpredictable errors. Once the query is completed, the "submit the query" button will display the results in frame 2.

-

3. How to compose a pre-defined query

+

3. How to compose a pre-defined query

There are actually three pre-defined queries, Locate Object, Search Pattern and Match Conclusion. By clicking on "submit a pre-defined query" in the main page, a small menu with the three options will appear in frame 2.
Locate Object is very simple, you must enter the name of the object to search in the text box and click "display results".
@@ -36,4 +37,4 @@ First thing to do is to insert a list of aliases (you may skip this step since t

- \ No newline at end of file +