]> matita.cs.unibo.it Git - helm.git/blob - helm/uwobo-panel/control.html
5345fa33466762b593164b36fe785ecd2c0e2293
[helm.git] / helm / uwobo-panel / control.html
1 <html>
2
3 <head>
4 <title>UWOBO Control Panel</title>
5
6 <style type="text/css">
7 #normal { background-color: white; font-family: sans-serif }
8 td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
9 td.back { background-color: #e6e6fa; color: brown }
10 #indent { margin-left: 1cm; margin-right: 1cm }
11 </style>
12
13 <script language="JavaScript" src="control.js">
14 </script>
15
16 </head>
17
18 <body id="normal">
19 <a name="top"/>
20 <table border="0" width="100%" cellpadding="4">
21 <tr><td class="head" align="center"><big><big>UWOBO Control Panel</big></big></td></tr>
22 </table>
23
24 <br />
25
26 <div id="indent">
27 This is a control panel for the UWOBO Web-Service. You can control a local or remote UWOBO service by filling
28 the appropriate fields <a href="#params">below</a> and sending the desired commands. In most cases, results of commands, such as error
29 messages or documents, will be opened in the frame at the bottom of this page. For those commands sending multiple
30 requests to the UWOBO server, a new window will be opened for each request issued. Note that in order to use
31 this page <i>you must have JavaScript enabled</i>.
32
33 <br /><br />
34
35 The sections:
36 <ul>
37   <li><a href="#params">Global Parameters</a></li>
38   <li><a href="#sessions">Daemon Management</a></li>
39   <li><a href="#queries">Queries</a></li>
40   <li><a href="#stylesheets">Stylesheet Management</a></li>
41   <li><a href="#process">Processing</a></li>
42 </ul>
43
44 In case you want to customize the panel for your own needs, you can download the source archive
45 (HTML + JavaScript):
46 <ul>
47   <li>UWOBO Panel [<a href="uwobo-panel.tar.gz">.tar.gz</a>]</li>
48 </ul>
49
50 </div>
51
52 <a name="params"/>
53 <table border="0" width="100%" cellpadding="4" cellspacing="0">
54 <tr>
55   <td class="head" align="left"><big>Global Parameters</big></td>
56   <td class="back" align="right"><a href="#top">top</a></td>
57 </tr>
58 </table>
59
60 <br />
61
62 <div id="indent">
63 The following are global parameters used by all the other section to contact the UWOBO service and possibly a
64 Getter. The Getter is not required for some operations and can be excluded by unchecking the proper buttons
65 below.
66
67 <br /><br />
68
69 The following is the URL used to contact the UWOBO Web-Service.
70 <tt>localhost</tt> is relative to your machine. 
71
72 <br /><br />
73
74 <table border="0">
75   <tr>
76     <th colspan="2" align="left">UWOBO URL</th>
77   </tr>
78   <tr>
79     <td>
80       <form name="uwoboURL">
81         <script>
82           document.write('<input type="text" value="' + getInitialProcessorURL() + '" size="50"/>');
83         </script>
84       </form>
85     </td>
86     <td>
87       <form>
88         <select onChange="selectUwoboURL(this)">
89           <option value="">---</option>
90           <option value="localhost">localhost</option>
91           <option value="marcello.cs.unibo.it">marcello</option>
92           <option value="phd.cs.unibo.it">phd</option>
93           <option value="eolo.cs.unibo.it">eolo</option>
94     <option value="helm.phd.cs.unibo.it">helm</option>
95         </select>
96       </form>
97     </td>
98     <td>
99       <form>
100         <input type="button" value="Check" onClick="top.result.location.replace(getUwoboURL() + 'help')"/>
101       </form>
102     </td>
103   </tr>
104 </table>
105
106 The following is the URL used to contact the getter. The getter is usually launched manually.
107 In all cases except for the check button below, 
108 <tt>localhost</tt> is relative to the host running UWOBO, because the getter URL is sent as
109 a parameter along with UWOBO commands. In other words, <tt>localhost</tt> <i>is</i> the host
110 running UWOBO and not your machine.
111
112 <br /><br />
113
114 <table border="0">
115   <tr>
116     <th colspan="2" align="left">Getter URL</th>
117   </tr>
118   <tr>
119     <td>
120       <form name="getterURL">
121         <script>
122           document.write('<input type="text" value="' + getInitialGetterURL() + '" size="50"/>');
123         </script>
124       </form>
125     </td>
126     <td>
127       <form>
128         <select onChange="selectGetterURL(this)">
129           <option value="">---</option>
130           <option value="localhost">localhost</option>
131           <option value="marcello.cs.unibo.it">marcello</option>
132           <option value="phd.cs.unibo.it">phd</option>
133           <option value="eolo.cs.unibo.it">eolo</option>
134         </select>
135       </form>
136     </td>
137     <td>
138       <form>
139         <input type="button" value="Check" onClick="top.result.location.replace(getGetterURL() + 'help')"/>
140       </form>
141     </td>
142   </tr>
143 </table>
144 </div>
145
146 <br />
147
148 <a name="sessions"/>
149 <table border="0" width="100%" cellpadding="4" cellspacing="0">
150 <tr>
151   <td class="head" align="left"><big>Daemon Management</big></td>
152   <td class="back" align="right"><a href="#top">top</a></td>
153 </tr>
154 </table>
155
156 <br />
157
158 <div id="indent">
159 <p>You can start a new daemon on a given port. The new daemon will have
160    an empty list of processed stylesheets.
161 </p>
162 <table border="0">
163   <tr>
164     <th colspan="2" align="left">Port</th>
165   </tr>
166   <tr>
167     <td>
168       <form name="sessions">
169         <script>
170           document.write('<input type="text" value="' + getInitialPort() + '" size="5"/>');
171         </script>
172       </form>
173     </td>
174     <td>
175       <form>
176         <input type="button" value="Start New Daemon" onClick="top.result.location.replace(getUwoboURL() + 'newsession?port=' + document.sessions.elements[0].value)"/>
177       </form>
178     </td>
179   </tr>
180 </table>
181 </div>
182
183 <br />
184
185 <div id="indent">
186 <p>You can also kill the daemon. The log file will be mantained.</p>
187 <table border="0">
188   <tr>
189     <td>
190       <form>
191         <input type="button" value="Stop Daemon" onClick="top.result.location.replace(getUwoboURL() + 'kill')"/>
192       </form>
193     </td>
194   </tr>
195 </table>
196 </div>
197
198 <br />
199 <a name="queries"/>
200 <table border="0" width="100%" cellpadding="4" cellspacing="0">
201 <tr>
202   <td class="head" align="left"><big>Queries</big></td>
203   <td class="back" align="right"><a href="#top">top</a></td>
204 </tr>
205 </table>
206
207 <div id="indent">
208
209 <br />
210
211 The following are commands to do some simple queries about the UWOBO service.
212
213 <br /><br />
214
215 <table border="0">
216 <tr>
217   <td>
218     Retrieve the version of the UWOBO service running at the UWOBO URL and list the syntax
219     of the accepted commands.
220     You can use this button to verify that a UWOBO service
221     is actually running there:
222   </td>
223 </tr>
224 <tr>
225   <td><form><input type="button" value="Help" onClick="top.result.location.replace(getUwoboURL() + 'help')"/></form></td>
226 </tr>
227 <tr>
228   <td>
229     Ask UWOBO for a list of the stylesheets currently compiled inside the Web-Service, along with their keys:
230   </td>
231 </tr>
232 <tr>
233   <td><form><input type="button" value="List Stylesheets" onClick="top.result.location.replace(getUwoboURL() + 'list')"/></form></td>
234 </tr>
235 </table>
236
237 <br />
238
239 </div>
240
241 <a name="stylesheets"/>
242 <table border="0" width="100%" cellpadding="4" cellspacing="0">
243 <tr>
244   <td class="head" align="left"><big>Stylesheet Management</big></td>
245   <td class="back" align="right"><a href="#top">top</a></td>
246 </tr>
247 </table>
248
249 <div id="indent">
250
251 <br />
252
253 In this section you can add, remove and reload stylesheet into the server. There are
254 some frequently used stylesheets whose URIs and keys can be automatically filled in
255 by selecting one of the options of the box below. Note that for such stylesheets
256 the getter is used by default (you can deselect it, however):
257
258 <br /><br 7>
259
260 <table border="0">
261 <tr>
262   <th align="left">Predefined Stylesheets</th>
263 </tr>
264 <tr>
265   <td>
266     <form name="predefinedStylesheets">
267       <select size="1" onChange="selectPredefinedStylesheet(this)">
268         <option value="">---</option>
269         <option value="C1,rootcontent.xsl,true">CIC ==&gt; MathML Content</option>
270         <option value="TC1,objtheorycontent.xsl,true">CIC ==&gt; MathML Content (Show only the thesis)</option>
271         <option value="C2,annotatedpres.xsl,true">MathML Content ==&gt; MathML Presentation</option>
272         <option value="T1,theory_content.xsl,true">Theory CIC ==&gt; MathML Content</option>
273         <option value="T2,theory_pres.xsl,true">Theory Content ==&gt; MathML Presentation</option>
274         <option value="E,expandobj.xsl,true">Expander</option>
275         <option value="G,genmmlid.xsl,true">MathML Content ==&gt; MathML Content + IDs</option>
276         <option value="HC2,content_to_html.xsl,true">MathML Content ==&gt; HTML</option>
277         <option value="L,link.xsl,true">Resolve links</option>
278         <option value="d_c,drop_coercions.xsl,true">Drop implicit coercions</option>
279         <option value="meta_theory,mk_meta_theory.xsl,true">Metadata (back-pointers) to theory</option>
280         <option value="L2H,ls2html.xsl,true">Getter LS ==&gt; HTML</option>
281         <option value="GP,getParam.xsl,true">Get Param</option>
282         <option value="RT,resolve_topurl.xsl,true">Logic-sheet to substitute the interface URL</option>
283         <option value="MC,metadataControl.xsl,true">Stylesheet to create links to metadata</option>
284         <option value="MGL,makeGraphLinks.xsl,true">Add hyperlink menus to graphs</option>
285         <option value="MMG,mk_meta_graph.xsl,true">Make graph of backward dependencies</option>
286         <option value="MDG,mk_dep_graph.xsl,true">Make graph of dependencies</option>
287         <option value="HAT,hanane_textedepreuve2omdoc.xsl,true">Proof-Trees ==&gt; OMDoc</option>
288         <option value="HAO,hanane_omdoc2xhtml.xsl,true">OMDoc ==&gt; XHTML+MathML</option>
289       </select>
290     </form>
291   </td>
292   <td>
293     <form>
294       <input type="button" value="Load All Predefined" onClick="loadAllPredefined()"/>
295     </form>
296   </td>
297   <td>
298     <form>
299       <input type="button" value="Remove All Predefined" onClick="removeAllPredefined()"/>
300     </form>
301   </td>
302 </tr>
303 </table>
304
305 Here you have to identify a stylesheet by means of a relative or absolute URI. Usually
306 you will specify a relative URI when using the getter to retrieve the stylesheet.
307 Moreover, you can specify a key associated to this stylesheet, so that it will be easier to
308 refer to it in subsequent operations. If escaping is enabled, then the stylesheet URI will
309 be escaped. This might be particularly useful if the stylesheet is loaded by the getter.
310
311 <br /><br />
312
313 <table border="0">
314 <tr>
315   <th align="left">Stylesheet</th>
316   <th align="left">Key</th>
317   <th align="left">Use Getter</th>
318   <th align="left">Escape</th>
319 </tr>
320 <tr>
321   <td>
322     <form name="stylesheetURI">
323       <input type="text" size="50"/>
324     </form>
325   </td>
326   <td>
327     <form name="stylesheetKey">
328       <input type="text" size="10"/>
329     </form>
330   </td>
331   <td>
332     <form name="loadUseGetter">
333       <input type="checkbox" checked="true"/>
334     </form>
335   </td>
336   <td>
337     <form name="loadEscape">
338       <input type="checkbox" checked="true"/>
339     </form>
340   </td>
341   <td>
342     <form>
343       <input type="button" value="Load" onClick="loadStylesheet()"/>
344     </form>
345   </td>
346   <td>
347     <form>
348       <input type="button" value="Reload" onClick="reloadStylesheet()"/>
349     </form>
350   </td>
351   <td>
352     <form>
353       <input type="button" value="Remove" onClick="removeStylesheet()"/>
354     </form>
355   </td>
356 </tr>
357 </table>
358
359 Use the buttons below to remove or reload <i>all</i> the stylesheets.
360 Use these commands with
361 care, and remember that UWOBO can be shared among different users:
362
363 <br /><br />
364
365 <table border="0">
366 <tr>
367   <td>
368     <form>
369       <input type="button" value="Remove All" onClick="removeAllStylesheets()"/>
370     </form>
371   </td>
372   <td>
373     <form>
374       <input type="button" value="Reload All" onClick="reloadAllStylesheets()"/>
375     </form>
376   </td>
377 </tr>
378 </table>
379 </div>
380
381 <a name="process"/>
382 <table border="0" width="100%" cellpadding="4" cellspacing="0">
383 <tr>
384   <td class="head" align="left"><big>Processing</big></td>
385   <td class="back" align="right"><a href="#top">top</a></td>
386 </tr>
387 </table>
388
389 <div id="indent">
390
391 <br />
392
393 You can use the &quot;Apply&quot; command to perform a transformation. Specify the URI of the source
394 document in the form below. The URI can be relative or absolute (in the former case you
395 will probably want to enable the use of the getter).
396 If escaping is enabled, then special characters are escaped. This might be particularly useful
397 if the source is loaded by the getter.
398
399 <br /><br />
400
401 <table border="0">
402 <tr>
403   <th align="left">Source Document</th>
404   <th align="left">Escape</th>
405 </tr>
406 <tr>
407   <td>
408     <form name="sourceDocument">
409       <input type="text" size="50"/>
410     </form>
411   </td>
412   <td>
413     <form name="escapeSource">
414       <input type="checkbox" checked="true"/>
415     </form>
416   </td>
417 </tr>
418 </table>
419
420 You can specify a sequence of zero or more parameters separated by blanks. Each
421 parameter is made of a name immediately followed by <tt>=</tt> and then a value.
422 If &quot;Escape&quot; is checked, then parameters are escaped in the final
423 URI.
424
425 <br /><br />
426
427 <table border="0">
428 <tr>
429   <th align="left">Parameters (optional)</th>
430   <th align="left">Escape</th>
431 </tr>
432 <tr>
433   <td>
434     <form name="parameters">
435       <input type="text" size="50"/>
436     </form>
437   </td>
438   <td>
439     <form name="escapeParameters">
440       <input type="checkbox" checked="true"/>
441     </form>
442   </td>
443 </tr>
444 </table>
445
446 In the key list specify a list of keys
447 separated by blanks. This is the list of stylesheets to be applied in sequence to the
448 source document.
449 When ready, click on the button and have fun!
450
451 <br /><br />
452
453 <table border="0">
454 <tr>
455   <th align="left">Key list</th>
456   <th align="left">Use Getter</th>
457 </tr>
458 <tr>
459   <td>
460     <form name="keyList">
461       <input type="text" size="50"/>
462     </form>
463   </td>
464   <td>
465     <form name="applyUseGetter">
466       <input type="checkbox" checked="true"/>
467     </form>
468   </td>
469   <td>
470     <form>
471       <input type="button" value="Apply" onClick="applyStylesheets()"/>
472     </form>
473   </td>
474 </tr>
475 </table>
476
477 </div>
478
479 <table border="0" width="100%" cellpadding="4" cellspacing="0">
480 <tr>
481   <td class="back" align="left">Page maintained by: <a href="http://www.cs.unibo.it/~lpadovan">Luca Padovani</a></td>
482   <td class="back" align="right"><a href="#top">top</a></td>
483 </tr>
484 </table>
485
486 </body>
487
488 </html>
489