Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed Markup.class to Markup.tclass, to avoid potential conflicts with spacial meaning in markup languages (e.g. HTML);
authorwenzelm
Mon, 11 Aug 2008 18:37:49 +0200
changeset 27828 edafacb690a3
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 file | annotate | diff | comparison | revisions
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions
src/Pure/ProofGeneral/proof_general_emacs.ML file | annotate | diff | comparison | revisions
src/Pure/ProofGeneral/proof_general_pgip.ML file | annotate | diff | comparison | revisions 
--- 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;
--- 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);
 
--- 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")
--- 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
isabelle