use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
authorwenzelm
Wed Aug 22 15:53:17 2012 +0200 (2012-08-22)
changeset 4888261dc7d5d150a
parent 48881 46e053eda5dd
child 48883 04cd2fddb4d9
use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
tuned signatures;
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_load.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_thy_load.scala
     1.1 --- a/src/Pure/Thy/thy_header.scala	Wed Aug 22 12:47:49 2012 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Wed Aug 22 15:53:17 2012 +0200
     1.3 @@ -106,13 +106,6 @@
     1.4    def read(source: CharSequence): Thy_Header =
     1.5      read(new CharSequenceReader(source))
     1.6  
     1.7 -  def read(file: JFile): Thy_Header =
     1.8 -  {
     1.9 -    val reader = Scan.byte_reader(file)
    1.10 -    try { read(reader).map(Standard_System.decode_permissive_utf8) }
    1.11 -    finally { reader.close }
    1.12 -  }
    1.13 -
    1.14  
    1.15    /* keywords */
    1.16  
     2.1 --- a/src/Pure/Thy/thy_load.scala	Wed Aug 22 12:47:49 2012 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.scala	Wed Aug 22 15:53:17 2012 +0200
     2.3 @@ -27,13 +27,6 @@
     2.4    def append(dir: String, source_path: Path): String =
     2.5      (Path.explode(dir) + source_path).expand.implode
     2.6  
     2.7 -  def read_header(name: Document.Node.Name): Thy_Header =
     2.8 -  {
     2.9 -    val path = Path.explode(name.node)
    2.10 -    if (!path.is_file) error("No such file: " + path.toString)
    2.11 -    Thy_Header.read(path.file)
    2.12 -  }
    2.13 -
    2.14  
    2.15    /* theory files */
    2.16  
    2.17 @@ -49,8 +42,9 @@
    2.18      }
    2.19    }
    2.20  
    2.21 -  def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header =
    2.22 +  def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
    2.23    {
    2.24 +    val header = Thy_Header.read(text)
    2.25      val name1 = header.name
    2.26      val imports = header.imports.map(import_name(name.dir, _))
    2.27      // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
    2.28 @@ -62,6 +56,10 @@
    2.29    }
    2.30  
    2.31    def check_thy(name: Document.Node.Name): Document.Node.Header =
    2.32 -    check_header(name, read_header(name))
    2.33 +  {
    2.34 +    val path = Path.explode(name.node)
    2.35 +    if (!path.is_file) error("No such file: " + path.toString)
    2.36 +    check_thy_text(name, File.read(path))
    2.37 +  }
    2.38  }
    2.39  
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 22 12:47:49 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 22 15:53:17 2012 +0200
     3.3 @@ -68,8 +68,7 @@
     3.4      Swing_Thread.require()
     3.5      Isabelle.buffer_lock(buffer) {
     3.6        Exn.capture {
     3.7 -        Isabelle.thy_load.check_header(name,
     3.8 -          Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
     3.9 +        Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
    3.10        } match {
    3.11          case Exn.Res(header) => header
    3.12          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
     4.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 12:47:49 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 15:53:17 2012 +0200
     4.3 @@ -53,22 +53,20 @@
     4.4      }
     4.5    }
     4.6  
     4.7 -  override def read_header(name: Document.Node.Name): Thy_Header =
     4.8 +  override def check_thy(name: Document.Node.Name): Document.Node.Header =
     4.9    {
    4.10      Swing_Thread.now {
    4.11        Isabelle.jedit_buffer(name.node) match {
    4.12          case Some(buffer) =>
    4.13            Isabelle.buffer_lock(buffer) {
    4.14 -            val text = new Segment
    4.15 -            buffer.getText(0, buffer.getLength, text)
    4.16 -            Some(Thy_Header.read(text))
    4.17 +            Some(check_thy_text(name, buffer.getSegment(0, buffer.getLength)))
    4.18            }
    4.19          case None => None
    4.20        }
    4.21      } getOrElse {
    4.22        val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
    4.23        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    4.24 -      Thy_Header.read(file)
    4.25 +      check_thy_text(name, File.read(file))
    4.26      }
    4.27    }
    4.28  }