src/Pure/Isar/outer_syntax.scala
changeset 58694 983e98da2a42
parent 58503 ea22f2380871
child 58695 91839729224e
--- 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)
   }