equal
deleted
inserted
replaced
13 import java.io.{File => JFile} |
13 import java.io.{File => JFile} |
14 |
14 |
15 |
15 |
16 class Resources( |
16 class Resources( |
17 val session_base: Sessions.Base, |
17 val session_base: Sessions.Base, |
18 val default_qualifier: String = Sessions.DRAFT, |
|
19 val log: Logger = No_Logger) |
18 val log: Logger = No_Logger) |
20 { |
19 { |
21 val thy_info = new Thy_Info(this) |
20 val thy_info = new Thy_Info(this) |
22 |
21 |
23 def thy_path(path: Path): Path = path.ext("thy") |
22 def thy_path(path: Path): Path = path.ext("thy") |