]> matita.cs.unibo.it Git - helm.git/blob - helm/on-line/html/cic/control.html
ocaml 3.09 transition
[helm.git] / helm / on-line / html / cic / control.html
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
2 "http://www.w3.org/TR/REC-html40/loose.dtd">
3 <html xmlns="http://www.w3.org/1999/xhtml" xmlns:subst="http://www.cs.unibo.it/helm/subst">
4
5 <head>
6
7 <style type="text/css">
8 #normal { background-color: #e6e6fa; font-family: sans-serif }
9 td.head { font-weight: bold; background-color: #e6e6fa; color: brown }
10 td.back { background-color: #e6e6fa; color: brown }
11 #indent { margin-left: 1cm; margin-right: 1cm }
12 ul.control { padding-left: 1em; list-style: none; }
13 ul.control2 { font-size: small; padding-left: 2em; }
14 div.center { text-align: center }
15 h2.uri { margin-top: 0ex; margin-bottom: 0ex }
16 </style>
17
18 <script>
19  var annotations="<subst:annotations/>";
20  var CICURI="<subst:CICURI/>";
21  var cleanCICURI="<subst:cleanCICURI/>";
22  var CICURL = "<subst:CICURL/>";
23  var DCRDFURL = "<subst:DCRDFURL/>";
24  var DirectRDFURL = "<subst:DirectRDFURL/>";
25  var getterURL = "<subst:getterURL/>";
26  var HTMLURL = "<subst:HTMLURL/>";
27  var ProofTreeURL = "<subst:makeProofTreeURL/>";
28  var InverseRDFURL = "<subst:InverseRDFURL/>";
29  var MathMLContentURL = "<subst:MathMLContentURL/>";
30  var MathMLPresentationURL = "<subst:MathMLPresentationURL/>";
31  var interfaceURL = "<subst:interfaceURL/>";
32  var mkDirDepURL = "<subst:makeDirectDependencyURL/>";
33  var mkInvDepURL = "<subst:makeInverseDirectDependencyURL/>";
34  var mkInvRecDepURL = "<subst:makeInverseRecDependencyURL/>";
35  var mkRecDepURL = "<subst:makeRecDependencyURL/>";
36  var processorURL = "<subst:processorURL/>";
37  var profile = "<subst:profile/>";
38  var proofcheckerURL = "<subst:proofcheckerURL/>";
39  var url = "<subst:url/>";
40 </script>
41 </head>
42
43 <body id="normal">
44  <div class="center">
45  <small>
46  User:
47    <uwobo:profileCtrlOptionList xmlns:uwobo="http://helm.cs.unibo.it/uwobo"
48     type="cic"/>
49  <br />
50  [<a href="http://helm.cs.unibo.it" target="_top">HELM home</a>]
51  <script>
52    document.write('[<a target="_top" href="' + processorURL +
53      'apply?keys=SPK&amp;param.processorURL=' + escape(processorURL) +
54      '&amp;param.profile=' + escape(profile) +
55      '&amp;xmluri=' + interfaceURL + 'html/configuration.html' +
56      '">configuration</a>]');
57  </script>
58  </small>
59  </div>
60  <hr />
61  <div class="center">
62    <script>
63      document.write('&lt;a target="result" style="color:black; text-decoration:none" href="' + url + '">');
64      document.write('<img style="border-style:none" src="' + interfaceURL + '/icons/object.png" />');
65    </script>
66   <h2 class="uri"><subst:base_CICURI/></h2>
67   <script>document.write('&lt;/a>');</script>
68  </div>
69  <hr />
70 <!--
71   [Annotations are <script>if (annotations) == 'no') document.write('off'); else document.write('on')</script>]
72 -->
73 <ul class="control">
74 <!--
75   <li>
76     <script>
77      var url = "<subst:url/>";
78      document.write('<a href="' + url + '" target="_blank">Open object in new window</a>');
79      </script>
80   </li>
81 -->
82   <li>
83     View
84     <script>
85      document.write('[ <a href="' + HTMLURL + '&amp;param.toplevel=true" target="result"><small>HTML</small></a>');
86      document.write(' | ');
87      document.write('<a href="' + MathMLPresentationURL + '&amp;param.toplevel=true" target="result"><small>MathML</small></a> ]');
88      </script>
89   </li>
90   <li>
91     <script>
92       document.write('<a href="' + ProofTreeURL + '&amp;param.toplevel=true" target="result">View proof tree</a>');
93     </script>
94   </li>
95   <li>
96     <script>
97      var url = processorURL + "apply?keys=MC%2CRT%2CL&amp;xmluri=" +
98          getterURL + "getxml%3Furi%3D" + cleanCICURI +
99          "&amp;prop.media-type=text/html&amp;prop.encoding=iso-8859-1" +
100          "&amp;param.CICURI=" + cleanCICURI + "&amp;param.profile=" + profile +
101          "&amp;profile=" + profile;
102      document.write(
103       '<a target="result" href="' + url + '">View metadata</a>'
104      );
105     </script>
106   </li>
107   <li>
108     <script>
109      url = proofcheckerURL + "proofCheck?uri=" + cleanCICURI;
110      document.write(
111       '<a target="result" href="' + url + '">Proof check</a>'
112      );
113     </script>
114   </li>
115   <li>
116     Analyse dependencies
117     <ul class="control2">
118       <li>
119         <script>
120           document.write('<a target="result" href="' + mkDirDepURL + '">direct</a>');
121         </script>
122       </li>
123       <li>
124         <script>
125           document.write('<a target="result" href="' + mkInvDepURL + '">inverse</a>');
126         </script>
127       </li>
128       <li>
129         <script>
130           document.write('<a target="result" href="' + mkRecDepURL + '">recursive direct</a> (graph)');
131         </script>
132       </li>
133       <li>
134         <script>
135           document.write('<a target="result" href="' + mkInvRecDepURL + '">recursive inverse</a> (graph)');
136         </script>
137       </li>
138     </ul>
139   </li>
140 </ul>
141 <hr />
142 <ul class="control">
143   <li> Download
144     <ul class="control2">
145       <li>
146         <script>
147          document.write('<a href="' + CICURL + '" target="result">CIC XML</a>');
148         </script>
149           </li>
150       <li>
151         <script>
152          document.write('<a href="' + MathMLContentURL + '" target="result">MathML Content</a>');
153         </script>
154       </li>
155       <li>
156         <script>
157          document.write('<a href="' + MathMLPresentationURL + '" target="result">MathML Presentation</a>');
158         </script>
159       </li>
160       <li>
161         <script>
162          document.write('<a href="' + HTMLURL + '" target="result">HTML</a>');
163         </script>
164       </li>
165     </ul>
166   </li>
167   <li>
168     Download metadata
169     <ul class="control2">
170       <li>
171         <script>
172           document.write('<a target="result" href="' + DirectRDFURL + '">direct dependencies</a>');
173         </script>
174       </li>
175       <li>
176         <script>
177           document.write('<a target="result" href="' + InverseRDFURL + '">inverse dependencies</a>');
178         </script>
179       </li>
180       <li>
181         <script>
182           document.write('<a target="result" href="' + DCRDFURL + '">Dublin Core</a>');
183         </script>
184       </li>
185     </ul>
186   </li>
187 </ul>
188 </body>
189 </html>