src/Pure/PIDE/resources.scala
changeset 66700 5174ce7c84f0
parent 66699 16fd7655d39d
child 66701 d181f8a0e857
equal deleted inserted replaced
66699:16fd7655d39d 66700:5174ce7c84f0
    64       val text = Symbol.decode(raw_text)
    64       val text = Symbol.decode(raw_text)
    65       if (syntax.load_commands_in(text)) {
    65       if (syntax.load_commands_in(text)) {
    66         val spans = syntax.parse_spans(text)
    66         val spans = syntax.parse_spans(text)
    67         val dir = Path.explode(name.master_dir)
    67         val dir = Path.explode(name.master_dir)
    68         spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
    68         spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
    69           map(a => dir + Path.explode(a)).toList
    69           map(a => (dir + Path.explode(a)).expand).toList
    70       }
    70       }
    71       else Nil
    71       else Nil
    72     }
    72     }
    73   }
    73   }
    74 
    74