renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
authorwenzelm
Mon Aug 11 18:37:49 2008 +0200 (2008-08-11 ago)
changeset 27828edafacb690a3
parent 27827 03ed3519cf48
child 27829 c073006e0137
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
src/Pure/General/markup.ML
src/Pure/Isar/proof_context.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/General/markup.ML	Mon Aug 11 17:37:48 2008 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Mon Aug 11 18:37:49 2008 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    val widthN: string
     1.5    val breakN: string val break: int -> T
     1.6    val fbreakN: string val fbreak: T
     1.7 -  val classN: string val class: string -> T
     1.8 +  val tclassN: string val tclass: string -> T
     1.9    val tyconN: string val tycon: string -> T
    1.10    val fixedN: string val fixed: string -> T
    1.11    val constN: string val const: string -> T
    1.12 @@ -163,7 +163,7 @@
    1.13  
    1.14  (* logical entities *)
    1.15  
    1.16 -val (classN, class) = markup_string "class" nameN;
    1.17 +val (tclassN, tclass) = markup_string "tclass" nameN;
    1.18  val (tyconN, tycon) = markup_string "tycon" nameN;
    1.19  val (fixedN, fixed) = markup_string "fixed" nameN;
    1.20  val (constN, const) = markup_string "const" nameN;
     2.1 --- a/src/Pure/Isar/proof_context.ML	Mon Aug 11 17:37:48 2008 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Aug 11 18:37:49 2008 +0200
     2.3 @@ -373,7 +373,7 @@
     2.4    | NONE => Pretty.mark Markup.var (Pretty.str s));
     2.5  
     2.6  fun class_markup _ c =    (* FIXME authentic name *)
     2.7 -  Pretty.mark (Markup.classN, []) (Pretty.str c);
     2.8 +  Pretty.mark (Markup.tclassN, []) (Pretty.str c);
     2.9  
    2.10  fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
    2.11  
     3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 11 17:37:48 2008 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 11 18:37:49 2008 +0200
     3.3 @@ -62,7 +62,7 @@
     3.4        if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
     3.5        else if name = Markup.sendbackN then (special "376", special "377")
     3.6        else if name = Markup.hiliteN then (special "327", special "330")
     3.7 -      else if name = Markup.classN then (special "351", special "350")
     3.8 +      else if name = Markup.tclassN then (special "351", special "350")
     3.9        else if name = Markup.tfreeN then (special "352", special "350")
    3.10        else if name = Markup.tvarN then (special "353", special "350")
    3.11        else if name = Markup.freeN then (special "354", special "350")
     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 11 17:37:48 2008 +0200
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 11 18:37:49 2008 +0200
     4.3 @@ -248,7 +248,7 @@
     4.4      split_markup (output_pgmltext (pgml PgipTypes.Display pgmlterms_no_text))
     4.5  
     4.6  val token_markups =
     4.7 - [Markup.classN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
     4.8 + [Markup.tclassN, Markup.tfreeN, Markup.tvarN, Markup.freeN,
     4.9    Markup.boundN, Markup.varN, Markup.skolemN];
    4.10  
    4.11  in