equal
deleted
inserted
replaced
86 theory <- Url.get_base_name(name.node) |
86 theory <- Url.get_base_name(name.node) |
87 if detect(name.node) && theory_suffix.nonEmpty |
87 if detect(name.node) && theory_suffix.nonEmpty |
88 } |
88 } |
89 yield { |
89 yield { |
90 val node = resources.append_path(name.node, Path.explode(theory_suffix)) |
90 val node = resources.append_path(name.node, Path.explode(theory_suffix)) |
91 val master_dir = Url.strip_base_name(node).getOrElse("") |
91 Document.Node.Name(node, theory = theory) |
92 Document.Node.Name(node, master_dir = master_dir, theory = theory) |
|
93 } |
92 } |
94 } |
93 } |
95 |
94 |
96 def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = { |
95 def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = { |
97 for { |
96 for { |