--- a/lib/Tools/build Thu Dec 06 11:27:44 2012 +0100
+++ b/lib/Tools/build Thu Dec 06 11:42:23 2012 +0100
@@ -148,7 +148,6 @@
if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
echo -n "Finished at "; date
-
fi
. "$ISABELLE_HOME/lib/scripts/timestop.bash"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/build_dialog Thu Dec 06 11:42:23 2012 +0100
@@ -0,0 +1,91 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: build Isabelle session images via GUI dialog
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [OPTIONS] SESSION"
+ echo
+ echo " Options are:"
+ echo " -C check for existing image"
+ echo " -d DIR include session directory"
+ echo " -s system build mode: produce output in ISABELLE_HOME"
+ echo
+ echo " Build Isabelle session image via GUI dialog."
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+CHECK_EXISTING=false
+declare -a INCLUDE_DIRS=()
+SYSTEM_MODE=false
+
+while getopts "Cd:s" OPT
+do
+ case "$OPT" in
+ C)
+ CHECK_EXISTING="true"
+ ;;
+ d)
+ INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
+ ;;
+ s)
+ SYSTEM_MODE="true"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ "$#" -ne 1 ] && usage
+
+SESSION="$1"; shift
+
+
+## existing image
+
+EXISTING=false
+if [ "$CHECK_EXISTING" = true ]; then
+ declare -a ISABELLE_PATHS=()
+ splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}")
+
+ for DIR in "${ISABELLE_PATHS[@]}"
+ do
+ FILE="$DIR/$ML_IDENTIFIER/$SESSION"
+ [ -f "$FILE" ] && EXISTING=true
+ done
+fi
+
+
+## build
+
+if [ "$EXISTING" = false ]; then
+ [ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
+
+ "$ISABELLE_TOOL" java isabelle.Build_Dialog \
+ "$SYSTEM_MODE" "$SESSION" "${INCLUDE_DIRS[@]}"
+fi
+
--- a/src/Pure/System/build.scala Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Pure/System/build.scala Thu Dec 06 11:42:23 2012 +0100
@@ -1,5 +1,6 @@
/* Title: Pure/System/build.scala
Author: Makarius
+ Options: :folding=explicit:collapseFolds=1:
Build and manage Isabelle sessions.
*/
@@ -18,6 +19,21 @@
object Build
{
+ /** progress context **/
+
+ class Progress {
+ def echo(msg: String) {}
+ def stopped: Boolean = false
+ }
+
+ object Ignore_Progress extends Progress
+
+ object Console_Progress extends Progress {
+ override def echo(msg: String) { java.lang.System.out.println(msg) }
+ }
+
+
+
/** session information **/
// external version
@@ -263,10 +279,6 @@
/** build **/
- private def echo(msg: String) { java.lang.System.out.println(msg) }
- private def sleep(): Unit = Thread.sleep(500)
-
-
/* queue */
object Queue
@@ -334,8 +346,8 @@
def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
}
- def dependencies(inlined_files: Boolean, verbose: Boolean, list_files: Boolean,
- tree: Session_Tree): Deps =
+ def dependencies(progress: Build.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)) =>
val (preloaded, parent_syntax, parent_errors) =
@@ -352,7 +364,7 @@
val groups =
if (info.groups.isEmpty) ""
else info.groups.mkString(" (", " ", ")")
- echo("Session " + name + groups)
+ progress.echo("Session " + name + groups)
}
val thy_deps =
@@ -371,7 +383,7 @@
}).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
if (list_files)
- echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
+ progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
val sources =
try { all_files.map(p => (p, SHA1.digest(p.file))) }
@@ -390,7 +402,7 @@
val options = Options.init
val (_, tree) =
find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, List(session))
- dependencies(inlined_files, false, false, tree)(session)
+ dependencies(Build.Ignore_Progress, inlined_files, false, false, tree)(session)
}
def outer_syntax(session: String): Outer_Syntax =
@@ -537,6 +549,7 @@
/* build */
def build(
+ progress: Build.Progress,
requirements: Boolean = false,
all_sessions: Boolean = false,
build_heap: Boolean = false,
@@ -556,7 +569,7 @@
val (selected, selected_tree) =
full_tree.selection(requirements, all_sessions, session_groups, sessions)
- val deps = dependencies(true, verbose, list_files, selected_tree)
+ val deps = dependencies(progress, true, verbose, list_files, selected_tree)
val queue = Queue(selected_tree)
def make_stamp(name: String): String =
@@ -581,27 +594,33 @@
for (name <- full_tree.graph.all_succs(selected)) {
val files =
List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
- if (!files.isEmpty) echo("Cleaning " + name + " ...")
- if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
+ if (!files.isEmpty) progress.echo("Cleaning " + name + " ...")
+ if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
}
}
// scheduler loop
case class Result(current: Boolean, heap: String, rc: Int)
+ def sleep(): Unit = Thread.sleep(500)
+
@tailrec def loop(
pending: Queue,
running: Map[String, (String, Job)],
results: Map[String, Result]): Map[String, Result] =
{
if (pending.is_empty) results
+ else if (progress.stopped) {
+ for ((_, (_, job)) <- running) job.terminate
+ sleep(); loop(pending, running, results)
+ }
else
running.find({ case (_, (_, job)) => job.is_finished }) match {
case Some((name, (parent_heap, job))) =>
- // finish job
+ //{{{ finish job
val (out, err, rc) = job.join
- echo(Library.trim_line(err))
+ progress.echo(Library.trim_line(err))
val heap =
if (rc == 0) {
@@ -619,20 +638,20 @@
(output_dir + log_gz(name)).file.delete
File.write(output_dir + log(name), out)
- echo(name + " FAILED")
+ progress.echo(name + " FAILED")
if (rc != 130) {
- echo("(see also " + (output_dir + log(name)).file.toString + ")")
+ progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
val lines = split_lines(out)
val tail = lines.drop(lines.length - 20 max 0)
- echo("\n" + cat_lines(tail))
+ progress.echo("\n" + cat_lines(tail))
}
no_heap
}
loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
-
+ //}}}
case None if (running.size < (max_jobs max 1)) =>
- // check/start next job
+ //{{{ check/start next job
pending.dequeue(running.isDefinedAt(_)) match {
case Some((name, info)) =>
val parent_result =
@@ -662,27 +681,28 @@
if (all_current)
loop(pending - name, running, results + (name -> Result(true, heap, 0)))
else if (no_build) {
- if (verbose) echo("Skipping " + name + " ...")
+ if (verbose) progress.echo("Skipping " + name + " ...")
loop(pending - name, running, results + (name -> Result(false, heap, 1)))
}
else if (parent_result.rc == 0) {
- echo((if (do_output) "Building " else "Running ") + name + " ...")
+ progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
val job = new Job(name, info, output, do_output, verbose, browser_info)
loop(pending, running + (name -> (parent_result.heap, job)), results)
}
else {
- echo(name + " CANCELLED")
+ progress.echo(name + " CANCELLED")
loop(pending - name, running, results + (name -> Result(false, heap, 1)))
}
case None => sleep(); loop(pending, running, results)
}
+ ///}}}
case None => sleep(); loop(pending, running, results)
}
}
val results =
if (deps.is_empty) {
- echo("### Nothing to build")
+ progress.echo("### Nothing to build")
Map.empty
}
else loop(queue, Map.empty, Map.empty)
@@ -692,7 +712,7 @@
val unfinished =
(for ((name, res) <- results.iterator if res.rc != 0) yield name).toList
.sorted(scala.math.Ordering.String) // FIXME scala-2.10.0-RC1
- echo("Unfinished session(s): " + commas(unfinished))
+ progress.echo("Unfinished session(s): " + commas(unfinished))
}
rc
}
@@ -718,8 +738,9 @@
val dirs =
select_dirs.map(d => (true, Path.explode(d))) :::
include_dirs.map(d => (false, Path.explode(d)))
- build(requirements, all_sessions, build_heap, clean_build, dirs, session_groups,
- max_jobs, list_files, no_build, build_options, system_mode, verbose, sessions)
+ build(Build.Console_Progress, requirements, all_sessions, build_heap, clean_build,
+ dirs, session_groups, max_jobs, list_files, no_build, build_options, system_mode,
+ verbose, sessions)
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/build_dialog.scala Thu Dec 06 11:42:23 2012 +0100
@@ -0,0 +1,118 @@
+/* Title: Pure/System/build_dialog.scala
+ Author: Makarius
+
+Dialog for session build process.
+*/
+
+package isabelle
+
+
+import java.awt.{GraphicsEnvironment, Point, Font}
+
+import scala.swing.{ScrollPane, Button, CheckBox, FlowPanel,
+ BorderPanel, MainFrame, TextArea, SwingApplication}
+import scala.swing.event.ButtonClicked
+
+
+object Build_Dialog extends SwingApplication
+{
+ def startup(args: Array[String]) =
+ {
+ Platform.init_laf()
+
+ try {
+ args.toList match {
+ case
+ Properties.Value.Boolean(system_mode) ::
+ session :: include_dirs =>
+ val center = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
+ val top = build_dialog(system_mode, include_dirs.map(Path.explode), session)
+ top.pack()
+ top.location = new Point(center.x - top.size.width / 2, center.y - top.size.height / 2)
+ top.visible = true
+ case _ => error("Bad arguments:\n" + cat_lines(args))
+ }
+ }
+ catch {
+ case exn: Throwable =>
+ Library.error_dialog(null, "Isabelle build failure",
+ Library.scrollable_text(Exn.message(exn)))
+ sys.exit(2)
+ }
+ }
+
+
+ def build_dialog(
+ system_mode: Boolean,
+ include_dirs: List[Path],
+ session: String): MainFrame = new MainFrame
+ {
+ /* GUI state */
+
+ private var is_stopped = false
+ private var return_code = 0
+
+
+ /* text */
+
+ val text = new TextArea {
+ font = new Font("SansSerif", Font.PLAIN, 14)
+ editable = false
+ columns = 40
+ rows = 10
+ }
+
+ val progress = new Build.Progress
+ {
+ override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
+ override def stopped: Boolean =
+ Swing_Thread.now { val b = is_stopped; is_stopped = false; b }
+ }
+
+
+ /* action button */
+
+ var button_action: () => Unit = (() => is_stopped = true)
+ val button = new Button("Cancel") {
+ reactions += { case ButtonClicked(_) => button_action() }
+ }
+ def button_exit(rc: Int)
+ {
+ button.text = if (rc == 0) "OK" else "Exit"
+ button_action = (() => sys.exit(rc))
+ button.peer.getRootPane.setDefaultButton(button.peer)
+ }
+
+ val action_panel = new FlowPanel(FlowPanel.Alignment.Center)(button)
+
+
+ /* layout panel */
+
+ val layout_panel = new BorderPanel
+ layout_panel.layout(new ScrollPane(text)) = BorderPanel.Position.Center
+ layout_panel.layout(action_panel) = BorderPanel.Position.South
+
+ contents = layout_panel
+
+
+ /* main build */
+
+ title = "Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")"
+ progress.echo("Build started for Isabelle/" + session + " ...")
+
+ default_thread_pool.submit(() => {
+ val (out, rc) =
+ try {
+ ("",
+ Build.build(progress, build_heap = true,
+ system_mode = system_mode, sessions = List(session)))
+ }
+ catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
+ Swing_Thread.now {
+ progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
+ button_exit(rc)
+ }
+ })
+ }
+}
+
--- a/src/Pure/System/session.scala Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Pure/System/session.scala Thu Dec 06 11:42:23 2012 +0100
@@ -465,14 +465,6 @@
def cancel_execution() { session_actor ! Cancel_Execution }
- def edit(edits: List[Document.Edit_Text])
+ def update(edits: List[Document.Edit_Text])
{ session_actor !? Session.Raw_Edits(edits) }
-
- def edit_node(name: Document.Node.Name,
- header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
- {
- edit(List(header_edit(name, header),
- name -> Document.Node.Edits(text_edits),
- name -> Document.Node.Perspective(perspective)))
- }
}
--- a/src/Pure/build-jars Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Pure/build-jars Thu Dec 06 11:42:23 2012 +0100
@@ -39,6 +39,7 @@
PIDE/xml.scala
PIDE/yxml.scala
System/build.scala
+ System/build_dialog.scala
System/color_value.scala
System/command_line.scala
System/event_bus.scala
--- a/src/Tools/jEdit/lib/Tools/jedit Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Dec 06 11:42:23 2012 +0100
@@ -68,8 +68,9 @@
echo " -f fresh build"
echo " -j OPTION add jEdit runtime option"
echo " (default JEDIT_OPTIONS=$JEDIT_OPTIONS)"
- echo " -l NAME logic image name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
+ echo " -l NAME logic session name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
echo " -m MODE add print mode for output"
+ echo " -s system build mode for session image"
echo
echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
echo "(default \"$USER_HOME/Scratch.thy\")."
@@ -93,6 +94,8 @@
# options
+declare -a BUILD_DIALOG_OPTIONS=()
+
BUILD_ONLY=false
BUILD_JARS="jars"
JEDIT_SESSION_DIRS=""
@@ -102,7 +105,7 @@
function getoptions()
{
OPTIND=1
- while getopts "J:bd:fj:l:m:" OPT
+ while getopts "J:bd:fj:l:m:s" OPT
do
case "$OPT" in
J)
@@ -117,6 +120,8 @@
else
JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
fi
+ BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-d"
+ BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"
;;
f)
BUILD_JARS="jars_fresh"
@@ -134,6 +139,9 @@
JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG"
fi
;;
+ s)
+ BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-s"
+ ;;
\?)
usage
;;
@@ -303,17 +311,16 @@
fi
-# run
+# build logic
+
+"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -C "$JEDIT_LOGIC"
+RC="$?"
+[ "$RC" = 0 ] || exit "$RC"
+
+
+# main
[ "$BUILD_ONLY" = true ] || {
- case "$JEDIT_LOGIC" in
- /*)
- ;;
- */*)
- JEDIT_LOGIC="$(pwd -P)/$JEDIT_LOGIC"
- ;;
- esac
-
export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
--- a/src/Tools/jEdit/src/document_model.scala Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Thu Dec 06 11:42:23 2012 +0100
@@ -79,8 +79,6 @@
/* perspective */
- def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
-
def node_perspective(): Text.Perspective =
{
Swing_Thread.require()
@@ -92,7 +90,7 @@
}
- /* initial edits */
+ /* edits */
def init_edits(): List[Document.Edit_Text] =
{
@@ -107,6 +105,17 @@
name -> Document.Node.Perspective(perspective))
}
+ def node_edits(perspective: Text.Perspective, text_edits: List[Text.Edit])
+ : List[Document.Edit_Text] =
+ {
+ Swing_Thread.require()
+ val header = node_header()
+
+ List(session.header_edit(name, header),
+ name -> Document.Node.Edits(text_edits),
+ name -> Document.Node.Perspective(perspective))
+ }
+
/* pending edits */
@@ -126,7 +135,7 @@
if (!edits.isEmpty || last_perspective != new_perspective) {
pending.clear
last_perspective = new_perspective
- session.edit_node(name, node_header(), new_perspective, edits)
+ session.update(node_edits(new_perspective, edits))
}
}
@@ -148,7 +157,7 @@
def init()
{
flush()
- session.edit(init_edits())
+ session.update(init_edits())
}
def exit()
@@ -167,7 +176,7 @@
def full_perspective()
{
pending_edits.flush()
- session.edit_node(name, node_header(), Text.Perspective(List(buffer_range())), Nil)
+ session.update(node_edits(Text.Perspective(List(JEdit_Lib.buffer_range(buffer))), Nil))
}
--- a/src/Tools/jEdit/src/document_view.scala Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Thu Dec 06 11:42:23 2012 +0100
@@ -79,7 +79,7 @@
def perspective(): Text.Perspective =
{
Swing_Thread.require()
- val buffer_range = model.buffer_range()
+ val buffer_range = JEdit_Lib.buffer_range(model.buffer)
Text.Perspective(
for {
i <- 0 until text_area.getVisibleLines
--- a/src/Tools/jEdit/src/isabelle_logic.scala Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Thu Dec 06 11:42:23 2012 +0100
@@ -27,7 +27,7 @@
override def toString = description
}
- private val opt_name = "jedit_logic"
+ private val option_name = "jedit_logic"
def logic_selector(autosave: Boolean): Option_Component =
{
@@ -35,20 +35,20 @@
val entries =
new Logic_Entry("", "default (" + default_logic() + ")") ::
- Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
+ Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name))
val component = new ComboBox(entries) with Option_Component {
- name = opt_name
+ name = option_name
val title = "Logic"
def load: Unit =
{
- val logic = PIDE.options.string(opt_name)
+ val logic = PIDE.options.string(option_name)
entries.find(_.name == logic) match {
case Some(entry) => selection.item = entry
case None =>
}
}
- def save: Unit = PIDE.options.string(opt_name) = selection.item.name
+ def save: Unit = PIDE.options.string(option_name) = selection.item.name
}
component.load()
@@ -56,7 +56,7 @@
component.listenTo(component.selection)
component.reactions += { case SelectionChanged(_) => component.save() }
}
- component.tooltip = PIDE.options.value.check_name(opt_name).print_default
+ component.tooltip = "Logic session name (change requires restart)"
component
}
@@ -64,17 +64,25 @@
{
val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
val logic =
- PIDE.options.string(opt_name) match {
+ PIDE.options.string(option_name) match {
case "" => default_logic()
case logic => logic
}
modes ::: List(logic)
}
+ def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+
+ def session_list(): List[String] =
+ {
+ val dirs = session_dirs().map((false, _))
+ Build.find_sessions(PIDE.options.value, dirs).topological_order.map(_._1).sorted
+ }
+
def session_content(inlined_files: Boolean): Build.Session_Content =
{
- val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
- val name = Path.explode(session_args().last).base.implode // FIXME more robust
+ val dirs = session_dirs()
+ val name = session_args().last
Build.session_content(inlined_files, dirs, name).check_errors
}
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Dec 06 11:42:23 2012 +0100
@@ -112,6 +112,12 @@
catch { case _: ArrayIndexOutOfBoundsException => None }
+ /* buffer range */
+
+ def buffer_range(buffer: JEditBuffer): Text.Range =
+ Text.Range(0, (buffer.getLength - 1) max 0)
+
+
/* point range */
def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
--- a/src/Tools/jEdit/src/plugin.scala Thu Dec 06 11:27:44 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Dec 06 11:42:23 2012 +0100
@@ -1,7 +1,7 @@
/* Title: Tools/jEdit/src/plugin.scala
Author: Makarius
-Main Isabelle/jEdit plugin setup.
+Main plumbing for PIDE infrastructure as jEdit plugin.
*/
package isabelle.jedit
@@ -15,7 +15,7 @@
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
-import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
+import org.gjt.sp.jedit.syntax.ModeProvider
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.util.SyntaxUtilities
@@ -95,7 +95,7 @@
model_edits ::: edits
}
}
- PIDE.session.edit(init_edits)
+ PIDE.session.update(init_edits)
}
}
@@ -122,8 +122,8 @@
def check_buffer(buffer: Buffer)
{
PIDE.document_model(buffer) match {
+ case Some(model) => model.full_perspective()
case None =>
- case Some(model) => model.full_perspective()
}
}