diff -r 4c9aa5f7bfa0 -r 983e98da2a42 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Thu Oct 16 10:59:43 2014 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Thu Oct 16 12:09:57 2014 +0200 @@ -134,7 +134,8 @@ } } - def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) = + def scan_line(input: CharSequence, context: Scan.Line_Context, depth: Int) + : (List[Token], Scan.Line_Context, Int) = { var in: Reader[Char] = new CharSequenceReader(input) val toks = new mutable.ListBuffer[Token] @@ -146,7 +147,9 @@ error("Unexpected failure of tokenizing input:\n" + rest.source.toString) } } - (toks.toList, ctxt) + + val depth1 = depth // FIXME + (toks.toList, ctxt, depth1) }