# HG changeset patch
# User wenzelm
# Date 1344586687 -7200
# Node ID dc3bbdda4bc880b76c1c80edadd8c4e2dd3c51be
# Parent  c197b3c3e7fa7326c262d221d53b1ba84bdfa956
more visible markup of malformed input as "bad";

diff -r c197b3c3e7fa -r dc3bbdda4bc8 etc/isabelle.css
--- a/etc/isabelle.css	Thu Aug 09 22:31:04 2012 +0200
+++ b/etc/isabelle.css	Fri Aug 10 10:18:07 2012 +0200
@@ -42,7 +42,7 @@
 .verbatim       { color: #00008B; }
 .comment        { color: #8B0000; }
 .control        { background-color: #FF6A6A; }
-.malformed      { background-color: #FF6A6A; }
+.bad            { background-color: #FF6A6A; }
 
 .malformed_span { background-color: #FF6A6A; }
 
diff -r c197b3c3e7fa -r dc3bbdda4bc8 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/Pure/ML/ml_lex.ML	Fri Aug 10 10:18:07 2012 +0200
@@ -115,7 +115,7 @@
   | String    => Isabelle_Markup.ML_string
   | Space     => Markup.empty
   | Comment   => Isabelle_Markup.ML_comment
-  | Error _   => Isabelle_Markup.ML_malformed
+  | Error _   => Isabelle_Markup.bad
   | EOF       => Markup.empty;
 
 fun token_markup kind x =
diff -r c197b3c3e7fa -r dc3bbdda4bc8 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Aug 10 10:18:07 2012 +0200
@@ -55,7 +55,6 @@
   val ML_charN: string val ML_char: Markup.T
   val ML_stringN: string val ML_string: Markup.T
   val ML_commentN: string val ML_comment: Markup.T
-  val ML_malformedN: string val ML_malformed: Markup.T
   val ML_defN: string
   val ML_openN: string
   val ML_structN: string
@@ -74,7 +73,6 @@
   val verbatimN: string val verbatim: Markup.T
   val commentN: string val comment: Markup.T
   val controlN: string val control: Markup.T
-  val malformedN: string val malformed: Markup.T
   val tokenN: string val token: Properties.T -> Markup.T
   val command_spanN: string val command_span: string -> Markup.T
   val ignored_spanN: string val ignored_span: Markup.T
@@ -211,7 +209,6 @@
 val (ML_charN, ML_char) = markup_elem "ML_char";
 val (ML_stringN, ML_string) = markup_elem "ML_string";
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
-val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
 
 val ML_defN = "ML_def";
 val ML_openN = "ML_open";
@@ -240,7 +237,6 @@
 val (verbatimN, verbatim) = markup_elem "verbatim";
 val (commentN, comment) = markup_elem "comment";
 val (controlN, control) = markup_elem "control";
-val (malformedN, malformed) = markup_elem "malformed";
 
 val tokenN = "token";
 fun token props = (tokenN, props);
diff -r c197b3c3e7fa -r dc3bbdda4bc8 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Aug 10 10:18:07 2012 +0200
@@ -132,7 +132,6 @@
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
   val ML_COMMENT = "ML_comment"
-  val ML_MALFORMED = "ML_malformed"
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
@@ -150,7 +149,6 @@
   val VERBATIM = "verbatim"
   val COMMENT = "comment"
   val CONTROL = "control"
-  val MALFORMED = "malformed"
 
   val COMMAND_SPAN = "command_span"
   val IGNORED_SPAN = "ignored_span"
diff -r c197b3c3e7fa -r dc3bbdda4bc8 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 10 10:18:07 2012 +0200
@@ -609,7 +609,7 @@
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Isabelle_Markup.tvar, x))
       | token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
       | token_trans "_bound" x = SOME (Pretty.mark_str (Isabelle_Markup.bound, x))
-      | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.malformed, x))
+      | token_trans "_loose" x = SOME (Pretty.mark_str (Isabelle_Markup.bad, x))
       | token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
       | token_trans "_numeral" x = SOME (Pretty.mark_str (Isabelle_Markup.numeral, x))
       | token_trans "_inner_string" x = SOME (Pretty.mark_str (Isabelle_Markup.inner_string, x))
diff -r c197b3c3e7fa -r dc3bbdda4bc8 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Fri Aug 10 10:18:07 2012 +0200
@@ -54,7 +54,7 @@
   | Token.Space         => Markup.empty
   | Token.Comment       => Isabelle_Markup.comment
   | Token.InternalValue => Markup.empty
-  | Token.Error _       => Isabelle_Markup.malformed
+  | Token.Error _       => Isabelle_Markup.bad
   | Token.Sync          => Isabelle_Markup.control
   | Token.EOF           => Isabelle_Markup.control;
 
@@ -74,7 +74,7 @@
     val malformed_symbols =
       Symbol_Pos.explode (Token.source_position_of tok)
       |> map_filter (fn (sym, pos) =>
-          if Symbol.is_malformed sym then SOME (pos, Isabelle_Markup.malformed) else NONE);
+          if Symbol.is_malformed sym then SOME (pos, Isabelle_Markup.bad) else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
     val reports = (Token.position_of tok, token_markup tok) :: malformed_symbols;
   in (is_malformed, reports) end;
diff -r c197b3c3e7fa -r dc3bbdda4bc8 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 10 10:18:07 2012 +0200
@@ -22,7 +22,7 @@
 {
   /* physical rendering */
 
-  // see http://www.w3schools.com/css/css_colornames.asp
+  // see http://www.w3schools.com/cssref/css_colornames.asp
 
   def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
 
@@ -290,7 +290,6 @@
       Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
       Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
       Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
-      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
       Isabelle_Markup.ANTIQ -> get_color("blue"))
 
   private val text_color_elements = Set.empty[String] ++ text_colors.keys