src/Tools/VSCode/src/vscode_resources.scala
changeset 64834 0a7179ad430d
parent 64833 0f410e3b1d20
child 64839 842163abfc0d
     1.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 13:08:17 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 14:46:04 2017 +0100
     1.3 @@ -67,6 +67,28 @@
     1.4      else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
     1.5    }
     1.6  
     1.7 +  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
     1.8 +  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
     1.9 +
    1.10 +
    1.11 +  /* file content */
    1.12 +
    1.13 +  def read_file_content(file: JFile): Option[String] =
    1.14 +    try { Some(Line.normalize(File.read(file))) }
    1.15 +    catch { case ERROR(_) => None }
    1.16 +
    1.17 +  def get_file_content(file: JFile): Option[String] =
    1.18 +    get_model(file) match {
    1.19 +      case Some(model) => Some(model.content.text)
    1.20 +      case None => read_file_content(file)
    1.21 +    }
    1.22 +
    1.23 +  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    1.24 +    for {
    1.25 +      (_, model) <- state.value.models.iterator
    1.26 +      Text.Info(range, entry) <- model.content.bibtex_entries.iterator
    1.27 +    } yield Text.Info(range, (entry, model))
    1.28 +
    1.29    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.30    {
    1.31      val file = node_file(name)
    1.32 @@ -83,15 +105,6 @@
    1.33  
    1.34    /* document models */
    1.35  
    1.36 -  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
    1.37 -  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
    1.38 -
    1.39 -  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    1.40 -    for {
    1.41 -      (_, model) <- state.value.models.iterator
    1.42 -      Text.Info(range, entry) <- model.content.bibtex_entries.iterator
    1.43 -    } yield Text.Info(range, (entry, model))
    1.44 -
    1.45    def visible_node(name: Document.Node.Name): Boolean =
    1.46      get_model(name) match {
    1.47        case Some(model) => model.node_visible
    1.48 @@ -136,19 +149,6 @@
    1.49        })
    1.50  
    1.51  
    1.52 -  /* file content */
    1.53 -
    1.54 -  def read_file_content(file: JFile): Option[String] =
    1.55 -    try { Some(Line.normalize(File.read(file))) }
    1.56 -    catch { case ERROR(_) => None }
    1.57 -
    1.58 -  def get_file_content(file: JFile): Option[String] =
    1.59 -    get_model(file) match {
    1.60 -      case Some(model) => Some(model.content.text)
    1.61 -      case None => read_file_content(file)
    1.62 -    }
    1.63 -
    1.64 -
    1.65    /* resolve dependencies */
    1.66  
    1.67    val thy_info = new Thy_Info(this)