# HG changeset patch
# User wenzelm
# Date 1256399384 -7200
# Node ID 757d7787b10ceec0e2b50bea9949c2d17220dd33
# Parent  e50f948fd6bdee49f665af6ea74f118ecd81874d
markup for formal entities, with "def" or "ref" occurrences;

diff -r e50f948fd6bd -r 757d7787b10c src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Oct 24 17:47:53 2009 +0200
+++ b/src/Pure/General/markup.ML	Sat Oct 24 17:49:44 2009 +0200
@@ -18,6 +18,9 @@
   val kindN: string
   val internalK: string
   val property_internal: Properties.property
+  val entityN: string val entity: string -> T
+  val defN: string
+  val refN: string
   val lineN: string
   val columnN: string
   val offsetN: string
@@ -161,6 +164,14 @@
 val property_internal = (kindN, internalK);
 
 
+(* formal entities *)
+
+val (entityN, entity) = markup_string "entity" nameN;
+
+val defN = "def";
+val refN = "ref";
+
+
 (* position *)
 
 val lineN = "line";
diff -r e50f948fd6bd -r 757d7787b10c src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Oct 24 17:47:53 2009 +0200
+++ b/src/Pure/General/markup.scala	Sat Oct 24 17:49:44 2009 +0200
@@ -15,6 +15,13 @@
   val KIND = "kind"
 
 
+  /* formal entities */
+
+  val ENTITY = "entity"
+  val DEF = "def"
+  val REF = "ref"
+
+
   /* position */
 
   val LINE = "line"