--- a/src/FOL/ROOT Thu Jul 19 19:38:39 2012 +0200
+++ b/src/FOL/ROOT Thu Jul 19 20:52:17 2012 +0200
@@ -1,4 +1,4 @@
-session FOL! in "." = Pure +
+session FOL! (10) in "." = Pure +
description "First-Order Logic with Natural Deduction"
options [proofs = 2]
theories FOL
--- a/src/HOL/ROOT Thu Jul 19 19:38:39 2012 +0200
+++ b/src/HOL/ROOT Thu Jul 19 20:52:17 2012 +0200
@@ -1,4 +1,4 @@
-session HOL! in "." = Pure +
+session HOL! (1) in "." = Pure +
description {* Classical Higher-order Logic *}
options [document_graph]
theories Complex_Main
@@ -19,12 +19,12 @@
options [document = false]
theories Main
-session "HOL-Proofs"! in "." = Pure +
+session "HOL-Proofs"! (2) in "." = Pure +
description {* HOL-Main with proof terms *}
options [document = false, proofs = 2, parallel_proofs = false]
theories Main
-session HOLCF! = HOL +
+session HOLCF! (3) = HOL +
description {*
Author: Franz Regensburger
Author: Brian Huffman
--- a/src/Pure/Concurrent/simple_thread.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala Thu Jul 19 20:52:17 2012 +0200
@@ -30,11 +30,11 @@
/* future result via thread */
- def future[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] =
+ def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
{
val result = Future.promise[A]
- fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
- result
+ val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
+ (thread, result)
}
--- a/src/Pure/General/graph.ML Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/General/graph.ML Thu Jul 19 20:52:17 2012 +0200
@@ -144,7 +144,7 @@
let
fun reach x (rs, R) =
if Keys.member R x then (rs, R)
- else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
+ else Keys.fold_rev reach (next x) (rs, Keys.insert x R) |>> cons x;
fun reachs x (rss, R) =
reach x ([], R) |>> (fn rs => rs :: rss);
in fold reachs xs ([], Keys.empty) end;
--- a/src/Pure/General/graph.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/General/graph.scala Thu Jul 19 20:52:17 2012 +0200
@@ -14,9 +14,9 @@
object Graph
{
- class Duplicate[Key](x: Key) extends Exception
- class Undefined[Key](x: Key) extends Exception
- class Cycles[Key](cycles: List[List[Key]]) extends Exception
+ class Duplicate[Key](val key: Key) extends Exception
+ class Undefined[Key](val key: Key) extends Exception
+ class Cycles[Key](val cycles: List[List[Key]]) extends Exception
def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
new Graph[Key, A](SortedMap.empty(ord))
@@ -73,19 +73,19 @@
/*nodes reachable from xs -- topologically sorted for acyclic graphs*/
def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) =
{
- def reach(reached: (List[Key], Keys), x: Key): (List[Key], Keys) =
+ def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) =
{
val (rs, r_set) = reached
if (r_set(x)) reached
else {
- val (rs1, r_set1) = ((rs, r_set + x) /: next(x))(reach)
+ val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach)
(x :: rs1, r_set1)
}
}
def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) =
{
val (rss, r_set) = reached
- val (rs, r_set1) = reach((Nil, r_set), x)
+ val (rs, r_set1) = reach(x, (Nil, r_set))
(rs :: rss, r_set1)
}
((List.empty[List[Key]], empty_keys) /: xs)(reachs)
@@ -209,7 +209,7 @@
}
}
- def add_deps_cyclic(y: Key, xs: List[Key]): Graph[Key, A] =
+ def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] =
(this /: xs)(_.add_edge_acyclic(_, y))
def topological_order: List[Key] = all_succs(minimals)
--- a/src/Pure/General/properties.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/General/properties.scala Thu Jul 19 20:52:17 2012 +0200
@@ -14,6 +14,17 @@
object Value
{
+ object Boolean
+ {
+ def apply(x: scala.Boolean): java.lang.String = x.toString
+ def unapply(s: java.lang.String): Option[scala.Boolean] =
+ s match {
+ case "true" => Some(true)
+ case "false" => Some(false)
+ case _ => None
+ }
+ }
+
object Int
{
def apply(x: scala.Int): java.lang.String = x.toString
@@ -52,6 +63,16 @@
props.find(_._1 == name).map(_._2)
}
+ class Boolean(val name: java.lang.String)
+ {
+ def apply(value: scala.Boolean): T = List((name, Value.Boolean(value)))
+ def unapply(props: T): Option[scala.Boolean] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Value.Boolean.unapply(value)
+ }
+ }
+
class Int(val name: java.lang.String)
{
def apply(value: scala.Int): T = List((name, Value.Int(value)))
--- a/src/Pure/Isar/parse.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/Isar/parse.scala Thu Jul 19 20:52:17 2012 +0200
@@ -54,6 +54,7 @@
tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
def string: Parser[String] = atom("string", _.is_string)
+ def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
def name: Parser[String] = atom("name declaration", _.is_name)
def xname: Parser[String] = atom("name reference", _.is_xname)
def text: Parser[String] = atom("text", _.is_text)
--- a/src/Pure/Isar/token.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/Isar/token.scala Thu Jul 19 20:52:17 2012 +0200
@@ -74,6 +74,7 @@
kind == Token.Kind.VERBATIM ||
kind == Token.Kind.COMMENT
def is_string: Boolean = kind == Token.Kind.STRING
+ def is_nat: Boolean = kind == Token.Kind.NAT
def is_name: Boolean =
kind == Token.Kind.IDENT ||
kind == Token.Kind.SYM_IDENT ||
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ROOT Thu Jul 19 20:52:17 2012 +0200
@@ -0,0 +1,24 @@
+session RAW in "." =
+ files
+ "General/exn.ML"
+ "ML-Systems/compiler_polyml.ML"
+ "ML-Systems/ml_name_space.ML"
+ "ML-Systems/ml_pretty.ML"
+ "ML-Systems/ml_system.ML"
+ "ML-Systems/multithreading.ML"
+ "ML-Systems/multithreading_polyml.ML"
+ "ML-Systems/overloading_smlnj.ML"
+ "ML-Systems/polyml.ML"
+ "ML-Systems/pp_dummy.ML"
+ "ML-Systems/proper_int.ML"
+ "ML-Systems/single_assignment.ML"
+ "ML-Systems/single_assignment_polyml.ML"
+ "ML-Systems/smlnj.ML"
+ "ML-Systems/thread_dummy.ML"
+ "ML-Systems/universal.ML"
+ "ML-Systems/unsynchronized.ML"
+ "ML-Systems/use_context.ML"
+
+session Pure in "." =
+ files "ROOT.ML" (* FIXME *)
+
--- a/src/Pure/System/build.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/System/build.scala Thu Jul 19 20:52:17 2012 +0200
@@ -19,28 +19,76 @@
type Options = List[(String, Option[String])]
- case class Session_Info(
- dir: Path,
- name: String,
- parent: String,
- description: String,
- options: Options,
- theories: List[(Options, String)],
- files: List[String])
+ object Session
+ {
+ object Key
+ {
+ object Ordering extends scala.math.Ordering[Key]
+ {
+ def compare(key1: Key, key2: Key): Int =
+ key1.order compare key2.order match {
+ case 0 => key1.name compare key2.name
+ case ord => ord
+ }
+ }
+ }
+
+ sealed case class Key(name: String, order: Int)
+ {
+ override def toString: String = name
+ }
+
+ sealed case class Info(
+ dir: Path,
+ description: String,
+ options: Options,
+ theories: List[(Options, String)],
+ files: List[String])
- private val pure_info =
- Session_Info(Path.current, "Pure", "", "", Nil, List((Nil, "Pure")), Nil)
+ object Queue
+ {
+ val empty: Queue = new Queue()
+ }
+
+ final class Queue private(
+ keys: Map[String, Key] = Map.empty,
+ graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
+ {
+ def defined(name: String): Boolean = keys.isDefinedAt(name)
+
+ def + (key: Key, info: Info, parent: Option[String]): Queue =
+ {
+ val keys1 =
+ if (defined(key.name)) error("Duplicate session: " + quote(key.name))
+ else keys + (key.name -> key)
+
+ val graph1 =
+ try {
+ graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_)))
+ }
+ catch {
+ case exn: Graph.Cycles[_] =>
+ error(cat_lines(exn.cycles.map(cycle =>
+ "Cyclic session dependency of " +
+ cycle.map(key => quote(key.toString)).mkString(" via "))))
+ }
+ new Queue(keys1, graph1)
+ }
+
+ def topological_order: List[(Key, Info)] =
+ graph.topological_order.map(key => (key, graph.get_node(key)))
+ }
+ }
/* parsing */
- val ROOT_NAME = "ROOT"
-
private case class Session_Entry(
name: String,
reset: Boolean,
+ order: Int,
path: Option[String],
- parent: String,
+ parent: Option[String],
description: String,
options: Options,
theories: List[(Options, List[String])],
@@ -74,13 +122,14 @@
((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
(keyword("!") ^^^ true | success(false)) ~
+ (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
(opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
- (keyword("=") ~> session_name <~ keyword("+")) ~
+ (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
(keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
(keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
- rep1(theories) ~
+ rep(theories) ~
(keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
- { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(a, b, c, d, e, f, g, h) }
+ { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
}
def parse_entries(root: File): List[Session_Entry] =
@@ -96,50 +145,84 @@
/* find sessions */
- def find_sessions(more_dirs: List[Path]): List[Session_Info] =
+ private def sessions_root(dir: Path, root: File, sessions: Session.Queue): Session.Queue =
{
- val infos = new mutable.ListBuffer[Session_Info]
- infos += pure_info
+ (sessions /: Parser.parse_entries(root))((sessions1, entry) =>
+ try {
+ if (entry.name == "") error("Bad session name")
- for {
- (dir, strict) <- Isabelle_System.components().map((_, false)) ++ more_dirs.map((_, true))
- root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
- _ = (strict && !root.isFile && error("Bad session root file: " + quote(root.toString)))
- if root.isFile
- entry <- Parser.parse_entries(root)
- }
- {
- try {
- val parent =
- infos.find(_.name == entry.parent) getOrElse
- error("Unknown parent session: " + quote(entry.parent))
val full_name =
- if (entry.reset) entry.name
- else parent.name + "-" + entry.name
-
- if (entry.name == "") error("Bad session name")
- if (infos.exists(_.name == full_name))
- error("Duplicate session name: " + quote(full_name))
+ if (entry.name == "RAW" || entry.name == "Pure") {
+ if (entry.parent.isDefined) error("Illegal parent session")
+ else entry.name
+ }
+ else
+ entry.parent match {
+ case Some(parent_name) if sessions1.defined(parent_name) =>
+ if (entry.reset) entry.name
+ else parent_name + "-" + entry.name
+ case _ => error("Bad parent session")
+ }
val path =
entry.path match {
case Some(p) => Path.explode(p)
case None => Path.basic(entry.name)
}
- val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
- val info =
- Session_Info(dir + path, full_name, entry.parent, entry.description,
- entry.options, thys, entry.files)
- infos += info
+ val key = Session.Key(full_name, entry.order)
+ val info = Session.Info(dir + path, entry.description, entry.options,
+ entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
+
+ sessions1 + (key, info, entry.parent)
}
catch {
case ERROR(msg) =>
error(msg + "\nThe error(s) above occurred in session entry " +
quote(entry.name) + " (file " + quote(root.toString) + ")")
+ })
+ }
+
+ private def sessions_dir(strict: Boolean, dir: Path, sessions: Session.Queue): Session.Queue =
+ {
+ val root = Isabelle_System.platform_file(dir + Path.basic("ROOT"))
+ if (root.isFile) sessions_root(dir, root, sessions)
+ else if (strict) error("Bad session root file: " + quote(root.toString))
+ else sessions
+ }
+
+ private def sessions_catalog(dir: Path, catalog: File, sessions: Session.Queue): Session.Queue =
+ {
+ val dirs =
+ split_lines(Standard_System.read_file(catalog)).
+ filterNot(line => line == "" || line.startsWith("#"))
+ (sessions /: dirs)((sessions1, dir1) =>
+ try {
+ val dir2 = dir + Path.explode(dir1)
+ if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, sessions1)
+ else error("Bad session directory: " + dir2.toString)
}
+ catch {
+ case ERROR(msg) =>
+ error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
+ })
+ }
+
+ def find_sessions(more_dirs: List[Path]): Session.Queue =
+ {
+ var sessions = Session.Queue.empty
+
+ for (dir <- Isabelle_System.components()) {
+ sessions = sessions_dir(false, dir, sessions)
+
+ val catalog = Isabelle_System.platform_file(dir + Path.explode("etc/sessions"))
+ if (catalog.isFile)
+ sessions = sessions_catalog(dir, catalog, sessions)
}
- infos.toList
+
+ for (dir <- more_dirs) sessions = sessions_dir(true, dir, sessions)
+
+ sessions
}
@@ -153,53 +236,29 @@
println("options = " + options.toString)
println("sessions = " + sessions.toString)
- find_sessions(more_dirs) foreach println
+ for ((key, info) <- find_sessions(more_dirs).topological_order)
+ println(key.name + " in " + info.dir)
0
}
-
- /** command line entry point **/
-
- private object Bool
- {
- def unapply(s: String): Option[Boolean] =
- s match {
- case "true" => Some(true)
- case "false" => Some(false)
- case _ => None
- }
- }
-
- private object Chunks
- {
- private def chunks(list: List[String]): List[List[String]] =
- list.indexWhere(_ == "\n") match {
- case -1 => List(list)
- case i =>
- val (chunk, rest) = list.splitAt(i)
- chunk :: chunks(rest.tail)
- }
- def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
- }
+ /* command line entry point */
def main(args: Array[String])
{
- val rc =
- try {
- args.toList match {
- case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) ::
- Chunks(more_dirs, options, sessions) =>
- build(all_sessions, build_images, list_only,
- more_dirs.map(Path.explode), options, sessions)
- case _ => error("Bad arguments:\n" + cat_lines(args))
- }
+ Command_Line.tool {
+ args.toList match {
+ case
+ Properties.Value.Boolean(all_sessions) ::
+ Properties.Value.Boolean(build_images) ::
+ Properties.Value.Boolean(list_only) ::
+ Command_Line.Chunks(more_dirs, options, sessions) =>
+ build(all_sessions, build_images, list_only,
+ more_dirs.map(Path.explode), options, sessions)
+ case _ => error("Bad arguments:\n" + cat_lines(args))
}
- catch {
- case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
- }
- sys.exit(rc)
+ }
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/command_line.scala Thu Jul 19 20:52:17 2012 +0200
@@ -0,0 +1,32 @@
+/* Title: Pure/System/command_line.scala
+ Author: Makarius
+
+Support for Isabelle/Scala command line tools.
+*/
+
+package isabelle
+
+
+object Command_Line
+{
+ object Chunks
+ {
+ private def chunks(list: List[String]): List[List[String]] =
+ list.indexWhere(_ == "\n") match {
+ case -1 => List(list)
+ case i =>
+ val (chunk, rest) = list.splitAt(i)
+ chunk :: chunks(rest.tail)
+ }
+ def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
+ }
+
+ def tool(body: => Int): Nothing =
+ {
+ val rc =
+ try { body }
+ catch { case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 }
+ sys.exit(rc)
+ }
+}
+
--- a/src/Pure/System/isabelle_process.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala Thu Jul 19 20:52:17 2012 +0200
@@ -137,11 +137,11 @@
val cmdline =
Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
(system_channel.isabelle_args ::: args)
- new Isabelle_System.Managed_Process(false, cmdline: _*)
+ new Isabelle_System.Managed_Process(null, null, false, cmdline: _*)
}
catch { case e: IOException => system_channel.accepted(); throw(e) }
- val process_result =
+ val (_, process_result) =
Simple_Thread.future("process_result") { process.join }
private def terminate_process()
--- a/src/Pure/System/isabelle_system.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Jul 19 20:52:17 2012 +0200
@@ -160,22 +160,26 @@
/* plain execute */
- def execute(redirect: Boolean, args: String*): Process =
+ def execute_env(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
{
val cmdline =
if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
else args
- Standard_System.raw_execute(null, settings, redirect, cmdline: _*)
+ val env1 = if (env == null) settings else settings ++ env
+ Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)
}
+ def execute(redirect: Boolean, args: String*): Process =
+ execute_env(null, null, redirect, args: _*)
+
/* managed process */
- class Managed_Process(redirect: Boolean, args: String*)
+ class Managed_Process(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
{
private val params =
List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
- private val proc = execute(redirect, (params ++ args):_*)
+ private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
// channels
@@ -238,15 +242,15 @@
/* bash */
- def bash(script: String): (String, String, Int) =
+ def bash_env(cwd: File, env: Map[String, String], script: String): (String, String, Int) =
{
Standard_System.with_tmp_file("isabelle_script") { script_file =>
Standard_System.write_file(script_file, script)
- val proc = new Managed_Process(false, "bash", posix_path(script_file.getPath))
+ val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
proc.stdin.close
- val stdout = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
- val stderr = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
+ val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
+ val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
val rc =
try { proc.join }
@@ -255,6 +259,19 @@
}
}
+ def bash(script: String): (String, String, Int) = bash_env(null, null, script)
+
+ class Bash_Job(cwd: File, env: Map[String, String], script: String)
+ {
+ private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
+
+ def terminate: Unit = thread.interrupt
+ def is_finished: Boolean = result.is_finished
+ def join: (String, String, Int) = result.join
+
+ override def toString: String = if (is_finished) join._3.toString else "<running>"
+ }
+
/* system tools */
--- a/src/Pure/build-jars Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/build-jars Thu Jul 19 20:52:17 2012 +0200
@@ -40,6 +40,7 @@
PIDE/xml.scala
PIDE/yxml.scala
System/build.scala
+ System/command_line.scala
System/event_bus.scala
System/gui_setup.scala
System/invoke_scala.scala
--- a/src/Pure/library.scala Thu Jul 19 19:38:39 2012 +0200
+++ b/src/Pure/library.scala Thu Jul 19 20:52:17 2012 +0200
@@ -130,7 +130,7 @@
/* simple dialogs */
- def scrollable_text(txt: String, width: Int = 76, editable: Boolean = false): ScrollPane =
+ def scrollable_text(txt: String, width: Int = 80, editable: Boolean = false): ScrollPane =
{
val text = new TextArea(txt)
if (width > 0) text.columns = width
--- a/src/ZF/ROOT Thu Jul 19 19:38:39 2012 +0200
+++ b/src/ZF/ROOT Thu Jul 19 20:52:17 2012 +0200
@@ -1,4 +1,4 @@
-session ZF! in "." = FOL +
+session ZF! (10) in "." = FOL +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1995 University of Cambridge