remove unnecessary js lang files from prettify, update styles for prettify

1 files changed, 10 insertions, 9 deletions

diff --git a/docs/assets/js/google-code-prettify/prettify.css b/docs/assets/js/google-code-prettify/prettify.css
index 579bf085a..da6b6e7e1 100644
--- a/docs/assets/js/google-code-prettify/prettify.css
+++ b/docs/assets/js/google-code-prettify/prettify.css
@@ -6,20 +6,21 @@
 .kwd, .tag { color: #195f91; }
 .typ, .atn, .dec, .var { color: #CB4B16; }
 .pln { color: #93a1a1; }
-pre.prettyprint { border: 1px solid #888; padding: 2px; }
-ol.linenums { margin-top: 0; margin-bottom: 0; }
-li.L0, li.L1, li.L2, li.L3, li.L5, li.L6, i.L7, li.L8 { list-style-type: none; }
-li.L1, li.L3, li.L5, li.L7, li.L9 { background-color: #fdf6e3; }
-
-.prettyprint {
-  background: #fefbf3 !important;
-  padding: 9px !important;
-  border: 1px solid rgba(0,0,0,.2) !important;
+pre.prettyprint {
+  background: #fefbf3;
+  padding: 9px;
+  border: 1px solid rgba(0,0,0,.2);
   -webkit-box-shadow: 0 1px 2px rgba(0,0,0,.1);
   -moz-box-shadow: 0 1px 2px rgba(0,0,0,.1);
   box-shadow: 0 1px 2px rgba(0,0,0,.1);
 }
 
+/* Specify class=linenums on a pre to get line numbering */
+ol.linenums { margin: 0 0 0 40px; } /* IE indents via margin-left */
+ol.linenums li { color: rgba(0,0,0,.15); line-height: 20px; }
+/* Alternate shading for lines */
+li.L1, li.L3, li.L5, li.L7, li.L9 {  }
+
 /*
 $base03:    #002b36;
 $base02:    #073642;