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
index c4226ea99ec52458d46c5489e604dc4091207f51..11ced417926c5ae9d39309931ce68e24b8f0852a 100644 (file)
@@ -1,14 +1,31 @@
 <!DOCTYPE html>
 <html>
 <head>
+  <!--all elements like "${}" is replaced by real values while loading page in StudyBrowser-->
+
+  <!--suppress HtmlUnknownTarget -->
   <link rel="stylesheet" href="${css_oldcodemirror}">
+  <!--suppress HtmlUnknownTarget -->
   <link rel="stylesheet" href="${css_codemirror}">
+  <!--suppress HtmlUnknownTarget -->
   <script src="${codemirror}"></script>
+  <!--suppress HtmlUnknownTarget -->
   <script src="${colorize}"></script>
+  <!--suppress HtmlUnknownTarget -->
   <script src="${runmode}"></script>
+  <!--suppress HtmlUnknownTarget -->
   <script src="${highlight_mode}"></script>
+  <!--suppress HtmlUnknownTarget -->
   <script src="${javascript}"></script>
+  <!--suppress HtmlUnknownTarget -->
   <script src="${python}"></script>
+  <!--suppress CssInvalidPropertyValue -->
+  <style media="screen" type="text/css">
+    body {
+      font-size: ${font_size}pt !important;
+    }
+
+  </style>
 </head>
 <body>
 ${code}