1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Aug 24 11:32:12 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Aug 24 12:35:39 2012 +0200
     1.3 @@ -33,6 +33,7 @@
     1.4    val parse: Position.T -> string -> Toplevel.transition list
     1.5    type isar
     1.6    val isar: TextIO.instream -> bool -> isar
     1.7 +  val span_cmts: Token.T list -> Token.T list
     1.8    val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
     1.9    val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
    1.10      (Toplevel.transition * Toplevel.transition list) list
    1.11 @@ -267,6 +268,22 @@
    1.12    |> toplevel_source term (SOME true) lookup_commands_dynamic;
    1.13  
    1.14  
    1.15 +(* side-comments *)
    1.16 +
    1.17 +local
    1.18 +
    1.19 +fun cmts (t1 :: t2 :: toks) =
    1.20 +      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    1.21 +      else cmts (t2 :: toks)
    1.22 +  | cmts toks = [];
    1.23 +
    1.24 +in
    1.25 +
    1.26 +val span_cmts = filter Token.is_proper #> cmts;
    1.27 +
    1.28 +end;
    1.29 +
    1.30 +
    1.31  (* read toplevel commands -- fail-safe *)
    1.32  
    1.33  fun read_span outer_syntax toks =