From 6ef524e4ce0449ead8dec0f28b85c96f65bd69b4 Mon Sep 17 00:00:00 2001 From: Matt Pass Date: Thu, 19 Apr 2012 17:47:49 +0100 Subject: [PATCH] Themes applied to editor & styling made more general Some of the general styling moved from default theme to here (margin on HTML & body, plus selected, gutter, cursor & matching styles) Removed setting of theme here, done dynamically with existing functions --- editor.php | 29 ++++++++++++++++++++--------- 1 file changed, 20 insertions(+), 9 deletions(-) diff --git a/editor.php b/editor.php index 8520e8d..30ec075 100644 --- a/editor.php +++ b/editor.php @@ -1,6 +1,6 @@ - + CodeMirror 2: ICE Coders Editor of Choice @@ -15,30 +15,41 @@ - +'; +} else { + echo ''; +} +?> - +