1 <?xml version="1.0" encoding="UTF-8"?>
3 <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "DTD/xhtml1-strict.dtd">
6 <html xmlns:subst="http://www.cs.unibo.it/helm/subst">
8 <title>Control panel</title>
9 <!-- Note: <subst:script/> are substitued by the stylesheet with <script /> -->
10 <!-- after changing @src in the concatenation of the interface URL with @src -->
11 <subst:script language="JavaScript" src="/javascript/defaults.js" />
12 <subst:script language="JavaScript" src="/javascript/utils.js" />
13 <subst:script language="JavaScript" src="/javascript/control.js" />
15 <body bgcolor="#ffffff" text="#000000">
23 <select name="output" onChange="updateOutput(this,document.forms[0].format)">
25 var mode = getParam2('mode');
26 var mode_list = mode.split(',');
27 outputOption(document, "processed", "Processed", mode_list[0]);
28 outputOption(document, "raw", "Raw", mode_list[0]);
33 <select name="format" onChange="updateFormat(this)">
35 var mode = getParam2('mode');
36 var mode_list = mode.split(',');
37 if (mode_list[0] == "raw") {
38 outputOption(document, "cic", "CIC", mode_list[1]);
39 outputOption(document, "types", "TYPES", mode_list[1]);
40 outputOption(document, "ann", "ANN", mode_list[1]);
42 outputOption(document, "html", "HTML", mode_list[2]);
43 outputOption(document, "mml_cont", "MathML Content", mode_list[2]);
44 outputOption(document, "mml_pres", "MathML Presentation", mode_list[2]);
52 document.write('<a target="_top" href="' +
53 getParam2('topurl') + '/html/library/index.html' +
54 '" onClick="refreshReload()">Reload</a>');
58 (do it also before attempting to take a link to the current page)
61 top.processorURL = getParam2('processorURL');
62 top.getterURL = getParam2('getterURL');
63 top.UNICODEvsSYMBOL = getParam2('UNICODEvsSYMBOL');
64 top.topurl = getParam2('topurl');
65 top.mode = getParam2('mode');
66 top.cicuri = getParam2('cicuri');
67 top.theoryuri = getParam2('theoryuri');
76 var mode = getParam2('mode');
77 var mode_list = mode.split(',');
78 if (mode_list[0] == "raw") {
79 outputCheckbox(document, "updateCompressed(this)",
80 " Compressed", mode_list[5] == "gz");
81 outputCheckbox(document, "updateDTDPatched(this)",
82 " Resolve DTD URL", mode_list[6] == "yes");
84 outputCheckbox(document, "updateNatural(this)",
85 " Natural Language", mode_list[3] == "yes");
86 outputCheckbox(document, "updateAnnotations(this)",
87 " Annotations", mode_list[4] == "yes");
95 document.write('<a target="_top" href=""' +
96 ' onClick="refreshReload()">Configuration Panel</a>');