--- a/NEWS Wed May 22 12:39:09 2013 +0200
+++ b/NEWS Wed May 22 19:44:51 2013 +0200
@@ -250,6 +250,9 @@
* Isabelle settings variable ISABELLE_BUILD_JAVA_OPTIONS allows to
specify global resources of the JVM process run by isabelle build.
+* Toplevel executable $ISABELLE_HOME/bin/isabelle_scala_script allows
+to run Isabelle/Scala source files as standalone programs.
+
New in Isabelle2013 (February 2013)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/bin/isabelle_scala_script Wed May 22 19:44:51 2013 +0200
@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Isabelle/Scala script wrapper.
+
+if [ -L "$0" ]; then
+ TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+ exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+fi
+
+
+## settings
+
+PRG="$(basename "$0")"
+
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
+source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
+
+
+## main
+
+exec "$ISABELLE_TOOL" scala -howtorun:script -nocompdaemon "$@"
+
--- a/lib/Tools/install Wed May 22 12:39:09 2013 +0200
+++ b/lib/Tools/install Wed May 22 19:44:51 2013 +0200
@@ -63,7 +63,7 @@
mkdir -p "$BINDIR" || fail "Bad directory: \"$BINDIR\""
-for NAME in isabelle isabelle-process
+for NAME in isabelle isabelle-process isabelle_scala_script
do
BIN="$BINDIR/$NAME"
DIST="$DISTDIR/bin/$NAME"
--- a/src/Doc/System/Scala.thy Wed May 22 12:39:09 2013 +0200
+++ b/src/Doc/System/Scala.thy Wed May 22 19:44:51 2013 +0200
@@ -48,6 +48,7 @@
scala> isabelle.Isabelle_System.getenv("ISABELLE_HOME")
scala> val options = isabelle.Options.init()
scala> options.bool("browser_info")
+ scala> options.string("document")
\end{alltt}
*}
@@ -69,4 +70,28 @@
adding plugin components, which needs special attention since
it overrides the standard Java class loader. *}
+
+section {* Scala script wrapper *}
+
+text {* The executable @{executable
+ "$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run
+ Isabelle/Scala source files stand-alone programs, by using a
+ suitable ``hash-bang'' line and executable file permissions.
+
+ The subsequent example assumes that the main Isabelle binaries have
+ been installed in some directory that is included in @{setting PATH}
+ (see also @{tool "install"}):
+
+\begin{alltt}
+#!/usr/bin/env isabelle_scala_script
+
+val options = isabelle.Options.init()
+Console.println("browser_info = " + options.bool("browser_info"))
+Console.println("document = " + options.string("document"))
+\end{alltt}
+
+ Alternatively the full @{"file"
+ "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in
+ expanded form. *}
+
end
--- a/src/Pure/PIDE/markup.ML Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Wed May 22 19:44:51 2013 +0200
@@ -142,6 +142,7 @@
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
+ val protocol_handler: string -> Properties.T
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
val ML_statistics: Properties.entry
@@ -461,6 +462,8 @@
val assign_execs = [(functionN, "assign_execs")];
val removed_versions = [(functionN, "removed_versions")];
+fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)];
+
fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
--- a/src/Pure/PIDE/markup.scala Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/PIDE/markup.scala Wed May 22 19:44:51 2013 +0200
@@ -316,19 +316,31 @@
val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
+ object Protocol_Handler
+ {
+ def unapply(props: Properties.T): Option[(String)] =
+ props match {
+ case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name)
+ case _ => None
+ }
+ }
+
+ val INVOKE_SCALA = "invoke_scala"
object Invoke_Scala
{
def unapply(props: Properties.T): Option[(String, String)] =
props match {
- case List((FUNCTION, "invoke_scala"), (NAME, name), (ID, id)) => Some((name, id))
+ case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
case _ => None
}
}
+
+ val CANCEL_SCALA = "cancel_scala"
object Cancel_Scala
{
def unapply(props: Properties.T): Option[String] =
props match {
- case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
+ case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
case _ => None
}
}
--- a/src/Pure/PIDE/protocol.ML Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Wed May 22 19:44:51 2013 +0200
@@ -78,11 +78,5 @@
Active.dialog_result (Markup.parse_int serial) result
handle exn => if Exn.is_interrupt exn then () else reraise exn);
-val _ =
- Isabelle_Process.protocol_command "Document.invoke_scala"
- (fn [id, tag, res] =>
- Invoke_Scala.fulfill_method id tag res
- handle exn => if Exn.is_interrupt exn then () else reraise exn);
-
end;
--- a/src/Pure/PIDE/protocol.scala Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed May 22 19:44:51 2013 +0200
@@ -364,12 +364,4 @@
{
input("Document.dialog_result", Properties.Value.Long(serial), result)
}
-
-
- /* method invocation service */
-
- def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String)
- {
- input("Document.invoke_scala", id, tag.toString, res)
- }
}
--- a/src/Pure/System/invoke_scala.ML Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/System/invoke_scala.ML Wed May 22 19:44:51 2013 +0200
@@ -6,16 +6,15 @@
signature INVOKE_SCALA =
sig
- exception Null
val method: string -> string -> string
val promise_method: string -> string -> string future
- val fulfill_method: string -> string -> string -> unit
+ exception Null
end;
structure Invoke_Scala: INVOKE_SCALA =
struct
-exception Null;
+val _ = Session.protocol_handler "isabelle.Invoke_Scala";
(* pending promises *)
@@ -40,9 +39,11 @@
fun method name arg = Future.join (promise_method name arg);
-(* fulfill method *)
+(* fulfill *)
-fun fulfill_method id tag res =
+exception Null;
+
+fun fulfill id tag res =
let
val result =
(case tag of
@@ -58,5 +59,11 @@
val _ = Future.fulfill_result promise result;
in () end;
+val _ =
+ Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
+ (fn [id, tag, res] =>
+ fulfill id tag res
+ handle exn => if Exn.is_interrupt exn then () else reraise exn);
+
end;
--- a/src/Pure/System/invoke_scala.scala Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/System/invoke_scala.scala Wed May 22 19:44:51 2013 +0200
@@ -64,3 +64,69 @@
case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
}
}
+
+
+/* protocol handler */
+
+class Invoke_Scala extends Session.Protocol_Handler
+{
+ private var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
+
+ private def fulfill(prover: Session.Prover,
+ id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit = synchronized
+ {
+ if (futures.isDefinedAt(id)) {
+ prover.input("Invoke_Scala.fulfill", id, tag.toString, res)
+ futures -= id
+ }
+ }
+
+ private def cancel(prover: Session.Prover,
+ id: String, future: java.util.concurrent.Future[Unit])
+ {
+ future.cancel(true)
+ fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
+ }
+
+ private def invoke_scala(
+ prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized
+ {
+ output.properties match {
+ case Markup.Invoke_Scala(name, id) =>
+ futures += (id ->
+ default_thread_pool.submit(() =>
+ {
+ val arg = XML.content(output.body)
+ val (tag, result) = Invoke_Scala.method(name, arg)
+ fulfill(prover, id, tag, result)
+ }))
+ true
+ case _ => false
+ }
+ }
+
+ private def cancel_scala(
+ prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized
+ {
+ output.properties match {
+ case Markup.Cancel_Scala(id) =>
+ futures.get(id) match {
+ case Some(future) => cancel(prover, id, future)
+ case None =>
+ }
+ true
+ case _ => false
+ }
+ }
+
+ override def stop(prover: Session.Prover): Unit = synchronized
+ {
+ for ((id, future) <- futures) cancel(prover, id, future)
+ futures = Map.empty
+ }
+
+ val functions = Map(
+ Markup.INVOKE_SCALA -> invoke_scala _,
+ Markup.CANCEL_SCALA -> cancel_scala _)
+}
+
--- a/src/Pure/System/isabelle_process.ML Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed May 22 19:44:51 2013 +0200
@@ -221,6 +221,7 @@
val channel = rendezvous ();
val _ = init_channels channel;
+ val _ = Session.init_protocol_handlers ();
in loop channel end));
fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
--- a/src/Pure/System/isabelle_system.scala Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed May 22 19:44:51 2013 +0200
@@ -305,8 +305,8 @@
private def kill(signal: String): Boolean =
{
try {
- execute(true, "kill", "-" + signal, "-" + pid).waitFor
- execute(true, "kill", "-0", "-" + pid).waitFor == 0
+ execute(true, "kill", "-" + signal, "--", "-" + pid).waitFor
+ execute(true, "kill", "-0", "--", "-" + pid).waitFor == 0
}
catch { case _: InterruptedException => true }
}
--- a/src/Pure/System/session.ML Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/System/session.ML Wed May 22 19:44:51 2013 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/System/session.ML
Author: Makarius
-Session management -- internal state of logic images (not thread-safe).
+Session management -- internal state of logic images.
*)
signature SESSION =
@@ -11,12 +11,14 @@
val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
string -> string * string -> bool * string -> bool -> unit
val finish: unit -> unit
+ val protocol_handler: string -> unit
+ val init_protocol_handlers: unit -> unit
end;
structure Session: SESSION =
struct
-(* session state *)
+(** session identification -- not thread-safe **)
val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
val session_finished = Unsynchronized.ref false;
@@ -58,4 +60,20 @@
Event_Timer.shutdown ();
session_finished := true);
+
+(** protocol handlers **)
+
+val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
+
+fun protocol_handler name =
+ Synchronized.change protocol_handlers (fn handlers =>
+ (Output.try_protocol_message (Markup.protocol_handler name) "";
+ if not (member (op =) handlers name) then ()
+ else warning ("Redefining protocol handler: " ^ quote name);
+ update (op =) name handlers));
+
+fun init_protocol_handlers () =
+ Synchronized.value protocol_handlers
+ |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
+
end;
--- a/src/Pure/System/session.scala Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/System/session.scala Wed May 22 19:44:51 2013 +0200
@@ -37,6 +37,74 @@
case object Ready extends Phase
case object Shutdown extends Phase // transient
//}}}
+
+
+ /* protocol handlers */
+
+ type Prover = Isabelle_Process with Protocol
+
+ abstract class Protocol_Handler
+ {
+ def stop(prover: Prover): Unit = {}
+ val functions: Map[String, (Prover, Isabelle_Process.Output) => Boolean]
+ }
+
+ class Protocol_Handlers(
+ handlers: Map[String, Session.Protocol_Handler] = Map.empty,
+ functions: Map[String, Isabelle_Process.Output => Boolean] = Map.empty)
+ {
+ def add(prover: Prover, name: String): Protocol_Handlers =
+ {
+ val (handlers1, functions1) =
+ handlers.get(name) match {
+ case Some(old_handler) =>
+ System.err.println("Redefining protocol handler: " + name)
+ old_handler.stop(prover)
+ (handlers - name, functions -- old_handler.functions.keys)
+ case None => (handlers, functions)
+ }
+
+ val (handlers2, functions2) =
+ try {
+ val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
+ val new_functions =
+ for ((a, f) <- new_handler.functions.toList) yield
+ (a, (output: Isabelle_Process.Output) => f(prover, output))
+
+ val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
+ if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
+
+ (handlers1 + (name -> new_handler), functions1 ++ new_functions)
+ }
+ catch {
+ case exn: Throwable =>
+ System.err.println("Failed to initialize protocol handler: " +
+ name + "\n" + Exn.message(exn))
+ (handlers1, functions1)
+ }
+
+ new Protocol_Handlers(handlers2, functions2)
+ }
+
+ def invoke(output: Isabelle_Process.Output): Boolean =
+ output.properties match {
+ case Markup.Function(a) if functions.isDefinedAt(a) =>
+ try { functions(a)(output) }
+ catch {
+ case exn: Throwable =>
+ System.err.println("Failed invocation of protocol function: " +
+ quote(a) + "\n" + Exn.message(exn))
+ false
+ }
+ case _ => false
+ }
+
+ def stop(prover: Prover): Protocol_Handlers =
+ {
+ for ((_, handler) <- handlers) handler.stop(prover)
+ new Protocol_Handlers()
+ }
+ }
}
@@ -176,16 +244,15 @@
previous: Document.Version,
version: Document.Version)
private case class Messages(msgs: List[Isabelle_Process.Message])
- private case class Finished_Scala(id: String, tag: Invoke_Scala.Tag.Value, result: String)
private case class Update_Options(options: Options)
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
{
val this_actor = self
- var prune_next = System.currentTimeMillis() + prune_delay.ms
+ var protocol_handlers = new Session.Protocol_Handlers()
- var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
+ var prune_next = System.currentTimeMillis() + prune_delay.ms
/* buffered prover messages */
@@ -222,7 +289,7 @@
def cancel() { timer.cancel() }
}
- var prover: Option[Isabelle_Process with Protocol] = None
+ var prover: Option[Session.Prover] = None
/* delayed command changes */
@@ -318,73 +385,68 @@
}
}
- output.properties match {
+ if (output.is_protocol) {
+ val handled = protocol_handlers.invoke(output)
+ if (!handled) {
+ output.properties match {
+ case Markup.Protocol_Handler(name) =>
+ protocol_handlers = protocol_handlers.add(prover.get, name)
- case Position.Id(state_id) if !output.is_protocol =>
- accumulate(state_id, output.message)
-
- case Protocol.Command_Timing(state_id, timing) if output.is_protocol =>
- val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
- accumulate(state_id, prover.get.xml_cache.elem(message))
+ case Protocol.Command_Timing(state_id, timing) =>
+ val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
+ accumulate(state_id, prover.get.xml_cache.elem(message))
- case Markup.Assign_Execs if output.is_protocol =>
- XML.content(output.body) match {
- case Protocol.Assign(id, assign) =>
- try {
- val cmds = global_state >>> (_.assign(id, assign))
- delay_commands_changed.invoke(true, cmds)
+ case Markup.Assign_Execs =>
+ XML.content(output.body) match {
+ case Protocol.Assign(id, assign) =>
+ try {
+ val cmds = global_state >>> (_.assign(id, assign))
+ delay_commands_changed.invoke(true, cmds)
+ }
+ catch { case _: Document.State.Fail => bad_output() }
+ case _ => bad_output()
+ }
+ // FIXME separate timeout event/message!?
+ if (prover.isDefined && System.currentTimeMillis() > prune_next) {
+ val old_versions = global_state >>> (_.prune_history(prune_size))
+ if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
+ prune_next = System.currentTimeMillis() + prune_delay.ms
}
- catch { case _: Document.State.Fail => bad_output() }
+
+ case Markup.Removed_Versions =>
+ XML.content(output.body) match {
+ case Protocol.Removed(removed) =>
+ try {
+ global_state >> (_.removed_versions(removed))
+ }
+ catch { case _: Document.State.Fail => bad_output() }
+ case _ => bad_output()
+ }
+
+ case Markup.ML_Statistics(props) =>
+ statistics.event(Session.Statistics(props))
+
+ case Markup.Task_Statistics(props) =>
+ // FIXME
+
case _ => bad_output()
}
- // FIXME separate timeout event/message!?
- if (prover.isDefined && System.currentTimeMillis() > prune_next) {
- val old_versions = global_state >>> (_.prune_history(prune_size))
- if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
- prune_next = System.currentTimeMillis() + prune_delay.ms
- }
-
- case Markup.Removed_Versions if output.is_protocol =>
- XML.content(output.body) match {
- case Protocol.Removed(removed) =>
- try {
- global_state >> (_.removed_versions(removed))
- }
- catch { case _: Document.State.Fail => bad_output() }
- case _ => bad_output()
- }
+ }
+ }
+ else {
+ output.properties match {
+ case Position.Id(state_id) =>
+ accumulate(state_id, output.message)
- case Markup.Invoke_Scala(name, id) if output.is_protocol =>
- futures += (id ->
- default_thread_pool.submit(() =>
- {
- val arg = XML.content(output.body)
- val (tag, result) = Invoke_Scala.method(name, arg)
- this_actor ! Finished_Scala(id, tag, result)
- }))
+ case _ if output.is_init =>
+ phase = Session.Ready
- case Markup.Cancel_Scala(id) if output.is_protocol =>
- futures.get(id) match {
- case Some(future) =>
- future.cancel(true)
- this_actor ! Finished_Scala(id, Invoke_Scala.Tag.INTERRUPT, "")
- case None =>
- }
-
- case Markup.ML_Statistics(props) if output.is_protocol =>
- statistics.event(Session.Statistics(props))
+ case Markup.Return_Code(rc) if output.is_exit =>
+ if (rc == 0) phase = Session.Inactive
+ else phase = Session.Failed
- case Markup.Task_Statistics(props) if output.is_protocol =>
- // FIXME
-
- case _ if output.is_init =>
- phase = Session.Ready
-
- case Markup.Return_Code(rc) if output.is_exit =>
- if (rc == 0) phase = Session.Inactive
- else phase = Session.Failed
-
- case _ => bad_output()
+ case _ => bad_output()
+ }
}
}
//}}}
@@ -406,6 +468,7 @@
case Stop =>
if (phase == Session.Ready) {
+ protocol_handlers = protocol_handlers.stop(prover.get)
global_state >> (_ => Document.State.init) // FIXME event bus!?
phase = Session.Shutdown
prover.get.terminate
@@ -455,12 +518,6 @@
if prover.isDefined && global_state().is_assigned(change.previous) =>
handle_change(change)
- case Finished_Scala(id, tag, result) if prover.isDefined =>
- if (futures.isDefinedAt(id)) {
- prover.get.invoke_scala(id, tag, result)
- futures -= id
- }
-
case bad if !bad.isInstanceOf[Change] =>
System.err.println("session_actor: ignoring bad message " + bad)
}
--- a/src/Pure/Tools/build.scala Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/Tools/build.scala Wed May 22 19:44:51 2013 +0200
@@ -404,7 +404,7 @@
def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
}
- def dependencies(progress: Build.Progress, inlined_files: Boolean,
+ def dependencies(progress: Progress, inlined_files: Boolean,
verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
@@ -458,7 +458,7 @@
val options = Options.init()
val (_, tree) =
find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
- dependencies(Build.Ignore_Progress, inlined_files, false, false, tree)(session)
+ dependencies(Ignore_Progress, inlined_files, false, false, tree)(session)
}
def outer_syntax(session: String): Outer_Syntax =
@@ -467,7 +467,7 @@
/* jobs */
- private class Job(progress: Build.Progress,
+ private class Job(progress: Progress,
name: String, val info: Session_Info, output: Path, do_output: Boolean,
verbose: Boolean, browser_info: Path, command_timings: List[Properties.T])
{
@@ -648,11 +648,11 @@
else None
- /* build */
+ /* build_results */
- def build(
- progress: Build.Progress,
+ def build_results(
options: Options,
+ progress: Progress = Ignore_Progress,
requirements: Boolean = false,
all_sessions: Boolean = false,
build_heap: Boolean = false,
@@ -664,7 +664,7 @@
no_build: Boolean = false,
system_mode: Boolean = false,
verbose: Boolean = false,
- sessions: List[String] = Nil): Int =
+ sessions: List[String] = Nil): Map[String, Int] =
{
/* session tree and dependencies */
@@ -889,12 +889,39 @@
}
- /* return code */
+ /* results */
+
+ results.map({ case (name, result) => (name, result.rc) })
+ }
+
+
+ /* build */
- val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
+ def build(
+ options: Options,
+ progress: Progress = Ignore_Progress,
+ requirements: Boolean = false,
+ all_sessions: Boolean = false,
+ build_heap: Boolean = false,
+ clean_build: Boolean = false,
+ more_dirs: List[(Boolean, Path)] = Nil,
+ session_groups: List[String] = Nil,
+ max_jobs: Int = 1,
+ list_files: Boolean = false,
+ no_build: Boolean = false,
+ system_mode: Boolean = false,
+ verbose: Boolean = false,
+ sessions: List[String] = Nil): Int =
+ {
+ val results =
+ build_results(options, progress, requirements, all_sessions,
+ build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
+ system_mode, verbose, sessions)
+
+ val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
if (rc != 0 && (verbose || !no_build)) {
val unfinished =
- (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted
+ (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted
progress.echo("Unfinished session(s): " + commas(unfinished))
}
rc
@@ -919,13 +946,13 @@
Properties.Value.Boolean(verbose) ::
Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
val options = (Options.init() /: build_options)(_ + _)
- val dirs =
+ val more_dirs =
select_dirs.map(d => (true, Path.explode(d))) :::
include_dirs.map(d => (false, Path.explode(d)))
- val progress = new Build.Console_Progress(verbose)
+ val progress = new Console_Progress(verbose)
progress.interrupt_handler {
- build(progress, options, requirements, all_sessions,
- build_heap, clean_build, dirs, session_groups, max_jobs, list_files, no_build,
+ build(options, progress, requirements, all_sessions,
+ build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
system_mode, verbose, sessions)
}
case _ => error("Bad arguments:\n" + cat_lines(args))
--- a/src/Pure/Tools/build_dialog.scala Wed May 22 12:39:09 2013 +0200
+++ b/src/Pure/Tools/build_dialog.scala Wed May 22 19:44:51 2013 +0200
@@ -33,7 +33,7 @@
Isabelle_System.default_logic(logic,
if (logic_option != "") options.string(logic_option) else "")
- if (Build.build(Build.Ignore_Progress, options, build_heap = true, no_build = true,
+ if (Build.build(options = options, build_heap = true, no_build = true,
more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
else
Swing_Thread.later {
@@ -167,7 +167,8 @@
val (out, rc) =
try {
("",
- Build.build(progress, options, build_heap = true, more_dirs = more_dirs,
+ Build.build(options = options, progress = progress,
+ build_heap = true, more_dirs = more_dirs,
system_mode = system_mode, sessions = List(session)))
}
catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }