clarifed name space "type name", which covers logical and non-logical types, and often occurs inside outer syntax "type" markup;
--- a/src/Pure/PIDE/isabelle_markup.ML Fri Feb 24 13:50:37 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML Fri Feb 24 18:14:06 2012 +0100
@@ -27,7 +27,7 @@
val fbreakN: string val fbreak: Markup.T
val hiddenN: string val hidden: Markup.T
val classN: string
- val typeN: string
+ val type_nameN: string
val constantN: string
val fixedN: string val fixed: string -> Markup.T
val dynamic_factN: string val dynamic_fact: string -> Markup.T
@@ -174,7 +174,7 @@
(* logical entities *)
val classN = "class";
-val typeN = "type";
+val type_nameN = "type name";
val constantN = "constant";
val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
--- a/src/Pure/PIDE/isabelle_markup.scala Fri Feb 24 13:50:37 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala Fri Feb 24 18:14:06 2012 +0100
@@ -78,7 +78,7 @@
/* logical entities */
val CLASS = "class"
- val TYPE = "type"
+ val TYPE_NAME = "type name"
val FIXED = "fixed"
val CONSTANT = "constant"
--- a/src/Pure/type.ML Fri Feb 24 13:50:37 2012 +0100
+++ b/src/Pure/type.ML Fri Feb 24 18:14:06 2012 +0100
@@ -187,7 +187,7 @@
val empty_tsig =
build_tsig ((Name_Space.empty Isabelle_Markup.classN, Sorts.empty_algebra), [],
- Name_Space.empty_table Isabelle_Markup.typeN);
+ Name_Space.empty_table Isabelle_Markup.type_nameN);
(* classes and sorts *)