Fix #EDU-526 Set task description font size depends on editor font size Change fonts...
[idea/community.git] / python / educational-core / student / resources / code-mirror / template.html
1 <!DOCTYPE html>
2 <html>
3 <head>
4   <!--all elements like "${}" is replaced by real values while loading page in StudyBrowser-->
5
6   <!--suppress HtmlUnknownTarget -->
7   <link rel="stylesheet" href="${css_oldcodemirror}">
8   <!--suppress HtmlUnknownTarget -->
9   <link rel="stylesheet" href="${css_codemirror}">
10   <!--suppress HtmlUnknownTarget -->
11   <script src="${codemirror}"></script>
12   <!--suppress HtmlUnknownTarget -->
13   <script src="${colorize}"></script>
14   <!--suppress HtmlUnknownTarget -->
15   <script src="${runmode}"></script>
16   <!--suppress HtmlUnknownTarget -->
17   <script src="${highlight_mode}"></script>
18   <!--suppress HtmlUnknownTarget -->
19   <script src="${javascript}"></script>
20   <!--suppress HtmlUnknownTarget -->
21   <script src="${python}"></script>
22   <!--suppress CssInvalidPropertyValue -->
23   <style media="screen" type="text/css">
24     body {
25       font-size: ${font_size}pt !important;
26     }
27
28   </style>
29 </head>
30 <body>
31 ${code}
32 <script>
33   var nodeList = document.body.getElementsByTagName("code");
34   CodeMirror.colorize(nodeList, "text/x-java")
35   CodeMirror.colorize();
36 </script>
37 </body>
38 </html>