# HG changeset patch
# User wenzelm
# Date 1322736879 -3600
# Node ID 7df60d1aa988801084d959e1dddf65a9f1edca9f
# Parent  615da8b8d758fd2c3d18be0aceaf3ed68d1a61ee
updated markup conforming to ML side;

diff -r 615da8b8d758 -r 7df60d1aa988 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Wed Nov 30 23:30:08 2011 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Thu Dec 01 11:54:39 2011 +0100
@@ -93,10 +93,7 @@
   val SKOLEM = "skolem"
   val BOUND = "bound"
   val VAR = "var"
-  val NUM = "num"
-  val FLOAT = "float"
-  val XNUM = "xnum"
-  val XSTR = "xstr"
+  val NUMERAL = "numeral"
   val LITERAL = "literal"
   val DELIMITER = "delimiter"
   val INNER_STRING = "inner_string"