# HG changeset patch
# User wenzelm
# Date 1202672986 -3600
# Node ID 7d5b3e34a7359bd52fe56f17d3076e9c8a2cfac5
# Parent  43bcb30a6d9736e66f89d5663967c331200b01ad
added default_properties;

diff -r 43bcb30a6d97 -r 7d5b3e34a735 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sun Feb 10 20:49:45 2008 +0100
+++ b/src/Pure/General/position.ML	Sun Feb 10 20:49:46 2008 +0100
@@ -18,6 +18,7 @@
   val advance: Symbol.symbol -> T -> T
   val of_properties: Markup.property list -> T
   val properties_of: T -> Markup.property list
+  val default_properties: T -> Markup.property list -> Markup.property list
   val str_of: T -> string
   val thread_data: unit -> T
   val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
@@ -71,6 +72,10 @@
     NONE => []
   | SOME (m, n) => [(Markup.lineN, string_of_int m), (Markup.columnN, string_of_int n)]) @ props;
 
+fun default_properties default props =
+  if exists (member (op =) Markup.position_properties o #1) props then props
+  else properties_of default @ props;
+
 
 (* str_of *)