more markup for improper elements;

--- a/src/Pure/Isar/args.ML	Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Pure/Isar/args.ML	Tue Mar 18 12:25:17 2014 +0100
@@ -159,7 +159,7 @@
   (ident || Parse.token Parse.keyword) :|-- (fn tok =>
     let val y = Token.content_of tok in
       if x = y
-      then (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; Scan.succeed x)
+      then (Token.assign (SOME (Token.Literal (false, Markup.quasi_keyword))) tok; Scan.succeed x)
       else Scan.fail
     end);
 
@@ -251,7 +251,7 @@
   Parse.nat >> (fn i => fn tac => tac i) ||
   $$$ "!" >> K ALLGOALS;
 
-val goal = $$$ "[" |-- Parse.!!! (from_to --| $$$ "]");
+val goal = Parse.keyword_improper "[" |-- Parse.!!! (from_to --| Parse.keyword_improper "]");
 fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
 
 

--- a/src/Pure/Isar/parse.ML	Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Pure/Isar/parse.ML	Tue Mar 18 12:25:17 2014 +0100
@@ -38,6 +38,8 @@
   val eof: string parser
   val command_name: string -> string parser
   val keyword_with: (string -> bool) -> string parser
+  val keyword_markup: bool * Markup.T -> string -> string parser
+  val keyword_improper: string -> string parser
   val $$$ : string -> string parser
   val reserved: string -> string parser
   val semicolon: string parser
@@ -198,17 +200,20 @@
 val sync = kind Token.Sync;
 val eof = kind Token.EOF;
 
-fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
-
 fun command_name x =
   group (fn () => Token.str_of_kind Token.Command ^ " " ^ quote x)
     (RESET_VALUE (Scan.one (fn tok => Token.is_command tok andalso Token.content_of tok = x)))
   >> Token.content_of;
 
-fun $$$ x =
+fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
+
+fun keyword_markup markup x =
   group (fn () => Token.str_of_kind Token.Keyword ^ " " ^ quote x)
     (Scan.ahead not_eof -- keyword_with (fn y => x = y))
-  >> (fn (tok, x) => (Token.assign (SOME (Token.Literal Markup.quasi_keyword)) tok; x));
+  >> (fn (tok, x) => (Token.assign (SOME (Token.Literal markup)) tok; x));
+
+val keyword_improper = keyword_markup (true, Markup.improper);
+val $$$ = keyword_markup (false, Markup.quasi_keyword);
 
 fun reserved x =
   group (fn () => "reserved identifier " ^ quote x)

--- a/src/Pure/Isar/proof_context.ML	Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 18 12:25:17 2014 +0100
@@ -1204,8 +1204,9 @@
 
 fun check_case ctxt (name, pos) fxs =
   let
-    val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, _), _)) =
+    val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, is_proper), _)) =
       Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
+    val _ = if is_proper then () else Context_Position.report ctxt pos Markup.improper;
 
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
       | replace [] ys = ys

--- a/src/Pure/Isar/token.ML	Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Pure/Isar/token.ML	Tue Mar 18 12:25:17 2014 +0100
@@ -12,7 +12,7 @@
     Error of string | Sync | EOF
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   datatype value =
-    Literal of Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
+    Literal of bool * Markup.T | Text of string | Typ of typ | Term of term | Fact of thm list |
     Attribute of morphism -> attribute | Files of file Exn.result list
   type T
   val str_of_kind: kind -> string
@@ -42,7 +42,7 @@
   val inner_syntax_of: T -> string
   val source_position_of: T -> Symbol_Pos.source
   val content_of: T -> string
-  val keyword_markup: Markup.T -> string -> Markup.T
+  val keyword_markup: bool * Markup.T -> string -> Markup.T
   val completion_report: T -> Position.report_text list
   val report: T -> Position.report_text
   val markup: T -> Markup.T
@@ -87,7 +87,7 @@
 type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T};
 
 datatype value =
-  Literal of Markup.T |
+  Literal of bool * Markup.T |
   Text of string |
   Typ of typ |
   Term of term |
@@ -255,8 +255,8 @@
 
 in
 
-fun keyword_markup keyword x =
-  if Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
+fun keyword_markup (important, keyword) x =
+  if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
 
 fun completion_report tok =
   if is_kind Keyword tok
@@ -265,7 +265,7 @@
 
 fun report tok =
   if is_kind Keyword tok then
-    ((pos_of tok, keyword_markup Markup.keyword2 (content_of tok)), "")
+    ((pos_of 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;

--- a/src/Pure/PIDE/markup.ML	Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Mar 18 12:25:17 2014 +0100
@@ -105,7 +105,6 @@
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
   val commandN: string val command: T
-  val operatorN: string val operator: T
   val stringN: string val string: T
   val altstringN: string val altstring: T
   val verbatimN: string val verbatim: T
@@ -117,6 +116,8 @@
   val keyword2N: string val keyword2: T
   val keyword3N: string val keyword3: T
   val quasi_keywordN: string val quasi_keyword: T
+  val improperN: string val improper: T
+  val operatorN: string val operator: T
   val elapsedN: string
   val cpuN: string
   val gcN: string
@@ -427,6 +428,7 @@
 val (keyword2N, keyword2) = markup_elem "keyword2";
 val (keyword3N, keyword3) = markup_elem "keyword3";
 val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
+val (improperN, improper) = markup_elem "improper";
 val (operatorN, operator) = markup_elem "operator";
 val (stringN, string) = markup_elem "string";
 val (altstringN, altstring) = markup_elem "altstring";

--- a/src/Pure/PIDE/markup.scala	Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Mar 18 12:25:17 2014 +0100
@@ -216,6 +216,7 @@
   val KEYWORD2 = "keyword2"
   val KEYWORD3 = "keyword3"
   val QUASI_KEYWORD = "quasi_keyword"
+  val IMPROPER = "improper"
   val OPERATOR = "operator"
   val STRING = "string"
   val ALTSTRING = "altstring"

--- a/src/Tools/jEdit/etc/options	Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Tools/jEdit/etc/options	Tue Mar 18 12:25:17 2014 +0100
@@ -82,6 +82,7 @@
 option keyword2_color : string = "009966FF"
 option keyword3_color : string = "0099FFFF"
 option quasi_keyword_color : string = "9966FFFF"
+option improper_color : string = "FF5050FF"
 option operator_color : string = "323232FF"
 option caret_invisible_color : string = "50000080"
 option completion_color : string = "0000FFFF"

--- a/src/Tools/jEdit/src/rendering.scala	Tue Mar 18 11:27:09 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Mar 18 12:25:17 2014 +0100
@@ -239,6 +239,7 @@
   val keyword2_color = color_value("keyword2_color")
   val keyword3_color = color_value("keyword3_color")
   val quasi_keyword_color = color_value("quasi_keyword_color")
+  val improper_color = color_value("improper_color")
   val operator_color = color_value("operator_color")
   val caret_invisible_color = color_value("caret_invisible_color")
   val completion_color = color_value("completion_color")
@@ -654,6 +655,7 @@
       Markup.KEYWORD2 -> keyword2_color,
       Markup.KEYWORD3 -> keyword3_color,
       Markup.QUASI_KEYWORD -> quasi_keyword_color,
+      Markup.IMPROPER -> improper_color,
       Markup.OPERATOR -> operator_color,
       Markup.STRING -> Color.BLACK,
       Markup.ALTSTRING -> Color.BLACK,