Add banner for clean.js; show banners everywhere; sans-serif in /src and /doc

300b9ec3 · Camil Staps · 503348d5 · 300b9ec3 · 300b9ec3 · 300b9ec3
Verified Commit 300b9ec3 authored Jul 03, 2018 by Camil Staps ⚽
7 changed files
--- a/frontend/banners.json
+++ b/frontend/banners.json
@@ -17,5 +17,11 @@
 		"from": "Wed, 2 May 2018 10:30:00 UTC",
 		"until": "Wed, 2 May 2018 13:30:00 UTC",
 		"useragent": "/SEB/"
+	},
+	{
+		"id": "clean.js2018",
+		"text": "We no longer use the unmainted <a href='http://pygments.org' target='_blank'>Pygments</a> library for highlighting and have moved to <a href='https://github.com/clean-cloogle/clean.js' target='_blank'>clean.js</a>. Please <a href='https://github.com/clean-cloogle/clean.js/issues/new' target='_blank'>report</a> any issues you see!",
+		"from": "Tue, 3 Jul 2018 00:00:00 UTC",
+		"until": "Tue, 10 Jul 2018 00:00:00 UTC"
 	}
 ]
--- a/frontend/banners.php
+++ b/frontend/banners.php
+<?php
+$banners = json_decode(file_get_contents(__DIR__ . '/banners.json'), true);
+foreach ($banners as $banner) {
+	$from = strtotime($banner['from']);
+	$until = strtotime($banner['until']);
+	if ($from > time() || $until < time())
+		continue;
+	if (isset($banner['useragent']) && !preg_match($banner['useragent'], $_SERVER['HTTP_USER_AGENT']))
+		continue;
+	echo "<div " .
+		"class='banner' " .
+		"data-id='{$banner['id']}' " .
+		"data-from='{$banner['from']}' " .
+		"data-until='{$banner['until']}'>" .
+		"<span id='{$banner['id']}'>{$banner['text']}</span>" .
+		"</div>";
+}
--- a/frontend/common.css
+++ b/frontend/common.css
+body {
+	color: #222;
+	font-family: sans-serif;
+	margin: 0 0 1em;
+}
+
 body.framelike {
 	margin: 0;
 	height: 100vh;
+	overflow: hidden;
 }

 body.framelike #logo {
@@ -134,6 +141,10 @@ a.more-info {
 	padding-left: .5em;
 }

+#sidebar br:last-child, #viewer br:last-child {
+	margin-top: 8em;
+}
+
 #viewer {
 	height: 100%;
 	overflow: auto;

--- a/frontend/doc/index.php
+++ b/frontend/doc/index.php
@@ -25,7 +25,7 @@

 		#sidebar h3 {
 			background: none;
-			font-family: serif;
+			font-family: sans-serif;
 			font-size: 1.17em;
 			font-weight: bold;
 			line-height: 22px;
@@ -43,6 +43,7 @@
 	</style>
 </head>
 <body class="framelike">
+	<?php include('../banners.php'); ?>
 	<div id="sidebar">
 		<a href="/"><img id="logo" src="../logo.png" alt="Cloogle logo"/></a>
 		<h3>Documentation browser</h3>

--- a/frontend/frontend.css
+++ b/frontend/frontend.css
-body {
-	color: #222;
-	font-family: sans-serif;
-	margin: 0 0 1em;
-}
-
 td, th {
 	vertical-align: top;
 }

--- a/frontend/index.php
+++ b/frontend/index.php
@@ -15,24 +15,7 @@
 	<link rel="stylesheet" href="frontend.css" type="text/css"/>
 </head>
 <body>
-	<?php
-		$banners = json_decode(file_get_contents('banners.json'), true);
-		foreach ($banners as $banner) {
-			$from = strtotime($banner['from']);
-			$until = strtotime($banner['until']);
-			if ($from > time() || $until < time())
-				continue;
-			if (isset($banner['useragent']) && !preg_match($banner['useragent'], $_SERVER['HTTP_USER_AGENT']))
-				continue;
-			echo "<div " .
-				"class='banner' " .
-				"data-id='{$banner['id']}' " .
-				"data-from='{$banner['from']}' " .
-				"data-until='{$banner['until']}'>" .
-				"<span id='{$banner['id']}'>{$banner['text']}</span>" .
-				"</div>";
-		}
-	?>
+	<?php include('banners.php'); ?>
 	<div id="header">
 		<div id="logo">
 			<a href="https://github.com/clean-cloogle/cloogle.org">

--- a/frontend/src/index.php
+++ b/frontend/src/index.php
@@ -15,6 +15,7 @@
 	<link rel="stylesheet" href="view.css" type="text/css"/>
 </head>
 <body class="framelike">
+	<?php include('../banners.php'); ?>
 	<div id="sidebar">
 		<a href="/"><img id="logo" src="../logo.png" alt="Cloogle logo"/></a>
 		<h3>Library browser</h3>