# HG changeset patch
# User wenzelm
# Date 1399031565 -7200
# Node ID 37be55461dbe9f13aff72835dcbf50c3ef4facbb
# Parent  6101243e6740fdf72e83b7743923531072859656
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
prefer non-strict Symbol.decode, since Reader[Char] may present symbols in either way;

diff -r 6101243e6740 -r 37be55461dbe src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri May 02 12:27:40 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri May 02 13:52:45 2014 +0200
@@ -8,6 +8,7 @@
 
 
 import scala.annotation.tailrec
+import scala.util.parsing.input.Reader
 
 import java.io.{File => JFile}
 
@@ -40,14 +41,13 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).expand.implode
 
-  def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
+  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     val path = Path.explode(name.node)
     if (!path.is_file) error("No such file: " + path.toString)
 
-    val text = File.read(path)
-    Symbol.decode_strict(text)
-    f(text)
+    val reader = Scan.byte_reader(path.file)
+    try { f(reader) } finally { reader.close }
   }
 
 
@@ -84,11 +84,11 @@
     }
   }
 
-  def check_thy_text(qualifier: String, name: Document.Node.Name, text: CharSequence)
+  def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
     : Document.Node.Header =
   {
     try {
-      val header = Thy_Header.read(text)
+      val header = Thy_Header.read(reader).decode_symbols
 
       val base_name = Long_Name.base_name(name.theory)
       val name1 = header.name
@@ -103,7 +103,7 @@
   }
 
   def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
-    with_thy_text(name, check_thy_text(qualifier, name, _))
+    with_thy_reader(name, check_thy_reader(qualifier, name, _))
 
 
   /* document changes */
diff -r 6101243e6740 -r 37be55461dbe src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri May 02 12:27:40 2014 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri May 02 13:52:45 2014 +0200
@@ -67,13 +67,16 @@
 
     val args =
       theory_name ~
-      (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
-      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
+      (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^
+        { case None => Nil case Some(_ ~ xs) => xs }) ~
+      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^
+        { case None => Nil case Some(_ ~ xs) => xs }) ~
       keyword(BEGIN) ^^
       { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
 
     (keyword(HEADER) ~ tags) ~!
-      ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
+      ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^
+        { case _ ~ x => x } |
     (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
   }
 
@@ -119,5 +122,13 @@
 {
   def map(f: String => String): Thy_Header =
     Thy_Header(f(name), imports.map(f), keywords)
+
+  def decode_symbols: Thy_Header =
+  {
+    val f = Symbol.decode _
+    Thy_Header(f(name), imports.map(f),
+      keywords.map({ case (a, b, c) =>
+        (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f))  }), c.map(f)) }))
+  }
 }
 
diff -r 6101243e6740 -r 37be55461dbe src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri May 02 12:27:40 2014 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri May 02 13:52:45 2014 +0200
@@ -30,7 +30,7 @@
   {
     def loaded_files(syntax: Prover.Syntax): List[String] =
     {
-      val string = resources.with_thy_text(name, _.toString)
+      val string = resources.with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
       resources.loaded_files(syntax, string)
     }
   }
diff -r 6101243e6740 -r 37be55461dbe src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri May 02 12:27:40 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri May 02 13:52:45 2014 +0200
@@ -70,7 +70,7 @@
     if (is_theory) {
       JEdit_Lib.buffer_lock(buffer) {
         Exn.capture {
-          PIDE.resources.check_thy_text("", node_name, buffer.getSegment(0, buffer.getLength))
+          PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
         } match {
           case Exn.Res(header) => header
           case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
diff -r 6101243e6740 -r 37be55461dbe src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Fri May 02 12:27:40 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri May 02 13:52:45 2014 +0200
@@ -14,6 +14,7 @@
 import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
 
 import scala.annotation.tailrec
+import scala.util.parsing.input.CharSequenceReader
 
 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
 import org.gjt.sp.jedit.gui.KeyEventWorkaround
@@ -97,6 +98,9 @@
   def buffer_text(buffer: JEditBuffer): String =
     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 
+  def buffer_reader(buffer: JEditBuffer): CharSequenceReader =
+    new CharSequenceReader(buffer.getSegment(0, buffer.getLength))
+
   def buffer_mode(buffer: JEditBuffer): String =
   {
     val mode = buffer.getMode
diff -r 6101243e6740 -r 37be55461dbe src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Fri May 02 12:27:40 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri May 02 13:52:45 2014 +0200
@@ -13,6 +13,8 @@
 import java.io.{File => JFile, ByteArrayOutputStream}
 import javax.swing.text.Segment
 
+import scala.util.parsing.input.Reader
+
 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
 import org.gjt.sp.jedit.MiscUtilities
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
@@ -58,21 +60,19 @@
     }
   }
 
-  override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A =
+  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     Swing_Thread.now {
       JEdit_Lib.jedit_buffer(name) match {
         case Some(buffer) =>
-          JEdit_Lib.buffer_lock(buffer) {
-            Some(consume(buffer.getSegment(0, buffer.getLength)))
-          }
+          JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
         case None => None
       }
     } getOrElse {
-      if (Url.is_wellformed(name.node)) consume(Url.read(name.node))
+      if (Url.is_wellformed(name.node)) f(Scan.byte_reader(Url(name.node)))
       else {
         val file = new JFile(name.node)
-        if (file.isFile) consume(File.read(file))
+        if (file.isFile) f(Scan.byte_reader(file))
         else error("No such file: " + quote(file.toString))
       }
     }