--- 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.
--- 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
-
--- 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 *}
--- 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
--- 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 =
--- 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))
}
--- 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) }
--- 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 */
--- 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 @@
<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
<p>
- <b>PIDE</b> is a novel framework for sophisticated Prover IDEs,
+ <b>PIDE</b> is a framework for sophisticated Prover IDEs,
based on Isabelle/Scala technology that is integrated with Isabelle.
It is built around a concept of
<em>asynchronous document processing</em>, which is supported
@@ -23,7 +23,7 @@
</p>
<p>
- <b>Isabelle/jEdit</b> is an example application within the PIDE
+ <b>Isabelle/jEdit</b> 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.
</p>
@@ -160,9 +160,6 @@
<h2>Limitations and workarounds</h2>
<ul>
- <li>No way to start/stop prover or switch to a different logic.<br/>
- <em>Workaround:</em> Change options and restart editor.</li>
-
<li>Odd behavior of some diagnostic commands, notably those starting
external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
<em>Workaround:</em> Avoid such commands.</li>
@@ -179,8 +176,6 @@
<li>No support for non-local markup, e.g. commands reporting on
previous commands (proof end on proof head), or markup produced by
loading external files.</li>
-
- <li>Lack of a few conveniences known from Proof General.</li>
</ul>
--- 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"
--- 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
--- 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"))
--- 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",
--- 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)
}
--- 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 =>