src/Pure/Isar/outer_syntax.scala
changeset 58748 8f92f17d8781
parent 58747 c680f181b32e
child 58753 960bf499ca5d
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 13:56:42 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Oct 21 15:21:44 2014 +0200
     1.3 @@ -216,11 +216,7 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def scan_line(
     1.8 -    input: CharSequence,
     1.9 -    context: Scan.Line_Context,
    1.10 -    structure: Outer_Syntax.Line_Structure)
    1.11 -    : (List[Token], Scan.Line_Context, Outer_Syntax.Line_Structure) =
    1.12 +  def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
    1.13    {
    1.14      var in: Reader[Char] = new CharSequenceReader(input)
    1.15      val toks = new mutable.ListBuffer[Token]
    1.16 @@ -232,8 +228,7 @@
    1.17            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    1.18        }
    1.19      }
    1.20 -    val tokens = toks.toList
    1.21 -    (tokens, ctxt, line_structure(tokens, structure))
    1.22 +    (toks.toList, ctxt)
    1.23    }
    1.24  
    1.25