# HG changeset patch
# User wenzelm
# Date 1184015555 -7200
# Node ID 9e8257472c27d99046ebb32680d0ad7a88d116d0
# Parent  681ffad36776f4127e73b1c634edfcc21faedce6
proper position markup;
added properties operation;
tuned;

diff -r 681ffad36776 -r 9e8257472c27 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Mon Jul 09 23:12:31 2007 +0200
+++ b/src/Pure/General/markup.ML	Mon Jul 09 23:12:35 2007 +0200
@@ -11,9 +11,11 @@
   type T = string * property list
   val nameN: string
   val kindN: string
-  val pos_lineN: string
-  val pos_nameN: string
   val none: T
+  val properties: (string * string) list -> T -> T
+  val lineN: string
+  val fileN: string
+  val positionN: string val position: T
   val indentN: string
   val blockN: string val block: int -> T
   val breakN: string val break: int -> T
@@ -43,14 +45,23 @@
 
 val none = ("", []);
 
+fun properties more_props ((elem, props): T) =
+  (elem, fold_rev (AList.update (op =)) more_props props);
+
 val nameN = "name";
 val kindN = "kind";
-val pos_lineN = "pos_line";
-val pos_nameN = "pos_name";
+
+fun markup elem = (elem, (elem, []): T);
+fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
+fun markup_int elem prop = (elem, fn i => (elem, [(prop, string_of_int i)]): T);
+
 
-fun markup kind = (kind, (kind, []): T);
-fun markup_string kind prop = (kind, fn s => (kind, [(prop, s)]): T);
-fun markup_int kind prop = (kind, fn i => (kind, [(prop, string_of_int i)]): T);
+(* position *)
+
+val lineN = "line";
+val fileN = "file";
+
+val (positionN, position) = markup "position";
 
 
 (* pretty printing *)