src/Pure/Isar/outer_syntax.scala
changeset 57906 020df63dd0a9
parent 57905 c0c5652e796e
child 57907 7fc36b4c7cce
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:17:02 2014 +0200
     1.3 @@ -186,6 +186,9 @@
     1.4      result.toList
     1.5    }
     1.6  
     1.7 +  def parse_spans(input: CharSequence): List[Command_Span.Span] =
     1.8 +    parse_spans(scan(input))
     1.9 +
    1.10  
    1.11    /* language context */
    1.12