The following are global parameters used by all the other section to contact the UWOBO service and possibly a Getter. The Getter is not required for some operations and can be excluded by unchecking the proper buttons below.

The following is the URL used to contact the UWOBO Web-Service. localhost is relative to your machine.

UWOBO URL
	--- localhost marcello phd eolo helm

The following is the URL used to contact the getter. The getter is usually launched manually. In all cases except for the check button below, localhost is relative to the host running UWOBO, because the getter URL is sent as a parameter along with UWOBO commands. In other words, localhost is the host running UWOBO and not your machine.

Getter URL
	--- localhost marcello phd eolo

You can start a new daemon on a given port. The new daemon will have an empty list of processed stylesheets.

Port

You can also kill the daemon. The log file will be mantained.

The following are commands to do some simple queries about the UWOBO service.

Retrieve the version of the UWOBO service running at the UWOBO URL and list the syntax of the accepted commands. You can use this button to verify that a UWOBO service is actually running there:

Ask UWOBO for a list of the stylesheets currently compiled inside the Web-Service, along with their keys:

The following are commands to list and edit the UWOBO profiles.

List existent profiles.

Create a new profile.

Name	Parent profile	Parent profile password

Remove a profile.

Name	Password

Show profile parameters.

Name	Password

Set profile parameters.

Name	Password	Parameter name	Parameter value

In this section you can add, remove and reload stylesheet into the server. There are some frequently used stylesheets whose URIs and keys can be automatically filled in by selecting one of the options of the box below. Note that for such stylesheets the getter is used by default (you can deselect it, however):

Predefined Stylesheets
--- CIC ==> MathML Content CIC ==> MathML Content (Show only the thesis) MathML Content ==> MathML Presentation Theory CIC ==> MathML Content Theory Content ==> MathML Presentation Expander MathML Content ==> MathML Content + IDs MathML Content ==> HTML Resolve links Drop implicit coercions Metadata (back-pointers) to theory Getter LS ==> Theory Get Param Logic-sheet to substitute the interface URL Call the search engine Stylesheet to create links to metadata Add hyperlink menus to graphs Make graph of backward dependencies Make graph of dependencies Proof-Trees ==> OMDoc OMDoc ==> XHTML+MathML Substitute UWOBO keys

Here you have to identify a stylesheet by means of a relative or absolute URI. Usually you will specify a relative URI when using the getter to retrieve the stylesheet. Moreover, you can specify a key associated to this stylesheet, so that it will be easier to refer to it in subsequent operations. If escaping is enabled, then the stylesheet URI will be escaped. This might be particularly useful if the stylesheet is loaded by the getter.

Stylesheet	Key	Use Getter	Escape

Use the buttons below to remove or reload all the stylesheets. Use these commands with care, and remember that UWOBO can be shared among different users:

You can use the "Apply" command to perform a transformation. Specify the URI of the source document in the form below. The URI can be relative or absolute (in the former case you will probably want to enable the use of the getter). If escaping is enabled, then special characters are escaped. This might be particularly useful if the source is loaded by the getter.

Source Document	Escape

You can specify a sequence of zero or more parameters separated by blanks. Each parameter is made of a name immediately followed by = and then a value. If "Escape" is checked, then parameters are escaped in the final URI.

Parameters (optional)	Escape

In the key list specify a list of keys separated by blanks. This is the list of stylesheets to be applied in sequence to the source document. When ready, click on the button and have fun!

Key list	Use Getter