src/Pure/Isar/outer_syntax.scala
changeset 58694 983e98da2a42
parent 58503 ea22f2380871
child 58695 91839729224e
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 10:59:43 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 12:09:57 2014 +0200
     1.3 @@ -134,7 +134,8 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
     1.8 +  def scan_line(input: CharSequence, context: Scan.Line_Context, depth: Int)
     1.9 +    : (List[Token], Scan.Line_Context, Int) =
    1.10    {
    1.11      var in: Reader[Char] = new CharSequenceReader(input)
    1.12      val toks = new mutable.ListBuffer[Token]
    1.13 @@ -146,7 +147,9 @@
    1.14            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.15        }
    1.16      }
    1.17 -    (toks.toList, ctxt)
    1.18 +
    1.19 +    val depth1 = depth // FIXME
    1.20 +    (toks.toList, ctxt, depth1)
    1.21    }
    1.22  
    1.23