equal
deleted
inserted
replaced
27 def is_pure(name: String): Boolean = name == Thy_Header.PURE |
27 def is_pure(name: String): Boolean = name == Thy_Header.PURE |
28 |
28 |
29 |
29 |
30 def exclude_session(name: String): Boolean = name == "" || name == DRAFT |
30 def exclude_session(name: String): Boolean = name == "" || name == DRAFT |
31 |
31 |
32 def exclude_theory(name: String): Boolean = name == root_name |
32 def exclude_theory(name: String): Boolean = |
|
33 name == root_name || name == "README" || name == "index" |
33 |
34 |
34 |
35 |
35 /* base info and source dependencies */ |
36 /* base info and source dependencies */ |
36 |
37 |
37 object Known |
38 object Known |