# HG changeset patch
# User wenzelm
# Date 1309023515 -7200
# Node ID 156c822f181a44533c4803fb2a6692305aed104c
# Parent  07a9cbf2376f646c8db7f4c98c02e63325d3b471
entity markup for "type", "constant";

diff -r 07a9cbf2376f -r 156c822f181a etc/isabelle.css
--- a/etc/isabelle.css	Sat Jun 25 19:19:13 2011 +0200
+++ b/etc/isabelle.css	Sat Jun 25 19:38:35 2011 +0200
@@ -21,6 +21,8 @@
 
 .binding        { color: #336655; }
 .entity_class   { color: red; }
+.entity_type    { }
+.entity_constant { }
 .tfree          { color: #A020F0; }
 .tvar           { color: #A020F0; }
 .free           { color: blue; }
diff -r 07a9cbf2376f -r 156c822f181a src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Jun 25 19:19:13 2011 +0200
+++ b/src/Pure/General/markup.ML	Sat Jun 25 19:38:35 2011 +0200
@@ -36,9 +36,9 @@
   val fbreakN: string val fbreak: T
   val hiddenN: string val hidden: T
   val classN: string
-  val tyconN: string val tycon: string -> T
+  val typeN: string
+  val constantN: string
   val fixedN: string val fixed: string -> T
-  val constN: string val const: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
@@ -213,9 +213,10 @@
 (* logical entities *)
 
 val classN = "class";
-val (tyconN, tycon) = markup_string "tycon" nameN;
+val typeN = "type";
+val constantN = "constant";
+
 val (fixedN, fixed) = markup_string "fixed" nameN;
-val (constN, const) = markup_string "constant" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 
 
diff -r 07a9cbf2376f -r 156c822f181a src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Jun 25 19:19:13 2011 +0200
+++ b/src/Pure/General/markup.scala	Sat Jun 25 19:38:35 2011 +0200
@@ -148,9 +148,10 @@
   /* logical entities */
 
   val CLASS = "class"
-  val TYCON = "tycon"
+  val TYPE = "type"
   val FIXED = "fixed"
-  val CONST = "constant"
+  val CONSTANT = "constant"
+
   val DYNAMIC_FACT = "dynamic_fact"
 
 
diff -r 07a9cbf2376f -r 156c822f181a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Jun 25 19:19:13 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jun 25 19:38:35 2011 +0200
@@ -451,7 +451,6 @@
     val _ =
       if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
       else ();
-    val _ = Context_Position.report ctxt pos (Markup.const d);
     val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
   in t end;
 
@@ -475,7 +474,6 @@
             Type.LogicalType n => n
           | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
           | Type.Nonterminal => if strict then err () else 0);
-        val _ = Context_Position.report ctxt pos (Markup.tycon d);
         val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.type_space tsig) d);
       in Type (d, replicate args dummyT) end
   end;
diff -r 07a9cbf2376f -r 156c822f181a src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Jun 25 19:19:13 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Jun 25 19:38:35 2011 +0200
@@ -625,8 +625,8 @@
       | SOME b => markup_extern b
       | NONE => c |> Lexicon.unmark
          {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_type = fn x => (markup_type ctxt x, Proof_Context.extern_type ctxt x),
+          case_const = fn x => (markup_const ctxt x, Proof_Context.extern_const ctxt x),
           case_fixed = fn x => free_or_skolem ctxt x,
           case_default = fn x => ([], x)});
   in
diff -r 07a9cbf2376f -r 156c822f181a src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sat Jun 25 19:19:13 2011 +0200
+++ b/src/Pure/consts.ML	Sat Jun 25 19:38:35 2011 +0200
@@ -311,7 +311,7 @@
 
 (* empty and merge *)
 
-val empty = make_consts (Name_Space.empty_table "constant", Symtab.empty, Symtab.empty);
+val empty = make_consts (Name_Space.empty_table Markup.constantN, Symtab.empty, Symtab.empty);
 
 fun merge
    (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
diff -r 07a9cbf2376f -r 156c822f181a src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Jun 25 19:19:13 2011 +0200
+++ b/src/Pure/type.ML	Sat Jun 25 19:38:35 2011 +0200
@@ -181,7 +181,8 @@
   build_tsig (f (classes, default, types));
 
 val empty_tsig =
-  build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [], Name_Space.empty_table "type");
+  build_tsig ((Name_Space.empty Markup.classN, Sorts.empty_algebra), [],
+    Name_Space.empty_table Markup.typeN);
 
 
 (* classes and sorts *)
diff -r 07a9cbf2376f -r 156c822f181a src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 25 19:19:13 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Jun 25 19:38:35 2011 +0200
@@ -112,7 +112,9 @@
 
   private val text_entity_colors: Map[String, Color] =
     Map(
-      Markup.CLASS -> get_color("red"))
+      Markup.CLASS -> get_color("red"),
+      Markup.TYPE -> get_color("black"),
+      Markup.CONSTANT -> get_color("black"))
 
   private val text_colors: Map[String, Color] =
     Map(
@@ -121,7 +123,6 @@
       Markup.IDENT -> get_color("black"),
       Markup.TFREE -> get_color("#A020F0"),
       Markup.TVAR -> get_color("#A020F0"),
-      Markup.CONST -> get_color("black"),
       Markup.FREE -> get_color("blue"),
       Markup.SKOLEM -> get_color("#D2691E"),
       Markup.BOUND -> get_color("green"),