# HG changeset patch # User wenzelm # Date 1354831630 -3600 # Node ID bf01be7d1a44c97710950214fa4b3a3c81b07ea9 # Parent e83ab94e3e6eeece73cf9a8b1b6df43c1dd58492# Parent 6ab3fadf43af3b6a1dfb7d9a72da873562110d34 merged diff -r e83ab94e3e6e -r bf01be7d1a44 NEWS --- a/NEWS Thu Dec 06 17:48:04 2012 +0100 +++ b/NEWS Thu Dec 06 23:07:10 2012 +0100 @@ -91,6 +91,11 @@ adjust the main text area font size, and its derivatives for output, tooltips etc. Cf. keyboard shortcuts C-PLUS and C-MINUS. +* Implicit check and build dialog of the specified logic session +image. For example, HOL, HOLCF, HOL-Nominal can be produced on +demand, without bundling big platform-dependent heap images in the +Isabelle distribution. + * Uniform Java 7 platform on Linux, Mac OS X, Windows: recent updates from Oracle provide better multi-platform experience. This version is now bundled exclusively with Isabelle. diff -r e83ab94e3e6e -r bf01be7d1a44 lib/Tools/build_dialog --- a/lib/Tools/build_dialog Thu Dec 06 17:48:04 2012 +0100 +++ b/lib/Tools/build_dialog Thu Dec 06 23:07:10 2012 +0100 @@ -12,14 +12,14 @@ function usage() { echo - echo "Usage: isabelle $PRG [OPTIONS] SESSION" + echo "Usage: isabelle $PRG [OPTIONS] LOGIC" echo echo " Options are:" - echo " -C check for existing image" + echo " -L OPTION default logic via system option" 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 " Build Isabelle session image LOGIC via GUI dialog." echo exit 1 } @@ -33,15 +33,15 @@ ## process command line -CHECK_EXISTING=false +LOGIC_OPTION="" declare -a INCLUDE_DIRS=() SYSTEM_MODE=false -while getopts "Cd:s" OPT +while getopts "L:d:s" OPT do case "$OPT" in - C) - CHECK_EXISTING="true" + L) + LOGIC_OPTION="$OPTARG" ;; d) INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG" @@ -62,30 +62,13 @@ [ "$#" -ne 1 ] && usage -SESSION="$1"; shift +LOGIC="$1"; shift -## existing image +## main -EXISTING=false -if [ "$CHECK_EXISTING" = true ]; then - declare -a ISABELLE_PATHS=() - splitarray ":" "$ISABELLE_PATH"; ISABELLE_PATHS=("${SPLITARRAY[@]}") +[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; } - for DIR in "${ISABELLE_PATHS[@]}" - do - FILE="$DIR/$ML_IDENTIFIER/$SESSION" - [ -f "$FILE" ] && EXISTING=true - done -fi - +"$ISABELLE_TOOL" java isabelle.Build_Dialog \ + "$LOGIC_OPTION" "$SYSTEM_MODE" "$LOGIC" "${INCLUDE_DIRS[@]}" -## 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 e83ab94e3e6e -r bf01be7d1a44 src/Doc/System/Interfaces.thy --- a/src/Doc/System/Interfaces.thy Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Doc/System/Interfaces.thy Thu Dec 06 23:07:10 2012 +0100 @@ -20,6 +20,8 @@ -j OPTION add jEdit runtime option (default JEDIT_OPTIONS) -l NAME logic image name (default ISABELLE_LOGIC) -m MODE add print mode for output + -n no build dialog for session image on startup + -s system build mode for session image Start jEdit with Isabelle plugin setup and opens theory FILES (default Scratch.thy). @@ -30,6 +32,11 @@ directories may be included via option @{verbatim "-d"} to augment that name space (see also \secref{sec:tool-build}). + By default, the specified image is checked and built on demand, see + also @{tool build_dialog}. The @{verbatim "-s"} determines where to + store the result session image (see also \secref{sec:tool-build}). + The @{verbatim "-n"} option bypasses the session build dialog. + The @{verbatim "-m"} option specifies additional print modes. The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass @@ -43,7 +50,8 @@ jedit_build} component.\footnote{\url{http://isabelle.in.tum.de/components}} Note that official Isabelle releases already include a version of - Isabelle/jEdit that is built properly. *} + Isabelle/jEdit that is built properly. +*} section {* Proof General / Emacs *} diff -r e83ab94e3e6e -r bf01be7d1a44 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Doc/System/Sessions.thy Thu Dec 06 23:07:10 2012 +0100 @@ -334,4 +334,29 @@ \end{ttbox} *} + +section {* Build dialog *} + +text {* The @{tool_def build_dialog} provides a simple GUI wrapper to + the tool Isabelle @{tool build} tool. This enables user interfaces + like Isabelle/jEdit \secref{sec:tool-jedit} to provide read-made + logic image on startup. Its command-line usage is: +\begin{ttbox} +Usage: isabelle build_dialog [OPTIONS] LOGIC + + Options are: + -L OPTION default logic via system option + -d DIR include session directory + -s system build mode: produce output in ISABELLE_HOME + + Build Isabelle session image LOGIC via GUI dialog. +\end{ttbox} + + \medskip Option @{verbatim "-L"} specifies a system option name as + fall-back, if the specified @{text "LOGIC"} name is empty. + + \medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same + meaning as for the command-line @{tool build} tool itself. +*} + end diff -r e83ab94e3e6e -r bf01be7d1a44 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 06 17:48:04 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Dec 06 23:07:10 2012 +0100 @@ -728,7 +728,7 @@ in "\n\nStructured proof " ^ (commas msg |> not (null msg) ? enclose "(" ")") - ^ ":\n" ^ Markup.markup Markup.sendback isar_text + ^ ":\n" ^ Sendback.markup isar_text end end val isar_proof = diff -r e83ab94e3e6e -r bf01be7d1a44 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Pure/System/build.scala Thu Dec 06 23:07:10 2012 +0100 @@ -399,7 +399,7 @@ def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content = { - val options = Options.init + 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) @@ -550,6 +550,7 @@ def build( progress: Build.Progress, + options: Options, requirements: Boolean = false, all_sessions: Boolean = false, build_heap: Boolean = false, @@ -559,12 +560,10 @@ max_jobs: Int = 1, list_files: Boolean = false, no_build: Boolean = false, - build_options: List[String] = Nil, system_mode: Boolean = false, verbose: Boolean = false, sessions: List[String] = Nil): Int = { - val options = (Options.init() /: build_options)(_ + _) val full_tree = find_sessions(options, more_dirs) val (selected, selected_tree) = full_tree.selection(requirements, all_sessions, session_groups, sessions) @@ -735,11 +734,12 @@ Properties.Value.Boolean(system_mode) :: Properties.Value.Boolean(verbose) :: Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) => + val options = (Options.init() /: build_options)(_ + _) val dirs = select_dirs.map(d => (true, Path.explode(d))) ::: include_dirs.map(d => (false, Path.explode(d))) - build(Build.Console_Progress, requirements, all_sessions, build_heap, clean_build, - dirs, session_groups, max_jobs, list_files, no_build, build_options, system_mode, + build(Build.Console_Progress, options, requirements, all_sessions, build_heap, + clean_build, dirs, session_groups, max_jobs, list_files, no_build, system_mode, verbose, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) } diff -r e83ab94e3e6e -r bf01be7d1a44 src/Pure/System/build_dialog.scala --- a/src/Pure/System/build_dialog.scala Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Pure/System/build_dialog.scala Thu Dec 06 23:07:10 2012 +0100 @@ -14,22 +14,38 @@ import scala.swing.event.ButtonClicked -object Build_Dialog extends SwingApplication +object Build_Dialog { - def startup(args: Array[String]) = + def main(args: Array[String]) = { - Platform.init_laf() - try { args.toList match { case + logic_option :: 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 + logic :: + include_dirs => + val more_dirs = include_dirs.map(s => ((false, Path.explode(s)))) + + val options = Options.init() + val session = + Isabelle_System.default_logic(logic, + if (logic_option != "") options.string(logic_option) else "") + + if (Build.build(Build.Ignore_Progress, options, no_build = true, + more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0) + else + Swing_Thread.later { + Platform.init_laf() + + val top = build_dialog(options, system_mode, more_dirs, session) + top.pack() + + val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint() + top.location = new Point(point.x - top.size.width / 2, point.y - top.size.height / 2) + + top.visible = true + } case _ => error("Bad arguments:\n" + cat_lines(args)) } } @@ -43,8 +59,9 @@ def build_dialog( + options: Options, system_mode: Boolean, - include_dirs: List[Path], + more_dirs: List[(Boolean, Path)], session: String): MainFrame = new MainFrame { /* GUI state */ @@ -104,7 +121,7 @@ val (out, rc) = try { ("", - Build.build(progress, build_heap = true, + Build.build(progress, options, build_heap = true, more_dirs = more_dirs, system_mode = system_mode, sessions = List(session))) } catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } diff -r e83ab94e3e6e -r bf01be7d1a44 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Pure/System/isabelle_system.scala Thu Dec 06 23:07:10 2012 +0100 @@ -273,7 +273,7 @@ Path.split(getenv_strict("ISABELLE_COMPONENTS")) - /* find logics */ + /* logic images */ def find_logics_dirs(): List[Path] = { @@ -287,6 +287,14 @@ files = dir.file.listFiles() if files != null file <- files.toList if file.isFile } yield file.getName).sorted + def default_logic(args: String*): String = + { + args.find(_ != "") match { + case Some(logic) => logic + case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC") + } + } + /* fonts */ diff -r e83ab94e3e6e -r bf01be7d1a44 src/Tools/jEdit/README.html --- a/src/Tools/jEdit/README.html Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Tools/jEdit/README.html Thu Dec 06 23:07:10 2012 +0100 @@ -15,7 +15,7 @@

