src/Pure/General/position.ML

   type report = T * Markup.T
   type report_text = report * string
   val reports_text: report_text list -> unit
   val reports: report list -> unit
   val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
-  val str_of: T -> string
+  val here: T -> string
   type range = T * T
   val no_range: range
   val set_range: range -> T
   val reset_range: T -> T
   val range: T -> T -> range

   | store_reports (r: report list Unsynchronized.ref) ps markup x =
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
 
 
-(* str_of *)
-
-fun str_of pos =
+(* here: inlined formal markup *)
+
+fun here pos =
   let
     val props = properties_of pos;
     val s =
       (case (line_of pos, file_of pos) of
         (SOME i, NONE) => "(line " ^ string_of_int i ^ ")"