# HG changeset patch
# User wenzelm
# Date 1492788853 -7200
# Node ID dbcd9b3e1b49d5a506cdd3c0b848282098d2a59e
# Parent  a39ef48fbee016c727fc671cb799a4e6bc3b3ec6
more precise position information;

diff -r a39ef48fbee0 -r dbcd9b3e1b49 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Apr 21 16:48:58 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Apr 21 17:34:13 2017 +0200
@@ -156,7 +156,7 @@
 
   /* read -- lazy scanning */
 
-  def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
+  private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) =
   {
     val token = Token.Parsers.token(bootstrap_keywords)
     def make_tokens(in: Reader[Char]): Stream[Token] =
@@ -165,14 +165,30 @@
         case _ => Stream.empty
       }
 
-    val tokens =
-      if (strict) make_tokens(reader)
-      else make_tokens(reader).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
+    val all_tokens = make_tokens(reader)
+    val drop_tokens =
+      if (strict) Nil
+      else all_tokens.takeWhile(tok => !tok.is_command(Thy_Header.THEORY)).toList
 
+    val tokens = all_tokens.drop(drop_tokens.length)
     val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList
     val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList
 
-    parse(commit(header), Token.reader(tokens1 ::: tokens2, start)) match {
+    (drop_tokens, tokens1 ::: tokens2)
+  }
+
+  def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
+  {
+    val (_, tokens0) = read_tokens(reader, true)
+    val text =
+      if (reader.isInstanceOf[Scan.Byte_Reader])
+        UTF8.decode_permissive(Token.implode(tokens0))
+      else Token.implode(tokens0)
+
+    val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
+    val pos = (start /: drop_tokens)(_.advance(_))
+
+    parse(commit(header), Token.reader(tokens, pos)) match {
       case Success(result, _) => result
       case bad => error(bad.toString)
     }
diff -r a39ef48fbee0 -r dbcd9b3e1b49 src/Pure/Tools/update_imports.scala
--- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 16:48:58 2017 +0200
+++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 17:34:13 2017 +0200
@@ -97,11 +97,7 @@
       val updates_theories =
         for {
           (_, name) <- session_base.known.theories_local.toList
-          (_, pos) <-
-            // FIXME proper UTF8 positions for check_thy
-            resources.check_thy_reader(name,
-              Scan.char_reader(File.read(Path.explode(name.node))),
-              Token.Pos.file(name.node)).imports
+          (_, pos) <- resources.check_thy(name, Token.Pos.file(name.node)).imports
           upd <- update_name(session_base.syntax.keywords, pos,
             standard_import(resources.theory_qualifier(name), name.master_dir, _))
         } yield upd