575 entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) }) |
575 entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) }) |
576 |
576 |
577 val meta_digest = |
577 val meta_digest = |
578 SHA1.digest( |
578 SHA1.digest( |
579 (name, chapter, entry.parent, entry.directories, entry.options, entry.imports, |
579 (name, chapter, entry.parent, entry.directories, entry.options, entry.imports, |
580 entry.theories_no_position, conditions, entry.document_theories, entry.document_files) |
580 entry.theories_no_position, conditions, entry.document_theories_no_position, |
|
581 entry.document_files) |
581 .toString) |
582 .toString) |
582 |
583 |
583 Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path, |
584 Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path, |
584 entry.parent, entry.description, directories, session_options, |
585 entry.parent, entry.description, directories, session_options, |
585 entry.imports, theories, global_theories, entry.document_theories, document_files, |
586 entry.imports, theories, global_theories, entry.document_theories, document_files, |
875 document_files: List[(String, String)], |
876 document_files: List[(String, String)], |
876 export_files: List[(String, Int, List[String])]) extends Entry |
877 export_files: List[(String, Int, List[String])]) extends Entry |
877 { |
878 { |
878 def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = |
879 def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = |
879 theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) |
880 theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) |
|
881 def document_theories_no_position: List[String] = |
|
882 document_theories.map(_._1) |
880 } |
883 } |
881 |
884 |
882 private object Parser extends Options.Parser |
885 private object Parser extends Options.Parser |
883 { |
886 { |
884 private val chapter: Parser[Chapter] = |
887 private val chapter: Parser[Chapter] = |