src/Tools/jEdit/src/jedit_resources.scala
changeset 64835 fd1efd6dd385
parent 64834 0a7179ad430d
child 64836 3611f759f896
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 14:46:04 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 16:47:53 2017 +0100
     1.3 @@ -67,6 +67,18 @@
     1.4  
     1.5    /* file content */
     1.6  
     1.7 +  def read_file_content(node_name: Document.Node.Name): Option[String] =
     1.8 +  {
     1.9 +    val name = node_name.node
    1.10 +    try {
    1.11 +      val text =
    1.12 +        if (Url.is_wellformed(name)) Url.read(Url(name))
    1.13 +        else File.read(new JFile(name))
    1.14 +      Some(Symbol.decode(Line.normalize(text)))
    1.15 +    }
    1.16 +    catch { case ERROR(_) => None }
    1.17 +  }
    1.18 +
    1.19    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.20    {
    1.21      GUI_Thread.now {
    1.22 @@ -104,7 +116,7 @@
    1.23      }
    1.24    }
    1.25  
    1.26 -  def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
    1.27 +  def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
    1.28  
    1.29  
    1.30    /* theory text edits */