diff -r ce37d4f8b4f4 -r 6e5fd4585512 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Aug 24 11:32:12 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Aug 24 12:35:39 2012 +0200
@@ -33,6 +33,7 @@
   val parse: Position.T -> string -> Toplevel.transition list
   type isar
   val isar: TextIO.instream -> bool -> isar
+  val span_cmts: Token.T list -> Token.T list
   val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
   val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     (Toplevel.transition * Toplevel.transition list) list
@@ -267,6 +268,22 @@
   |> toplevel_source term (SOME true) lookup_commands_dynamic;
 
 
+(* side-comments *)
+
+local
+
+fun cmts (t1 :: t2 :: toks) =
+      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
+      else cmts (t2 :: toks)
+  | cmts toks = [];
+
+in
+
+val span_cmts = filter Token.is_proper #> cmts;
+
+end;
+
+
 (* read toplevel commands -- fail-safe *)
 
 fun read_span outer_syntax toks =