type classes: entity markup instead of old-style token markup;

--- a/etc/isabelle.css	Sat Jun 25 17:17:49 2011 +0200
+++ b/etc/isabelle.css	Sat Jun 25 18:15:36 2011 +0200
@@ -20,7 +20,7 @@
 .hidden, hidden { font-size: 0.1pt; visibility: hidden; }
 
 .binding, binding             { color: #9966FF; }
-.tclass, tclass               { color: red; }
+.entity_class                 { color: red; }
 .tfree, tfree                 { color: #A020F0; }
 .tvar, tvar                   { color: #A020F0; }
 .free, free                   { color: blue; }

--- a/src/Pure/General/markup.ML	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/General/markup.ML	Sat Jun 25 18:15:36 2011 +0200
@@ -17,6 +17,7 @@
   val kindN: string
   val bindingN: string val binding: T
   val entityN: string val entity: string -> string -> T
+  val get_entity_kind: T -> string option
   val defN: string
   val refN: string
   val lineN: string
@@ -34,7 +35,7 @@
   val breakN: string val break: int -> T
   val fbreakN: string val fbreak: T
   val hiddenN: string val hidden: T
-  val tclassN: string val tclass: string -> T
+  val classN: string
   val tyconN: string val tycon: string -> T
   val fixedN: string val fixed: string -> T
   val constN: string val const: string -> T
@@ -170,6 +171,10 @@
 val entityN = "entity";
 fun entity kind name = (entityN, [(nameN, name), (kindN, kind)]);
 
+fun get_entity_kind (name, props) =
+  if name = entityN then AList.lookup (op =) props kindN
+  else NONE;
+
 val defN = "def";
 val refN = "ref";
 
@@ -207,7 +212,7 @@
 
 (* logical entities *)
 
-val (tclassN, tclass) = markup_string "tclass" nameN;
+val classN = "class";
 val (tyconN, tycon) = markup_string "tycon" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (constN, const) = markup_string "constant" nameN;

--- a/src/Pure/Isar/proof_context.ML	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jun 25 18:15:36 2011 +0200
@@ -362,7 +362,6 @@
     val (syms, pos) = Syntax.read_token text;
     val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
       handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
-    val _ = Context_Position.report ctxt pos (Markup.tclass c);
     val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
   in c end;
 

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jun 25 18:15:36 2011 +0200
@@ -43,14 +43,18 @@
           else if name = Markup.sendbackN then (special "W", special "X")
           else if name = Markup.bindingN then (special "F", special "A")
           else if name = Markup.hiliteN then (special "0", special "1")
-          else if name = Markup.tclassN then (special "B", special "A")
           else if name = Markup.tfreeN then (special "C", special "A")
           else if name = Markup.tvarN then (special "D", special "A")
           else if name = Markup.freeN then (special "E", special "A")
           else if name = Markup.boundN then (special "F", special "A")
           else if name = Markup.varN then (special "G", special "A")
           else if name = Markup.skolemN then (special "H", special "A")
-          else Markup.no_output;
+          else
+            (case Markup.get_entity_kind (name, props) of
+              SOME kind =>
+                if kind = Markup.classN then (special "B", special "A")
+                else Markup.no_output
+            | NONE => Markup.no_output);
       in
         Buffer.add bg1 #>
         Buffer.add bg2 #>

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Jun 25 18:15:36 2011 +0200
@@ -101,7 +101,7 @@
 val pgml_syms = map pgml_sym o Symbol.explode;
 
 val token_markups =
- [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
+ [Markup.tfreeN, Markup.tvarN, Markup.freeN,
   Markup.boundN, Markup.varN, Markup.skolemN];
 
 in

--- a/src/Pure/Syntax/syntax_phases.ML	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Jun 25 18:15:36 2011 +0200
@@ -624,7 +624,7 @@
         SOME "" => ([], c)
       | SOME b => markup_extern b
       | NONE => c |> Lexicon.unmark
-         {case_class = fn x => ([Markup.tclass x], Proof_Context.extern_class ctxt x),
+         {case_class = fn x => (markup_class ctxt x, Proof_Context.extern_class ctxt x),
           case_type = fn x => ([Markup.tycon x], Proof_Context.extern_type ctxt x),
           case_const = fn x => ([Markup.const x], Proof_Context.extern_const ctxt x),
           case_fixed = fn x => free_or_skolem ctxt x,

--- a/src/Pure/Thy/html.ML	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/Thy/html.ML	Sat Jun 25 18:15:36 2011 +0200
@@ -48,7 +48,12 @@
 
 fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
 
-val _ = Markup.add_mode htmlN (fn (name, _) => span name);
+fun span_class (name, props) =
+  (case Markup.get_entity_kind (name, props) of
+    SOME kind => Markup.entityN ^ "_" ^ name
+  | NONE => name);
+
+val _ = Markup.add_mode htmlN (span o span_class);
 
 
 (* symbol output *)

--- a/src/Pure/Thy/html.scala	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/Thy/html.scala	Sat Jun 25 18:15:36 2011 +0200
@@ -60,10 +60,12 @@
   {
     def html_spans(tree: XML.Tree): XML.Body =
       tree match {
-        case XML.Elem(Markup(name, _), ts) =>
-          if (original_data)
-            List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(html_spans)))))
-          else List(span(name, ts.flatMap(html_spans)))
+        case XML.Elem(m @ Markup(name, props), ts) =>
+          val span_class =
+            m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
+          val html_span = span(span_class, ts.flatMap(html_spans))
+          if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
+          else List(html_span)
         case XML.Text(txt) =>
           val ts = new ListBuffer[XML.Tree]
           val t = new StringBuilder

--- a/src/Pure/type.ML	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Pure/type.ML	Sat Jun 25 18:15:36 2011 +0200
@@ -181,7 +181,7 @@
   build_tsig (f (classes, default, types));
 
 val empty_tsig =
-  build_tsig ((Name_Space.empty "class", Sorts.empty_algebra), [], Name_Space.empty_table "type");
+  build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [], Name_Space.empty_table "type");
 
 
 (* classes and sorts *)

--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 25 17:17:49 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 25 18:15:36 2011 +0200
@@ -110,12 +110,15 @@
     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   }
 
+  private val text_entity_colors: Map[String, Color] =
+    Map(
+      Markup.CLASS -> get_color("red"))
+
   private val text_colors: Map[String, Color] =
     Map(
       Markup.LITERAL -> keyword1_color,
       Markup.DELIMITER -> get_color("black"),
       Markup.IDENT -> get_color("black"),
-      Markup.TCLASS -> get_color("red"),
       Markup.TFREE -> get_color("#A020F0"),
       Markup.TVAR -> get_color("#A020F0"),
       Markup.CONST -> get_color("black"),
@@ -137,6 +140,8 @@
 
   val text_color: Markup_Tree.Select[Color] =
   {
+    case Text.Info(_, XML.Elem(Markup.Entity(kind, _), _))
+    if text_entity_colors.isDefinedAt(kind) => text_entity_colors(kind)
     case Text.Info(_, XML.Elem(Markup(m, _), _))
     if text_colors.isDefinedAt(m) => text_colors(m)
   }