# HG changeset patch
# User wenzelm
# Date 1261946063 -3600
# Node ID fbfc18be1f8cce877a5d646ee4f37680500ed351
# Parent  7b659c1561f1e1f16c59148a8e37991aadb0565e
scan: operate on file (via Scan.byte_reader), more robust exception handling;

diff -r 7b659c1561f1 -r fbfc18be1f8c src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Dec 27 21:33:35 2009 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Dec 27 21:34:23 2009 +0100
@@ -10,6 +10,8 @@
 import scala.collection.mutable
 import scala.util.parsing.input.{Reader, CharSequenceReader}
 
+import java.io.File
+
 
 object Thy_Header
 {
@@ -52,21 +54,24 @@
 
   /* scan -- lazy approximation */
 
-  def scan(text: CharSequence): List[Outer_Lex.Token] =
+  def scan(file: File): List[Outer_Lex.Token] =
   {
     val token = lexicon.token(symbols, _ => false)
     val toks = new mutable.ListBuffer[Outer_Lex.Token]
-    def scan_until_begin(in: Reader[Char])
+
+    def scan_to_begin(in: Reader[Char])
     {
       token(in) match {
         case lexicon.Success(tok, rest) =>
           toks += tok
           if (!(tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == BEGIN))
-            scan_until_begin(rest)
+            scan_to_begin(rest)
         case _ =>
       }
     }
-    scan_until_begin(new CharSequenceReader(text))
+
+    val reader = Scan.byte_reader(file)
+    try { scan_to_begin(reader) } finally { reader.close }
     toks.toList
   }
 }