more explicit markup for improper commands;
clarified CSS rendering;

--- a/etc/isabelle.css	Wed Dec 10 10:44:56 2014 +0100
+++ b/etc/isabelle.css	Wed Dec 10 13:45:44 2014 +0100
@@ -44,9 +44,6 @@
 .verbatim       { color: #6600CC; }
 .cartouche      { color: #CC6600; }
 .comment        { color: #CC0000; }
-.control        { background-color: #FF6A6A; }
+.improper       { color: #FF5050; }
 .bad            { background-color: #FF6A6A; }
 
-.keyword1       { font-weight: bold; }
-.keyword2       { font-weight: bold; }
-

--- a/src/Pure/Isar/keyword.ML	Wed Dec 10 10:44:56 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Dec 10 13:45:44 2014 +0100
@@ -51,6 +51,7 @@
   val is_document_raw: keywords -> string -> bool
   val is_document: keywords -> string -> bool
   val is_theory_begin: keywords -> string -> bool
+  val is_theory_end: keywords -> string -> bool
   val is_theory_load: keywords -> string -> bool
   val is_theory: keywords -> string -> bool
   val is_theory_body: keywords -> string -> bool
@@ -60,6 +61,8 @@
   val is_proof_goal: keywords -> string -> bool
   val is_qed: keywords -> string -> bool
   val is_qed_global: keywords -> string -> bool
+  val is_proof_asm: keywords -> string -> bool
+  val is_improper: keywords -> string -> bool
   val is_printed: keywords -> string -> bool
 end;
 
@@ -217,6 +220,7 @@
 val is_document = command_category [document_heading, document_body, document_raw];
 
 val is_theory_begin = command_category [thy_begin];
+val is_theory_end = command_category [thy_end];
 
 val is_theory_load = command_category [thy_load];
 
@@ -239,6 +243,9 @@
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
+val is_proof_asm = command_category [prf_asm, prf_asm_goal];
+val is_improper = command_category [qed_script, prf_script, prf_asm_goal_script];
+
 fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
 
 end;

--- a/src/Pure/Isar/token.ML	Wed Dec 10 10:44:56 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 10 13:45:44 2014 +0100
@@ -60,8 +60,8 @@
   val content_of: T -> string
   val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
-  val report: Keyword.keywords -> T -> Position.report_text
-  val markup: Keyword.keywords -> T -> Markup.T
+  val reports: Keyword.keywords -> T -> Position.report_text list
+  val markups: Keyword.keywords -> T -> Markup.T list
   val unparse: T -> string
   val unparse_src: src -> string list
   val print: T -> string
@@ -305,15 +305,13 @@
   | Error msg => (Markup.bad, msg)
   | _ => (Markup.empty, "");
 
-fun keyword_report tok markup = ((pos_of tok, markup), "");
+fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
 
-fun command_markup keywords x =
-  (case Keyword.command_kind keywords x of
-    SOME k =>
-      if k = Keyword.thy_end then Markup.keyword2
-      else if k = Keyword.prf_asm orelse k = Keyword.prf_asm_goal then Markup.keyword3
-      else Markup.keyword1
-  | NONE => Markup.keyword1);
+fun command_markups keywords x =
+  if Keyword.is_theory_end keywords x then [Markup.keyword2]
+  else if Keyword.is_proof_asm keywords x then [Markup.keyword3]
+  else if Keyword.is_improper keywords x then [Markup.keyword1, Markup.improper]
+  else [Markup.keyword1];
 
 in
 
@@ -325,16 +323,16 @@
   then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
   else [];
 
-fun report keywords tok =
+fun reports keywords tok =
   if is_command tok then
-    keyword_report tok (command_markup keywords (content_of tok))
+    keyword_reports tok (command_markups keywords (content_of tok))
   else if is_kind Keyword tok then
-    keyword_report tok (keyword_markup (false, Markup.keyword2) (content_of tok))
+    keyword_reports tok [keyword_markup (false, Markup.keyword2) (content_of tok)]
   else
     let val (m, text) = token_kind_markup (kind_of tok)
-    in ((pos_of tok, m), text) end;
+    in [((pos_of tok, m), text)] end;
 
-fun markup keywords = #2 o #1 o report keywords;
+fun markups keywords = map (#2 o #1) o reports keywords;
 
 end;
 
@@ -353,18 +351,18 @@
 
 fun unparse_src (Src {args, ...}) = map unparse args;
 
-fun print tok = Markup.markup (markup Keyword.empty_keywords tok) (unparse tok);
+fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
 
 fun text_of tok =
   let
     val k = str_of_kind (kind_of tok);
-    val m = markup Keyword.empty_keywords tok;
+    val ms = markups Keyword.empty_keywords tok;
     val s = unparse tok;
   in
     if s = "" then (k, "")
     else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
-    then (k ^ " " ^ Markup.markup m s, "")
-    else (k, Markup.markup m s)
+    then (k ^ " " ^ Markup.markups ms s, "")
+    else (k, Markup.markups ms s)
   end;
 
 
@@ -455,7 +453,7 @@
   | SOME (Term t) => Syntax.pretty_term ctxt t
   | SOME (Fact (_, ths)) =>
       Pretty.enclose "(" ")" (Pretty.breaks (map (Pretty.backquote o Display.pretty_thm ctxt) ths))
-  | _ => Pretty.mark_str (markup Keyword.empty_keywords tok, unparse tok));
+  | _ => Pretty.marks_str (markups Keyword.empty_keywords tok, unparse tok));
 
 fun pretty_src ctxt src =
   let
@@ -468,6 +466,7 @@
   in Pretty.block (Pretty.breaks (prt_name :: map prt_arg args)) end;
 
 
+
 (** scanners **)
 
 open Basic_Symbol_Pos;

--- a/src/Pure/PIDE/markup.ML	Wed Dec 10 10:44:56 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Dec 10 13:45:44 2014 +0100
@@ -202,6 +202,7 @@
   val output: T -> Output.output * Output.output
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
+  val markups: T list -> string -> string
   val markup_only: T -> string
   val markup_report: string -> string
 end;
@@ -645,6 +646,8 @@
   let val (bg, en) = output m
   in Library.enclose (Output.escape bg) (Output.escape en) end;
 
+val markups = fold_rev markup;
+
 fun markup_only m = markup m "";
 
 fun markup_report "" = ""

--- a/src/Pure/Thy/thy_syntax.ML	Wed Dec 10 10:44:56 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Dec 10 13:45:44 2014 +0100
@@ -32,7 +32,7 @@
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
-    val reports = Token.report keywords tok :: Token.completion_report tok @ malformed_symbols;
+    val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
 
 in
@@ -44,7 +44,7 @@
 end;
 
 fun present_token keywords tok =
-  Markup.enclose (Token.markup keywords tok) (Output.output (Token.unparse tok));
+  fold_rev Markup.enclose (Token.markups keywords tok) (Output.output (Token.unparse tok));
 
 fun present_span keywords = implode o map (present_token keywords) o Command_Span.content;
 

--- a/src/Tools/jEdit/src/rendering.scala	Wed Dec 10 10:44:56 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Dec 10 13:45:44 2014 +0100
@@ -53,11 +53,8 @@
     import JEditToken._
     Map[String, Byte](
       Keyword.THY_END -> KEYWORD2,
-      Keyword.QED_SCRIPT -> DIGIT,
-      Keyword.PRF_SCRIPT -> DIGIT,
       Keyword.PRF_ASM -> KEYWORD3,
-      Keyword.PRF_ASM_GOAL -> KEYWORD3,
-      Keyword.PRF_ASM_GOAL_SCRIPT -> DIGIT
+      Keyword.PRF_ASM_GOAL -> KEYWORD3
     ).withDefaultValue(KEYWORD1)
   }