]> matita.cs.unibo.it Git - helm.git/commitdiff
NEW: manual added and linked to the interface.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 Mar 2003 16:24:59 +0000 (16:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 Mar 2003 16:24:59 +0000 (16:24 +0000)
helm/searchEngine/html/almost_blank.html
helm/searchEngine/html/manual/alias.jpg [new file with mode: 0644]
helm/searchEngine/html/manual/ex1.jpg [new file with mode: 0644]
helm/searchEngine/html/manual/frames.jpg [new file with mode: 0644]
helm/searchEngine/html/manual/index.html [new file with mode: 0644]
helm/searchEngine/html/start.html

index d5eef25184898b015756d61adb4ba69398c3cf68..05204a549c8ccc8571d7c35cf532ebe2f09e3229 100644 (file)
@@ -1,5 +1,5 @@
 <HTML>
 <body bgcolor="#ffffff";>
-Are you lost? Consult the <a href="http://helm.cs.unibo.it/searchEngine/manual.html" target="_blank">on-line manual</a>
+Are you lost? Consult the <a href="http://helm.cs.unibo.it/searchEngine/manual/index.html" target="_blank">on-line manual</a>
 </body>
 </HTML>
diff --git a/helm/searchEngine/html/manual/alias.jpg b/helm/searchEngine/html/manual/alias.jpg
new file mode 100644 (file)
index 0000000..0f57638
Binary files /dev/null and b/helm/searchEngine/html/manual/alias.jpg differ
diff --git a/helm/searchEngine/html/manual/ex1.jpg b/helm/searchEngine/html/manual/ex1.jpg
new file mode 100644 (file)
index 0000000..8e75c08
Binary files /dev/null and b/helm/searchEngine/html/manual/ex1.jpg differ
diff --git a/helm/searchEngine/html/manual/frames.jpg b/helm/searchEngine/html/manual/frames.jpg
new file mode 100644 (file)
index 0000000..994b7ae
Binary files /dev/null and b/helm/searchEngine/html/manual/frames.jpg differ
diff --git a/helm/searchEngine/html/manual/index.html b/helm/searchEngine/html/manual/index.html
new file mode 100644 (file)
index 0000000..0ffaa97
--- /dev/null
@@ -0,0 +1,39 @@
+<html>
+<head>
+<title>Search Engine Interface Online Manual</title>
+</head>
+<body>
+<h2>Index</h2>
+1. <a href="#roles">Roles of the frames</a><br>
+2. <a href="#mqlquery">How to compose a low-level query</a><br>
+3. <a href="#pdqquery">How to compose a pre-defined query</a><br>
+<a name="roles"><h2>1. Roles of the frames</h2></a>
+<p>
+The interface is composed by five frames, as you can see below.<br><br>
+<img src="./frames.jpg"><br><br>
+Each frame has its own role, in particular:<br><ul>
+<li>frame <b>1</b> contains the query as it is, the frame is refreshed whenever you modify the query.<br>
+<li>frame <b>2</b> contains all the available options for the composition of the query, it's where most of the interaction happens.<br>
+<li>frame <b>3</b> contains the form used for the submission of the query and various buttons to modify it.<br>
+<li>frame <b>4</b> contains the grammar.<br>
+<li>frame <b>5</b> contains online help.<br>
+</ul>
+</p>
+<a name="#mqlquery"><h2>2. How to compose a low-level query</h2></a>
+<p>
+In order to compose a low-level query, you must click the &quot;compose a query&quot; button in the main page. Here's what you'll get:<br> <ul><li>In frame 1, you have the query in its actual state, so at the beginning the frame is empty. Later, the frame will be updated automatically on every change of the query and will contain hypertextual links in this form: <b>[?&lt;production name&gt;&lt;production number&gt;]</b>. Possible names are &quot;set&quot;,&quot;val&quot; and &quot;bol&quot; and they represent the main productions of MathQL grammar. By clicking on each of these links you'll obtain the visualization of possible options for the corresponding production in frame 2, allowing the sobstitution of the link with what will be selected.<br> <li>Frame 2 contains, in order: the identifier of the production you are choosing (e.g. <b>[?set1]</b> or <b>[?bol3]</b>), an &quot;undo&quot; button, a &quot;redo&quot; button, the options list, a &quot;compose&quot; button to confirm your choice, a &quot;get help&quot; button to know the semantic meaning of the selected option. The options list is composed by various radio buttons, sometimes you'll have only to select one of them while sometimes you'll have to fill input areas with identifiers, paths or other things: anyway, whenever an input area gets the focus, a help about what you can write there will appear in frame 5.<br>
+<li>Frame 3 contains a textarea with the query, a &quot;submit the query&quot; button, a &quot;restart&quot; button (it will bring you to the main page, erasing you query) and an &quot;apply changes&quot; button to modify the query. <br><li> Frame 4 contains the MathQL grammar.<br> <li>Frame 5 contains various help messages, whenever an object gets the focus a message will appear there.<br></ul>
+Being &quot;set&quot; the main production of MathQL, at the beginning frame 1 is empty and frame 2 contains the menu for &quot;set&quot;. You should choose one option by clicking on its radio button and then press &quot;compose&quot;. 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 &quot;positions&quot; as the requested identifier. As you can see, frame 2 now displays the &quot;val&quot; menu.<br><br>
+<img src="./ex1.jpg"><br><br>
+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 &quot;apply changes&quot;. Obviously &quot;undo&quot; and &quot;redo&quot; buttons will allow you to recover from mistakes; just DON'T use &quot;back&quot;,&quot;forward&quot; and &quot;refresh&quot; buttons on your browser since they will cause unpredictable errors. Once the query is completed, the &quot;submit the query&quot; button will display the results in frame 2.</p>
+<a name="#pdqquery"><h2>3. How to compose a pre-defined query</h2></a>
+<p>
+There are actually three pre-defined queries, <b>Locate Object</b>, <b>Search Pattern</b> and <b>Match Conclusion</b>. By clicking on &quot;submit a pre-defined query&quot; in the main page, a small menu with the three options will appear in frame 2. <br>
+<b>Locate Object</b> is very simple, you must enter the name of the object to search in the text box and click &quot;display results&quot;.<br>
+<b>Search Pattern</b>, which takes a CIC term and finds theorems which have it as thesis, and <b>Match Conclusion</b> which takes a CIC term and finds theorems which have it as conclusion, have an identical interface, being the only difference in the output. 
+First thing to do is to insert a list of aliases (you may skip this step since the search engine will ask you later about ambiguous interpretations of your query if you don't know objects names, for example), then you must compose the CIC term. Composing a CIC term is pretty much the same thing as composing a MathQL query, except that the term is usually so short that there is no need for links, undo buttons and the like. While composing the term, you may modify your list of aliases (i.e. add or remove them) anytime by clicking &quot;edit&quot; in the frame 3. When the query is completed, the &quot;submit&quot; button will display the results in frame 2, and the server will ask you to solve ambiguities, thus adding aliases to your list.  Once a result is displayed, you may want to submit a different query but keep your aliases; in this case, just click &quot;new expression&quot; in frame 3. The &quot;edit&quot; button will work even in this phase.<br><br>
+<img src="./alias.jpg"><br><br>
+</p>
+
+</body>
+</html>
\ No newline at end of file
index 57e85c7e7994ad0d4868dfef7e5e155e531e72fa..c5a6ef70289dac432869f3b0f4112c0af88d7125 100644 (file)
@@ -4,7 +4,7 @@
 </SCRIPT>
 </HEAD>
 <BODY>
-Are you lost? Consult the <a href="http://helm.cs.unibo.it/searchEngine/manual.html" target="_blank">on-line manual</a>
+Are you lost? Consult the <a href="http://helm.cs.unibo.it/searchEngine/manual/index.html" target="_blank">on-line manual</a>
 <br><br>
 <center>
   <input type=button value="Compose a query" onClick="top.cw.location=top.topurl+top.action+'set.html';top.gw.location=top.topurl+top.action+'grammar.html#set';top.sw.location=top.topurl+top.action+'editor.html';top.qw.location=top.topurl+top.action+'almost_blank.html';top.initialize();">