PIDE

- PIDE is a novel framework for sophisticated Prover IDEs, + PIDE is a framework for sophisticated Prover IDEs, based on Isabelle/Scala technology that is integrated with Isabelle. It is built around a concept of asynchronous document processing, which is supported @@ -23,7 +23,7 @@

- Isabelle/jEdit is an example application within the PIDE + Isabelle/jEdit is the main example application within the PIDE framework — it illustrates many of the ideas in a realistic manner, ready to be used right now in Isabelle applications.

@@ -160,9 +160,6 @@

Limitations and workarounds

diff -r e83ab94e3e6e -r bf01be7d1a44 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Tools/jEdit/etc/options Thu Dec 06 23:07:10 2012 +0100 @@ -3,9 +3,6 @@ option jedit_logic : string = "" -- "default logic session" -option jedit_auto_start : bool = true - -- "auto-start prover session on editor startup" - option jedit_font_scale : real = 1.0 -- "scale factor of add-on panels wrt. main text area" diff -r e83ab94e3e6e -r bf01be7d1a44 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Dec 06 23:07:10 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 session name (default ISABELLE_LOGIC=$ISABELLE_LOGIC)" + echo " -l NAME logic session name" echo " -m MODE add print mode for output" + echo " -n no build dialog for session image on startup" echo " -s system build mode for session image" echo echo "Start jEdit with Isabelle plugin setup and opens theory FILES" @@ -99,13 +100,14 @@ BUILD_ONLY=false BUILD_JARS="jars" JEDIT_SESSION_DIRS="" -JEDIT_LOGIC="$ISABELLE_LOGIC" +JEDIT_LOGIC="" JEDIT_PRINT_MODE="" +NO_BUILD="false" function getoptions() { OPTIND=1 - while getopts "J:bd:fj:l:m:s" OPT + while getopts "J:bd:fj:l:m:ns" OPT do case "$OPT" in J) @@ -139,6 +141,9 @@ JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG" fi ;; + n) + NO_BUILD="true" + ;; s) BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-s" ;; @@ -313,9 +318,11 @@ # build logic -"$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -C "$JEDIT_LOGIC" -RC="$?" -[ "$RC" = 0 ] || exit "$RC" +if [ "$NO_BUILD" = false ]; then + "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC" + RC="$?" + [ "$RC" = 0 ] || exit "$RC" +fi # main diff -r e83ab94e3e6e -r bf01be7d1a44 src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Thu Dec 06 23:07:10 2012 +0100 @@ -15,26 +15,24 @@ object Isabelle_Logic { - private def default_logic(): String = - { - val logic = Isabelle_System.getenv("JEDIT_LOGIC") - if (logic != "") logic - else Isabelle_System.getenv_strict("ISABELLE_LOGIC") - } + private val option_name = "jedit_logic" + + private def jedit_logic(): String = + Isabelle_System.default_logic( + Isabelle_System.getenv("JEDIT_LOGIC"), + PIDE.options.string(option_name)) private class Logic_Entry(val name: String, val description: String) { override def toString = description } - private val option_name = "jedit_logic" - def logic_selector(autosave: Boolean): Option_Component = { Swing_Thread.require() val entries = - new Logic_Entry("", "default (" + default_logic() + ")") :: + new Logic_Entry("", "default (" + jedit_logic() + ")") :: Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name)) val component = new ComboBox(entries) with Option_Component { @@ -63,12 +61,7 @@ def session_args(): List[String] = { val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _) - val logic = - PIDE.options.string(option_name) match { - case "" => default_logic() - case logic => logic - } - modes ::: List(logic) + modes ::: List(jedit_logic()) } def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) diff -r e83ab94e3e6e -r bf01be7d1a44 src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_options.scala Thu Dec 06 23:07:10 2012 +0100 @@ -41,7 +41,7 @@ { // FIXME avoid hard-wired stuff private val relevant_options = - Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_text_overview_limit", + Set("jedit_logic", "jedit_font_scale", "jedit_text_overview_limit", "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin", "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics", "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit", diff -r e83ab94e3e6e -r bf01be7d1a44 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Dec 06 23:07:10 2012 +0100 @@ -29,12 +29,10 @@ /* component state -- owned by Swing thread */ private var zoom_factor = 100 - private var show_tracing = false private var do_update = true private var current_snapshot = Document.State.init.snapshot() private var current_state = Command.empty.init_state private var current_output: List[XML.Tree] = Nil - private var current_tracing = 0 /* pretty text area */ @@ -71,28 +69,17 @@ case None => (current_snapshot, current_state) } - val (new_output, new_tracing) = + val new_output = if (!restriction.isDefined || restriction.get.contains(new_state.command)) - { - val new_output = - new_state.results.iterator.map(_._2) - .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList - val new_tracing = - new_state.results.iterator.map(_._2).filter(Protocol.is_tracing(_)).length - (new_output, new_tracing) - } - else (current_output, current_tracing) + new_state.results.iterator.map(_._2).toList + else current_output if (new_output != current_output) pretty_text_area.update(new_snapshot, Pretty.separate(new_output)) - if (new_tracing != current_tracing) - tracing.text = tracing_text(new_tracing) - current_snapshot = new_snapshot current_state = new_state current_output = new_output - current_tracing = new_tracing } @@ -148,14 +135,6 @@ private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) zoom.tooltip = "Zoom factor for basic font size" - private def tracing_text(n: Int): String = "Tracing (" + n.toString + ")" - private val tracing = new CheckBox(tracing_text(current_tracing)) { - reactions += { - case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) } - } - tracing.selected = show_tracing - tracing.tooltip = "Indicate output of tracing messages" - private val auto_update = new CheckBox("Auto update") { reactions += { case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) } @@ -176,7 +155,6 @@ } detach.tooltip = "Detach window with static copy of current output" - private val controls = - new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update, detach) + private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, auto_update, update, detach) add(controls.peer, BorderLayout.NORTH) } diff -r e83ab94e3e6e -r bf01be7d1a44 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Dec 06 17:48:04 2012 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Thu Dec 06 23:07:10 2012 +0100 @@ -232,8 +232,7 @@ if (PIDE.startup_failure.isEmpty) { message match { case msg: EditorStarted => - if (PIDE.options.bool("jedit_auto_start")) - PIDE.session.start(Isabelle_Logic.session_args()) + PIDE.session.start(Isabelle_Logic.session_args()) case msg: BufferUpdate if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>