src/Pure/Isar/outer_syntax.ML

   val print_outer_syntax: unit -> unit
   val scan: Position.T -> string -> Token.T list
   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
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
 struct

   |> Symbol.source
   |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none
   |> 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 _ = [];
-
-in
-
-val span_cmts = filter Token.is_proper #> cmts;
-
-end;
-
-
 (* read command span -- fail-safe *)
 
 fun read_span outer_syntax toks =
   let
     val commands = lookup_commands outer_syntax;