--- a/src/Pure/General/position.ML Sat Apr 09 23:29:50 2011 +0200
+++ b/src/Pure/General/position.ML Mon Apr 11 17:11:03 2011 +0200
@@ -28,6 +28,7 @@
val put_id: string -> T -> T
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
+ val def_properties_of: T -> Properties.T
val default_properties: T -> Properties.T -> Properties.T
val markup: T -> Markup.T -> Markup.T
val is_reported: T -> bool
@@ -142,6 +143,8 @@
value Markup.lineN i @ value Markup.columnN j @
value Markup.offsetN k @ value Markup.end_offsetN l @ props;
+val def_properties_of = properties_of #> (map (fn (x, y) => ("def_" ^ x, y)));
+
fun default_properties default props =
if exists (member (op =) Markup.position_properties o #1) props then props
else properties_of default @ props;