| author | blanchet | 
| Thu, 19 Apr 2012 17:49:08 +0200 | |
| changeset 47606 | 06dde48a1503 | 
| parent 43669 | 9d34288e9351 | 
| permissions | -rw-r--r-- | 
| 34165 | 1 | /* Title: Pure/System/isabelle_manager.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 4 | Isabelle session manager. | |
| 5 | */ | |
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 10 | import java.io.{File, FileFilter}
 | |
| 11 | ||
| 12 | ||
| 43661 
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
 wenzelm parents: 
43606diff
changeset | 13 | class Session_Manager | 
| 34165 | 14 | {
 | 
| 15 | val ROOT_NAME = "session.root" | |
| 16 | ||
| 17 | def is_session_file(file: File): Boolean = | |
| 18 | file.isFile && file.getName == ROOT_NAME | |
| 19 | ||
| 20 | def is_session_dir(dir: File): Boolean = | |
| 21 | dir.isDirectory && (new File(dir, ROOT_NAME)).isFile | |
| 22 | ||
| 23 | ||
| 24 | // FIXME handle (potentially cyclic) directory graph | |
| 37072 
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
 wenzelm parents: 
34165diff
changeset | 25 | private def find_sessions(reverse_prefix: List[String], reverse_sessions: List[List[String]], | 
| 34165 | 26 | dir: File): List[List[String]] = | 
| 27 |   {
 | |
| 37072 
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
 wenzelm parents: 
34165diff
changeset | 28 | val (reverse_prefix1, reverse_sessions1) = | 
| 34165 | 29 |       if (is_session_dir(dir)) {
 | 
| 30 | val name = dir.getName // FIXME from root file | |
| 37072 
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
 wenzelm parents: 
34165diff
changeset | 31 | val reverse_prefix1 = name :: reverse_prefix | 
| 
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
 wenzelm parents: 
34165diff
changeset | 32 | val reverse_sessions1 = reverse_prefix1.reverse :: reverse_sessions | 
| 
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
 wenzelm parents: 
34165diff
changeset | 33 | (reverse_prefix1, reverse_sessions1) | 
| 34165 | 34 | } | 
| 37072 
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
 wenzelm parents: 
34165diff
changeset | 35 | else (reverse_prefix, reverse_sessions) | 
| 34165 | 36 | |
| 37 | val subdirs = | |
| 38 |       dir.listFiles(new FileFilter { def accept(entry: File) = entry.isDirectory })
 | |
| 37072 
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
 wenzelm parents: 
34165diff
changeset | 39 | (reverse_sessions1 /: subdirs)(find_sessions(reverse_prefix1, _, _)) | 
| 34165 | 40 | } | 
| 41 | ||
| 42 | def component_sessions(): List[List[String]] = | |
| 43 |   {
 | |
| 44 | val toplevel_sessions = | |
| 43669 | 45 | Isabelle_System.components().map(Isabelle_System.platform_file).filter(is_session_dir) | 
| 34165 | 46 | ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse | 
| 47 | } | |
| 48 | } |