src/Pure/PIDE/resources.scala
changeset 66695 91500c024c7f
parent 65532 febfd9f78bd4
child 66696 8f863dae78a0
equal deleted inserted replaced
66694:41177b124067 66695:91500c024c7f
    61     if (syntax.load_commands_in(text)) {
    61     if (syntax.load_commands_in(text)) {
    62       val spans = syntax.parse_spans(text)
    62       val spans = syntax.parse_spans(text)
    63       spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
    63       spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
    64     }
    64     }
    65     else Nil
    65     else Nil
       
    66 
       
    67   def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): List[Path] =
       
    68   {
       
    69     val text = with_thy_reader(name, reader => Symbol.decode(reader.source.toString))
       
    70     val dir = Path.explode(name.master_dir)
       
    71     loaded_files(syntax, text).map(a => dir + Path.explode(a))
       
    72   }
    66 
    73 
    67   def theory_qualifier(name: Document.Node.Name): String =
    74   def theory_qualifier(name: Document.Node.Name): String =
    68     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
    75     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
    69 
    76 
    70   def theory_name(qualifier: String, theory0: String): (Boolean, String) =
    77   def theory_name(qualifier: String, theory0: String): (Boolean, String) =