# HG changeset patch
# User wenzelm
# Date 1191162039 -7200
# Node ID c1250851d701a2b4f41bfcb3730a43325b5557e5
# Parent  38afb780f6224f4c9ef19226031e3d957c457da0
added internalK, property_internal;

diff -r 38afb780f622 -r c1250851d701 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun Sep 30 16:20:38 2007 +0200
+++ b/src/Pure/General/markup.ML	Sun Sep 30 16:20:39 2007 +0200
@@ -15,6 +15,8 @@
   val properties: (string * string) list -> T -> T
   val nameN: string
   val kindN: string
+  val internalK: string
+  val property_internal: property
   val lineN: string
   val fileN: string
   val positionN: string val position: T
@@ -84,8 +86,15 @@
 fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
 
 val nameN = "name";
+
+
+(* kind *)
+
 val kindN = "kind";
 
+val internalK = "internal";
+val property_internal = (kindN, internalK);
+
 
 (* position *)