src/Pure/System/session_manager.scala
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 37072 9105c8237c7a
child 43606 e1a09c2a6248
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
     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 
    13 class Session_Manager(system: Isabelle_System)
    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
    25   private def find_sessions(reverse_prefix: List[String], reverse_sessions: List[List[String]],
    26     dir: File): List[List[String]] =
    27   {
    28     val (reverse_prefix1, reverse_sessions1) =
    29       if (is_session_dir(dir)) {
    30         val name = dir.getName  // FIXME from root file
    31         val reverse_prefix1 = name :: reverse_prefix
    32         val reverse_sessions1 = reverse_prefix1.reverse :: reverse_sessions
    33         (reverse_prefix1, reverse_sessions1)
    34       }
    35       else (reverse_prefix, reverse_sessions)
    36 
    37     val subdirs =
    38       dir.listFiles(new FileFilter { def accept(entry: File) = entry.isDirectory })
    39     (reverse_sessions1 /: subdirs)(find_sessions(reverse_prefix1, _, _))
    40   }
    41 
    42   def component_sessions(): List[List[String]] =
    43   {
    44     val toplevel_sessions =
    45       system.components().map(system.platform_file(_)).filter(is_session_dir)
    46     ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
    47   }
    48 }