--- 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 *)