# HG changeset patch # User wenzelm # Date 1354790543 -3600 # Node ID fe9223fdd0603ffc7974c12e2dd819aee560d710 # Parent 52d9720f7a48b5a668ae611cf57a08a4e2e8a748# Parent d9711842f1f9ed82db1140fd9a8a8f9354e45f1e merged diff -r 52d9720f7a48 -r fe9223fdd060 lib/Tools/build --- 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" diff -r 52d9720f7a48 -r fe9223fdd060 lib/Tools/build_dialog --- /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 + diff -r 52d9720f7a48 -r fe9223fdd060 src/Pure/System/build.scala --- 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)) } } diff -r 52d9720f7a48 -r fe9223fdd060 src/Pure/System/build_dialog.scala --- /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) + } + }) + } +} + diff -r 52d9720f7a48 -r fe9223fdd060 src/Pure/System/session.scala --- 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))) - } } diff -r 52d9720f7a48 -r fe9223fdd060 src/Pure/build-jars --- 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 diff -r 52d9720f7a48 -r fe9223fdd060 src/Tools/jEdit/lib/Tools/jedit --- 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[@]}" \ diff -r 52d9720f7a48 -r fe9223fdd060 src/Tools/jEdit/src/document_model.scala --- 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)) } diff -r 52d9720f7a48 -r fe9223fdd060 src/Tools/jEdit/src/document_view.scala --- 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 diff -r 52d9720f7a48 -r fe9223fdd060 src/Tools/jEdit/src/isabelle_logic.scala --- 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 } } diff -r 52d9720f7a48 -r fe9223fdd060 src/Tools/jEdit/src/jedit_lib.scala --- 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 = diff -r 52d9720f7a48 -r fe9223fdd060 src/Tools/jEdit/src/plugin.scala --- 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() } }