# HG changeset patch # User wenzelm # Date 1342723937 -7200 # Node ID 04fed0cf775a52fc10e970f82901ad605be31c65 # Parent 828ace4f75ab06327c637a6d7033bdc9d0315fcd# Parent 6b36da29a0bf2c2eedb67052ccc77567b73c2a3d merged diff -r 828ace4f75ab -r 04fed0cf775a src/FOL/ROOT --- 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 diff -r 828ace4f75ab -r 04fed0cf775a src/HOL/ROOT --- 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 diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/Concurrent/simple_thread.scala --- 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) } diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/General/graph.ML --- 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; diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/General/graph.scala --- 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) diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/General/properties.scala --- 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))) diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/Isar/parse.scala --- 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) diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/Isar/token.scala --- 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 || diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/ROOT --- /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 *) + diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/System/build.scala --- 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) + } } } diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/System/command_line.scala --- /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) + } +} + diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/System/isabelle_process.scala --- 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() diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/System/isabelle_system.scala --- 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 "" + } + /* system tools */ diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/build-jars --- 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 diff -r 828ace4f75ab -r 04fed0cf775a src/Pure/library.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 diff -r 828ace4f75ab -r 04fed0cf775a src/ZF/ROOT --- 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