more frugal access to theory text via Reader, reduced costs for I/O text decoding;
authorwenzelm
Fri May 02 13:52:45 2014 +0200 (2014-05-02 ago)
changeset 5682337be55461dbe
parent 56822 6101243e6740
child 56824 5ae68f53b7c2
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;
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri May 02 12:27:40 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri May 02 13:52:45 2014 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  
     1.5  
     1.6  import scala.annotation.tailrec
     1.7 +import scala.util.parsing.input.Reader
     1.8  
     1.9  import java.io.{File => JFile}
    1.10  
    1.11 @@ -40,14 +41,13 @@
    1.12    def append(dir: String, source_path: Path): String =
    1.13      (Path.explode(dir) + source_path).expand.implode
    1.14  
    1.15 -  def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
    1.16 +  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.17    {
    1.18      val path = Path.explode(name.node)
    1.19      if (!path.is_file) error("No such file: " + path.toString)
    1.20  
    1.21 -    val text = File.read(path)
    1.22 -    Symbol.decode_strict(text)
    1.23 -    f(text)
    1.24 +    val reader = Scan.byte_reader(path.file)
    1.25 +    try { f(reader) } finally { reader.close }
    1.26    }
    1.27  
    1.28  
    1.29 @@ -84,11 +84,11 @@
    1.30      }
    1.31    }
    1.32  
    1.33 -  def check_thy_text(qualifier: String, name: Document.Node.Name, text: CharSequence)
    1.34 +  def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
    1.35      : Document.Node.Header =
    1.36    {
    1.37      try {
    1.38 -      val header = Thy_Header.read(text)
    1.39 +      val header = Thy_Header.read(reader).decode_symbols
    1.40  
    1.41        val base_name = Long_Name.base_name(name.theory)
    1.42        val name1 = header.name
    1.43 @@ -103,7 +103,7 @@
    1.44    }
    1.45  
    1.46    def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
    1.47 -    with_thy_text(name, check_thy_text(qualifier, name, _))
    1.48 +    with_thy_reader(name, check_thy_reader(qualifier, name, _))
    1.49  
    1.50  
    1.51    /* document changes */
     2.1 --- a/src/Pure/Thy/thy_header.scala	Fri May 02 12:27:40 2014 +0200
     2.2 +++ b/src/Pure/Thy/thy_header.scala	Fri May 02 13:52:45 2014 +0200
     2.3 @@ -67,13 +67,16 @@
     2.4  
     2.5      val args =
     2.6        theory_name ~
     2.7 -      (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
     2.8 -      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~
     2.9 +      (opt(keyword(IMPORTS) ~! (rep1(theory_xname))) ^^
    2.10 +        { case None => Nil case Some(_ ~ xs) => xs }) ~
    2.11 +      (opt(keyword(KEYWORDS) ~! keyword_decls) ^^
    2.12 +        { case None => Nil case Some(_ ~ xs) => xs }) ~
    2.13        keyword(BEGIN) ^^
    2.14        { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
    2.15  
    2.16      (keyword(HEADER) ~ tags) ~!
    2.17 -      ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
    2.18 +      ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^
    2.19 +        { case _ ~ x => x } |
    2.20      (keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
    2.21    }
    2.22  
    2.23 @@ -119,5 +122,13 @@
    2.24  {
    2.25    def map(f: String => String): Thy_Header =
    2.26      Thy_Header(f(name), imports.map(f), keywords)
    2.27 +
    2.28 +  def decode_symbols: Thy_Header =
    2.29 +  {
    2.30 +    val f = Symbol.decode _
    2.31 +    Thy_Header(f(name), imports.map(f),
    2.32 +      keywords.map({ case (a, b, c) =>
    2.33 +        (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f))  }), c.map(f)) }))
    2.34 +  }
    2.35  }
    2.36  
     3.1 --- a/src/Pure/Thy/thy_info.scala	Fri May 02 12:27:40 2014 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.scala	Fri May 02 13:52:45 2014 +0200
     3.3 @@ -30,7 +30,7 @@
     3.4    {
     3.5      def loaded_files(syntax: Prover.Syntax): List[String] =
     3.6      {
     3.7 -      val string = resources.with_thy_text(name, _.toString)
     3.8 +      val string = resources.with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
     3.9        resources.loaded_files(syntax, string)
    3.10      }
    3.11    }
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri May 02 12:27:40 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri May 02 13:52:45 2014 +0200
     4.3 @@ -70,7 +70,7 @@
     4.4      if (is_theory) {
     4.5        JEdit_Lib.buffer_lock(buffer) {
     4.6          Exn.capture {
     4.7 -          PIDE.resources.check_thy_text("", node_name, buffer.getSegment(0, buffer.getLength))
     4.8 +          PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer))
     4.9          } match {
    4.10            case Exn.Res(header) => header
    4.11            case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
     5.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri May 02 12:27:40 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri May 02 13:52:45 2014 +0200
     5.3 @@ -14,6 +14,7 @@
     5.4  import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
     5.5  
     5.6  import scala.annotation.tailrec
     5.7 +import scala.util.parsing.input.CharSequenceReader
     5.8  
     5.9  import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
    5.10  import org.gjt.sp.jedit.gui.KeyEventWorkaround
    5.11 @@ -97,6 +98,9 @@
    5.12    def buffer_text(buffer: JEditBuffer): String =
    5.13      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    5.14  
    5.15 +  def buffer_reader(buffer: JEditBuffer): CharSequenceReader =
    5.16 +    new CharSequenceReader(buffer.getSegment(0, buffer.getLength))
    5.17 +
    5.18    def buffer_mode(buffer: JEditBuffer): String =
    5.19    {
    5.20      val mode = buffer.getMode
     6.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Fri May 02 12:27:40 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri May 02 13:52:45 2014 +0200
     6.3 @@ -13,6 +13,8 @@
     6.4  import java.io.{File => JFile, ByteArrayOutputStream}
     6.5  import javax.swing.text.Segment
     6.6  
     6.7 +import scala.util.parsing.input.Reader
     6.8 +
     6.9  import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    6.10  import org.gjt.sp.jedit.MiscUtilities
    6.11  import org.gjt.sp.jedit.{jEdit, View, Buffer}
    6.12 @@ -58,21 +60,19 @@
    6.13      }
    6.14    }
    6.15  
    6.16 -  override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A =
    6.17 +  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    6.18    {
    6.19      Swing_Thread.now {
    6.20        JEdit_Lib.jedit_buffer(name) match {
    6.21          case Some(buffer) =>
    6.22 -          JEdit_Lib.buffer_lock(buffer) {
    6.23 -            Some(consume(buffer.getSegment(0, buffer.getLength)))
    6.24 -          }
    6.25 +          JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
    6.26          case None => None
    6.27        }
    6.28      } getOrElse {
    6.29 -      if (Url.is_wellformed(name.node)) consume(Url.read(name.node))
    6.30 +      if (Url.is_wellformed(name.node)) f(Scan.byte_reader(Url(name.node)))
    6.31        else {
    6.32          val file = new JFile(name.node)
    6.33 -        if (file.isFile) consume(File.read(file))
    6.34 +        if (file.isFile) f(Scan.byte_reader(file))
    6.35          else error("No such file: " + quote(file.toString))
    6.36        }
    6.37      }