src/Pure/System/session_manager.scala
author wenzelm
Thu, 30 Jun 2011 14:55:01 +0200
changeset 43606 e1a09c2a6248
parent 37072 9105c8237c7a
child 43661 39fdbd814c7f
permissions -rw-r--r--
prefer Isabelle path algebra;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34165
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/isabelle_manager.scala
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     3
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     4
Isabelle session manager.
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     5
*/
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     6
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     7
package isabelle
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     8
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
     9
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    10
import java.io.{File, FileFilter}
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    11
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    12
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    13
class Session_Manager(system: Isabelle_System)
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    14
{
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    15
  val ROOT_NAME = "session.root"
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    16
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    17
  def is_session_file(file: File): Boolean =
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    18
    file.isFile && file.getName == ROOT_NAME
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    19
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    20
  def is_session_dir(dir: File): Boolean =
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    21
    dir.isDirectory && (new File(dir, ROOT_NAME)).isFile
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    22
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    23
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    24
  // FIXME handle (potentially cyclic) directory graph
37072
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 34165
diff changeset
    25
  private def find_sessions(reverse_prefix: List[String], reverse_sessions: List[List[String]],
34165
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    26
    dir: File): List[List[String]] =
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    27
  {
37072
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 34165
diff changeset
    28
    val (reverse_prefix1, reverse_sessions1) =
34165
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    29
      if (is_session_dir(dir)) {
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    30
        val name = dir.getName  // FIXME from root file
37072
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 34165
diff changeset
    31
        val reverse_prefix1 = name :: reverse_prefix
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 34165
diff changeset
    32
        val reverse_sessions1 = reverse_prefix1.reverse :: reverse_sessions
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 34165
diff changeset
    33
        (reverse_prefix1, reverse_sessions1)
34165
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    34
      }
37072
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 34165
diff changeset
    35
      else (reverse_prefix, reverse_sessions)
34165
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    36
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    37
    val subdirs =
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    38
      dir.listFiles(new FileFilter { def accept(entry: File) = entry.isDirectory })
37072
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 34165
diff changeset
    39
    (reverse_sessions1 /: subdirs)(find_sessions(reverse_prefix1, _, _))
34165
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    40
  }
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    41
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    42
  def component_sessions(): List[List[String]] =
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    43
  {
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    44
    val toplevel_sessions =
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 37072
diff changeset
    45
      system.components().map(s => system.platform_file(Path.explode(s))).filter(is_session_dir)
34165
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    46
    ((Nil: List[List[String]]) /: toplevel_sessions)(find_sessions(Nil, _, _)).reverse
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    47
  }
557b1c60f27f Isabelle session manager -- most basic setup;
wenzelm
parents:
diff changeset
    48
}