--- a/src/Pure/General/position.ML Wed Oct 03 16:59:58 2012 +0200
+++ b/src/Pure/General/position.ML Wed Oct 03 17:12:08 2012 +0200
@@ -42,6 +42,7 @@
val reports: report list -> unit
val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
val here: T -> string
+ val here_list: T list -> string
type range = T * T
val no_range: range
val set_range: range -> T
@@ -198,6 +199,8 @@
Markup.markup (Markup.properties props Isabelle_Markup.position) s
end;
+val here_list = space_implode " " o map here;
+
(* range *)