--- a/src/Pure/General/symbol_pos.ML Thu Oct 15 21:17:41 2015 +0200
+++ b/src/Pure/General/symbol_pos.ML Thu Oct 15 22:25:57 2015 +0200
@@ -14,6 +14,7 @@
val ~$$$ : Symbol.symbol -> T list -> T list * T list
val content: T list -> string
val range: T list -> Position.range
+ val trim_blanks: T list -> T list
val is_eof: T -> bool
val stopper: T Scan.stopper
val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
@@ -59,6 +60,10 @@
in Position.range pos pos' end
| range [] = Position.no_range;
+val trim_blanks =
+ take_prefix (Symbol.is_blank o symbol) #> #2 #>
+ take_suffix (Symbol.is_blank o symbol) #> #1;
+
(* stopper *)