# HG changeset patch
# User wenzelm
# Date 1218472669 -7200
# Node ID edafacb690a3639a425b6be40e84de1e98e7b180
# Parent  03ed3519cf483156d6c9f68f974e7f2e8b5018c6
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);

diff -r 03ed3519cf48 -r edafacb690a3 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Aug 11 17:37:48 2008 +0200
+++ b/src/Pure/General/markup.ML	Mon Aug 11 18:37:49 2008 +0200
@@ -37,7 +37,7 @@
   val widthN: string
   val breakN: string val break: int -> T
   val fbreakN: string val fbreak: T
-  val classN: string val class: string -> T
+  val tclassN: string val tclass: string -> T
   val tyconN: string val tycon: string -> T
   val fixedN: string val fixed: string -> T
   val constN: string val const: string -> T
@@ -163,7 +163,7 @@
 
 (* logical entities *)
 
-val (classN, class) = markup_string "class" nameN;
+val (tclassN, tclass) = markup_string "tclass" nameN;
 val (tyconN, tycon) = markup_string "tycon" nameN;
 val (fixedN, fixed) = markup_string "fixed" nameN;
 val (constN, const) = markup_string "const" nameN;
diff -r 03ed3519cf48 -r edafacb690a3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Aug 11 17:37:48 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Aug 11 18:37:49 2008 +0200
@@ -373,7 +373,7 @@
   | NONE => Pretty.mark Markup.var (Pretty.str s));
 
 fun class_markup _ c =    (* FIXME authentic name *)
-  Pretty.mark (Markup.classN, []) (Pretty.str c);
+  Pretty.mark (Markup.tclassN, []) (Pretty.str c);
 
 fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
 
diff -r 03ed3519cf48 -r edafacb690a3 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 11 17:37:48 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 11 18:37:49 2008 +0200
@@ -62,7 +62,7 @@
       if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
       else if name = Markup.sendbackN then (special "376", special "377")
       else if name = Markup.hiliteN then (special "327", special "330")
-      else if name = Markup.classN then (special "351", special "350")
+      else if name = Markup.tclassN then (special "351", special "350")
       else if name = Markup.tfreeN then (special "352", special "350")
       else if name = Markup.tvarN then (special "353", special "350")
       else if name = Markup.freeN then (special "354", special "350")
diff -r 03ed3519cf48 -r edafacb690a3 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 11 17:37:48 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 11 18:37:49 2008 +0200
@@ -248,7 +248,7 @@
     split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text))
 
 val token_markups =
- [Markup.classN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
+ [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
   Markup.boundN, Markup.varN, Markup.skolemN];
 
 in