# HG changeset patch # User wenzelm # Date 1369244691 -7200 # Node ID 352ea4b159ffb67826cf91b8e8f1bf17d890c174 # Parent 411db77f96f2886053bfd628a5c8f2cdea019c4c# Parent abf9fcfa65cf19d11157b67271d1f9244ecd5543 merged diff -r 411db77f96f2 -r 352ea4b159ff NEWS --- 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) diff -r 411db77f96f2 -r 352ea4b159ff bin/isabelle_scala_script --- /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 "$@" + diff -r 411db77f96f2 -r 352ea4b159ff lib/Tools/install --- 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" diff -r 411db77f96f2 -r 352ea4b159ff src/Doc/System/Scala.thy --- 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 diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/PIDE/markup.ML --- 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)]; diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/PIDE/markup.scala --- 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 } } diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/PIDE/protocol.ML --- 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; diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/PIDE/protocol.scala --- 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) - } } diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/System/invoke_scala.ML --- 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; diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/System/invoke_scala.scala --- 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 _) +} + diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/System/isabelle_process.ML --- 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); diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/System/isabelle_system.scala --- 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 } } diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/System/session.ML --- 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; diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/System/session.scala --- 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) } diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/Tools/build.scala --- 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)) diff -r 411db77f96f2 -r 352ea4b159ff src/Pure/Tools/build_dialog.scala --- 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) }