equal
deleted
inserted
replaced
16 |
16 |
17 object Sessions |
17 object Sessions |
18 { |
18 { |
19 /* Pure */ |
19 /* Pure */ |
20 |
20 |
21 def pure_name(name: String): Boolean = name == "Pure" |
21 def pure_name(name: String): Boolean = name == Thy_Header.PURE |
22 |
22 |
23 def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] = |
23 def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] = |
24 { |
24 { |
25 val roots = Thy_Header.ml_roots.map(_._1) |
25 val roots = Thy_Header.ml_roots.map(_._1) |
26 val loaded_files = |
26 val loaded_files = |