--- a/src/Pure/Isar/outer_syntax.scala Tue Oct 21 13:56:42 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Oct 21 15:21:44 2014 +0200
@@ -216,11 +216,7 @@
}
}
- def scan_line(
- input: CharSequence,
- context: Scan.Line_Context,
- structure: Outer_Syntax.Line_Structure)
- : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Structure) =
+ def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
{
var in: Reader[Char] = new CharSequenceReader(input)
val toks = new mutable.ListBuffer[Token]
@@ -232,8 +228,7 @@
error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
}
}
- val tokens = toks.toList
- (tokens, ctxt, line_structure(tokens, structure))
+ (toks.toList, ctxt)
}