1.1 --- a/.hgtags Mon Nov 11 18:25:13 2013 +0100
1.2 +++ b/.hgtags Mon Nov 11 18:37:56 2013 +0100
1.3 @@ -26,3 +26,4 @@
1.4 76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1
1.5 21c42b095c841d1a7508c143d6b6e98d95dbfa69 Isabelle2012
1.6 d90218288d517942cfbc80a6b2654ecb22735e5c Isabelle2013
1.7 +9c1f2136532626c7cb5fae14a2aeac53be3aeb67 Isabelle2013-1
2.1 --- a/Admin/Linux/Isabelle Mon Nov 11 18:25:13 2013 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,30 +0,0 @@
2.4 -#!/usr/bin/env bash
2.5 -#
2.6 -# Author: Makarius
2.7 -#
2.8 -# Main Isabelle application wrapper.
2.9 -
2.10 -# dereference executable
2.11 -if [ -L "$0" ]; then
2.12 - TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
2.13 - exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
2.14 -fi
2.15 -
2.16 -
2.17 -# minimal Isabelle environment
2.18 -
2.19 -ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
2.20 -source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
2.21 -
2.22 -
2.23 -# main
2.24 -
2.25 -#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
2.26 -unset XMODIFIERS
2.27 -
2.28 -exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bin/java" \
2.29 - "-Disabelle.home=$ISABELLE_HOME" \
2.30 - {JAVA_ARGS} \
2.31 - -classpath "{CLASSPATH}" \
2.32 - isabelle.Main "$@"
2.33 -
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/Admin/Linux/Isabelle.c Mon Nov 11 18:37:56 2013 +0100
3.3 @@ -0,0 +1,41 @@
3.4 +/* Author: Makarius
3.5 +
3.6 +Main Isabelle application executable.
3.7 +*/
3.8 +
3.9 +#include <stdlib.h>
3.10 +#include <stdio.h>
3.11 +#include <string.h>
3.12 +#include <sys/types.h>
3.13 +#include <unistd.h>
3.14 +
3.15 +
3.16 +static void fail(const char *msg)
3.17 +{
3.18 + fprintf(stderr, "%s\n", msg);
3.19 + exit(2);
3.20 +}
3.21 +
3.22 +
3.23 +int main(int argc, char *argv[])
3.24 +{
3.25 + char **cmd_line = NULL;
3.26 + int i = 0;
3.27 +
3.28 + cmd_line = malloc(sizeof(char *) * (argc + 1));
3.29 + if (cmd_line == NULL) fail("Failed to allocate command line");
3.30 +
3.31 + cmd_line[0] = malloc(strlen(argv[0]) + 5);
3.32 + if (cmd_line[0] == NULL) fail("Failed to allocate command line");
3.33 +
3.34 + strcpy(cmd_line[0], argv[0]);
3.35 + strcat(cmd_line[0], ".run");
3.36 +
3.37 + for (i = 1; i < argc; i++) cmd_line[i] = argv[i];
3.38 +
3.39 + cmd_line[argc] = NULL;
3.40 +
3.41 + execvp(cmd_line[0], cmd_line);
3.42 + fail("Failed to execute application script");
3.43 +}
3.44 +
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/Admin/Linux/Isabelle.run Mon Nov 11 18:37:56 2013 +0100
4.3 @@ -0,0 +1,30 @@
4.4 +#!/usr/bin/env bash
4.5 +#
4.6 +# Author: Makarius
4.7 +#
4.8 +# Main Isabelle application script.
4.9 +
4.10 +# dereference executable
4.11 +if [ -L "$0" ]; then
4.12 + TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
4.13 + exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
4.14 +fi
4.15 +
4.16 +
4.17 +# minimal Isabelle environment
4.18 +
4.19 +ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
4.20 +source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
4.21 +
4.22 +
4.23 +# main
4.24 +
4.25 +#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
4.26 +unset XMODIFIERS
4.27 +
4.28 +exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bin/java" \
4.29 + "-Disabelle.home=$ISABELLE_HOME" \
4.30 + {JAVA_ARGS} \
4.31 + -classpath "{CLASSPATH}" \
4.32 + isabelle.Main "$@"
4.33 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/Admin/Linux/build Mon Nov 11 18:37:56 2013 +0100
5.3 @@ -0,0 +1,4 @@
5.4 +#!/usr/bin/env bash
5.5 +
5.6 +cc -static -m32 Isabelle.c -o Isabelle
5.7 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/Admin/components/bundled-linux Mon Nov 11 18:37:56 2013 +0100
6.3 @@ -0,0 +1,2 @@
6.4 +#additional components to be bundled for release
6.5 +linux_app-20131007
7.1 --- a/Admin/components/components.sha1 Mon Nov 11 18:25:13 2013 +0100
7.2 +++ b/Admin/components/components.sha1 Mon Nov 11 18:37:56 2013 +0100
7.3 @@ -38,16 +38,19 @@
7.4 87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz
7.5 c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz
7.6 65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz
7.7 +30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz
7.8 0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
7.9 8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
7.10 6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
7.11 5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
7.12 +377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
7.13 0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
7.14 1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
7.15 a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7.16 7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
7.17 b3d776e6744f0cd2773d467bc2cfe1de3d1ca2fd polyml-5.5.0-3.tar.gz
7.18 1812e9fa6d163f63edb93e37d1217640a166cf3e polyml-5.5.0.tar.gz
7.19 +36f5b8224f484721749682a3655c796a55a2718d polyml-5.5.1-1.tar.gz
7.20 36f78f27291a9ceb13bf1120b62a45625afd44a6 polyml-5.5.1.tar.gz
7.21 8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
7.22 847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
8.1 --- a/Admin/components/main Mon Nov 11 18:25:13 2013 +0100
8.2 +++ b/Admin/components/main Mon Nov 11 18:37:56 2013 +0100
8.3 @@ -4,10 +4,10 @@
8.4 exec_process-1.0.3
8.5 Haskabelle-2013
8.6 jdk-7u40
8.7 -jedit_build-20130926
8.8 +jedit_build-20131106
8.9 jfreechart-1.0.14-1
8.10 kodkodi-1.5.2
8.11 -polyml-5.5.1
8.12 +polyml-5.5.1-1
8.13 scala-2.10.3
8.14 spass-3.8ds
8.15 z3-3.2
9.1 --- a/Admin/lib/Tools/makedist_bundle Mon Nov 11 18:25:13 2013 +0100
9.2 +++ b/Admin/lib/Tools/makedist_bundle Mon Nov 11 18:37:56 2013 +0100
9.3 @@ -160,10 +160,13 @@
9.4 LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY"
9.5 fi
9.6 done
9.7 - cat "$ISABELLE_HOME/Admin/Linux/Isabelle" | \
9.8 - perl -p > "$ISABELLE_TARGET/$ISABELLE_NAME" \
9.9 + cat "$ISABELLE_HOME/Admin/Linux/Isabelle.run" | \
9.10 + perl -p > "$ISABELLE_TARGET/${ISABELLE_NAME}.run" \
9.11 -e "s,{JAVA_ARGS},$JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS,g; s,{CLASSPATH},$LINUX_CLASSPATH,;"
9.12 - chmod +x "$ISABELLE_TARGET/$ISABELLE_NAME"
9.13 + chmod +x "$ISABELLE_TARGET/${ISABELLE_NAME}.run"
9.14 +
9.15 + mv "$ISABELLE_TARGET/contrib/linux_app" "$TMP/."
9.16 + cp "$TMP/linux_app/Isabelle" "$ISABELLE_TARGET/$ISABELLE_NAME"
9.17 ;;
9.18 macos)
9.19 purge_contrib '-name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
10.1 --- a/CONTRIBUTORS Mon Nov 11 18:25:13 2013 +0100
10.2 +++ b/CONTRIBUTORS Mon Nov 11 18:37:56 2013 +0100
10.3 @@ -10,6 +10,12 @@
10.4 Contributions to Isabelle2013-1
10.5 -------------------------------
10.6
10.7 +* September 2013: Lars Noschinski, TUM
10.8 + Conversion between function definitions as list of equations and
10.9 + case expressions in HOL.
10.10 + New library Simps_Case_Conv with commands case_of_simps,
10.11 + simps_of_case.
10.12 +
10.13 * September 2013: Nik Sultana, University of Cambridge
10.14 Improvements to HOL/TPTP parser and import facilities.
10.15
11.1 --- a/NEWS Mon Nov 11 18:25:13 2013 +0100
11.2 +++ b/NEWS Mon Nov 11 18:37:56 2013 +0100
11.3 @@ -125,7 +125,10 @@
11.4 normal editing and checking process.
11.5
11.6 * Dockable window "Timing" provides an overview of relevant command
11.7 -timing information.
11.8 +timing information, depending on option jedit_timing_threshold. The
11.9 +same timing information is shown in the extended tooltip of the
11.10 +command keyword, when hovering the mouse over it while the CONTROL or
11.11 +COMMAND modifier is pressed.
11.12
11.13 * Improved dockable window "Theories": Continuous checking of proof
11.14 document (visible and required parts) may be controlled explicitly,
11.15 @@ -133,14 +136,22 @@
11.16 be marked explicitly as required and checked in full, using check box
11.17 or shortcut "C+e SPACE".
11.18
11.19 +* Improved completion mechanism, which is now managed by the
11.20 +Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle
11.21 +symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
11.22 +
11.23 +* Standard jEdit keyboard shortcut C+b complete-word is remapped to
11.24 +isabelle.complete for explicit completion in Isabelle sources.
11.25 +INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts
11.26 +to resolve conflict.
11.27 +
11.28 +* Improved support of various "minor modes" for Isabelle NEWS,
11.29 +options, session ROOT etc., with completion and SideKick tree view.
11.30 +
11.31 * Strictly monotonic document update, without premature cancellation of
11.32 running transactions that are still needed: avoid reset/restart of
11.33 such command executions while editing.
11.34
11.35 -* Improved completion mechanism, which is now managed by the
11.36 -Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle
11.37 -symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
11.38 -
11.39 * Support for asynchronous print functions, as overlay to existing
11.40 document content.
11.41
11.42 @@ -148,12 +159,13 @@
11.43 toplevel theorem statements.
11.44
11.45 * Action isabelle.reset-font-size resets main text area font size
11.46 -according to Isabelle/Scala plugin option "jedit_font_reset_size"
11.47 -(cf. keyboard shortcut C+0).
11.48 +according to Isabelle/Scala plugin option "jedit_font_reset_size" (see
11.49 +also "Plugin Options / Isabelle / General"). It can be bound to some
11.50 +keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0).
11.51
11.52 * File specifications in jEdit (e.g. file browser) may refer to
11.53 -$ISABELLE_HOME on all platforms. Discontinued obsolete
11.54 -$ISABELLE_HOME_WINDOWS variable.
11.55 +$ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms. Discontinued
11.56 +obsolete $ISABELLE_HOME_WINDOWS variable.
11.57
11.58 * Improved support for Linux look-and-feel "GTK+", see also "Utilities
11.59 / Global Options / Appearance".
11.60 @@ -250,7 +262,7 @@
11.61
11.62 * Lifting:
11.63 - parametrized correspondence relations are now supported:
11.64 - + parametricity theorems for the raw term can be specified in
11.65 + + parametricity theorems for the raw term can be specified in
11.66 the command lift_definition, which allow us to generate stronger
11.67 transfer rules
11.68 + setup_lifting generates stronger transfer rules if parametric
11.69 @@ -264,15 +276,15 @@
11.70 - ===> and --> are now local. The symbols can be introduced
11.71 by interpreting the locale lifting_syntax (typically in an
11.72 anonymous context)
11.73 - - Lifting/Transfer relevant parts of Library/Quotient_* are now in
11.74 + - Lifting/Transfer relevant parts of Library/Quotient_* are now in
11.75 Main. Potential INCOMPATIBILITY
11.76 - new commands for restoring and deleting Lifting/Transfer context:
11.77 lifting_forget, lifting_update
11.78 - - the command print_quotmaps was renamed to print_quot_maps.
11.79 + - the command print_quotmaps was renamed to print_quot_maps.
11.80 INCOMPATIBILITY
11.81
11.82 * Transfer:
11.83 - - better support for domains in Transfer: replace Domainp T
11.84 + - better support for domains in Transfer: replace Domainp T
11.85 by the actual invariant in a transferred goal
11.86 - transfer rules can have as assumptions other transfer rules
11.87 - Experimental support for transferring from the raw level to the
12.1 --- a/etc/settings Mon Nov 11 18:25:13 2013 +0100
12.2 +++ b/etc/settings Mon Nov 11 18:37:56 2013 +0100
12.3 @@ -106,7 +106,7 @@
12.4 PDF_VIEWER="xdg-open"
12.5 ;;
12.6 macos)
12.7 - PDF_VIEWER="open -W -n -a Safari"
12.8 + PDF_VIEWER="open -W -n -F"
12.9 ;;
12.10 windows)
12.11 PDF_VIEWER="cygstart"
13.1 --- a/src/Doc/IsarRef/Document_Preparation.thy Mon Nov 11 18:25:13 2013 +0100
13.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy Mon Nov 11 18:37:56 2013 +0100
13.3 @@ -5,17 +5,17 @@
13.4 chapter {* Document preparation \label{ch:document-prep} *}
13.5
13.6 text {* Isabelle/Isar provides a simple document preparation system
13.7 - based on regular {PDF-\LaTeX} technology, with support for
13.8 - hyper-links and bookmarks within that format. Thus the results are
13.9 - well suited for WWW browsing and as printed copies.
13.10 + based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks
13.11 + within that format. This allows to produce papers, books, theses
13.12 + etc.\ from Isabelle theory sources.
13.13
13.14 {\LaTeX} output is generated while processing a \emph{session} in
13.15 batch mode, as explained in the \emph{The Isabelle System Manual}
13.16 \cite{isabelle-sys}. The main Isabelle tools to get started with
13.17 - document prepation are @{tool_ref mkroot} and @{tool_ref build}.
13.18 + document preparation are @{tool_ref mkroot} and @{tool_ref build}.
13.19
13.20 - The Isabelle/HOL tutorial \cite{isabelle-hol-book} also covers
13.21 - theory presentation to some extent. *}
13.22 + The classic Isabelle/HOL tutorial \cite{isabelle-hol-book} also
13.23 + explains some aspects of theory presentation. *}
13.24
13.25
13.26 section {* Markup commands \label{sec:markup} *}
13.27 @@ -302,8 +302,8 @@
13.28 subsection {* General options *}
13.29
13.30 text {* The following options are available to tune the printed output
13.31 - of antiquotations. Note that many of these coincide with global ML
13.32 - flags of the same names.
13.33 + of antiquotations. Note that many of these coincide with system and
13.34 + configuration options of the same names.
13.35
13.36 \begin{description}
13.37
14.1 --- a/src/Doc/IsarRef/HOL_Specific.thy Mon Nov 11 18:25:13 2013 +0100
14.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy Mon Nov 11 18:37:56 2013 +0100
14.3 @@ -1259,17 +1259,18 @@
14.4 \end{matharray}
14.5
14.6 The quotient package defines a new quotient type given a raw type
14.7 - and a partial equivalence relation. It also includes automation for
14.8 - transporting definitions and theorems. It can automatically produce
14.9 - definitions and theorems on the quotient type, given the
14.10 - corresponding constants and facts on the raw type.
14.11 + and a partial equivalence relation. The package also historically
14.12 + includes automation for transporting definitions and theorems.
14.13 + But most of this automation was superseded by the Lifting and Transfer
14.14 + packages. The user should consider using these two new packages for
14.15 + lifting definitions and transporting theorems.
14.16
14.17 @{rail "
14.18 @@{command (HOL) quotient_type} (spec);
14.19
14.20 spec: @{syntax typespec} @{syntax mixfix}? '=' \\
14.21 @{syntax type} '/' ('partial' ':')? @{syntax term} \\
14.22 - (@'morphisms' @{syntax name} @{syntax name})?;
14.23 + (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?;
14.24 "}
14.25
14.26 @{rail "
14.27 @@ -1289,9 +1290,9 @@
14.28
14.29 \begin{description}
14.30
14.31 - \item @{command (HOL) "quotient_type"} defines quotient types. The
14.32 + \item @{command (HOL) "quotient_type"} defines a new quotient type @{text \<tau>}. The
14.33 injection from a quotient type to a raw type is called @{text
14.34 - rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)
14.35 + rep_\<tau>}, its inverse @{text abs_\<tau>} unless explicit @{keyword (HOL)
14.36 "morphisms"} specification provides alternative names. @{command
14.37 (HOL) "quotient_type"} requires the user to prove that the relation
14.38 is an equivalence relation (predicate @{text equivp}), unless the
14.39 @@ -1300,6 +1301,22 @@
14.40 partial} is weaker in the sense that less things can be proved
14.41 automatically.
14.42
14.43 + The command internally proves a Quotient theorem and sets up the Lifting
14.44 + package by the command @{command (HOL) setup_lifting}. Thus the Lifting
14.45 + and Transfer packages can be used also with quotient types defined by
14.46 + @{command (HOL) "quotient_type"} without any extra set-up. The parametricity
14.47 + theorem for the equivalence relation R can be provided as an extra argument
14.48 + of the command and is passed to the corresponding internal call of @{command (HOL) setup_lifting}.
14.49 + This theorem allows the Lifting package to generate a stronger transfer rule for equality.
14.50 +
14.51 + \end{description}
14.52 +
14.53 + The most of the rest of the package was superseded by the Lifting and Transfer
14.54 + packages. The user should consider using these two new packages for
14.55 + lifting definitions and transporting theorems.
14.56 +
14.57 + \begin{description}
14.58 +
14.59 \item @{command (HOL) "quotient_definition"} defines a constant on
14.60 the quotient type.
14.61
14.62 @@ -1497,8 +1514,12 @@
14.63 @{method_def (HOL) "transfer"} & : & @{text method} \\
14.64 @{method_def (HOL) "transfer'"} & : & @{text method} \\
14.65 @{method_def (HOL) "transfer_prover"} & : & @{text method} \\
14.66 + @{attribute_def (HOL) "Transfer.transferred"} & : & @{text attribute} \\
14.67 + @{attribute_def (HOL) "untransferred"} & : & @{text attribute} \\
14.68 @{attribute_def (HOL) "transfer_rule"} & : & @{text attribute} \\
14.69 + @{attribute_def (HOL) "transfer_domain_rule"} & : & @{text attribute} \\
14.70 @{attribute_def (HOL) "relator_eq"} & : & @{text attribute} \\
14.71 + @{attribute_def (HOL) "relator_domain"} & : & @{text attribute} \\
14.72 \end{matharray}
14.73
14.74 \begin{description}
14.75 @@ -1524,6 +1545,16 @@
14.76 rules. It should be applied after unfolding the constant
14.77 definitions.
14.78
14.79 + \item @{attribute (HOL) "untransferred"} proves the same equivalent theorem
14.80 + as @{method (HOL) "transfer"} internally does.
14.81 +
14.82 + \item @{attribute (HOL) Transfer.transferred} works in the opposite
14.83 + direction than @{method (HOL) "transfer'"}. E.g., given the transfer
14.84 + relation @{text "ZN x n \<equiv> (x = int n)"}, corresponding transfer rules and the theorem
14.85 + @{text "\<forall>x::int \<in> {0..}. x < x + 1"}, the attribute would prove
14.86 + @{text "\<forall>n::nat. n < n + 1"}. The attribute is still in experimental
14.87 + phase of development.
14.88 +
14.89 \item @{attribute (HOL) "transfer_rule"} attribute maintains a
14.90 collection of transfer rules, which relate constants at two
14.91 different types. Typical transfer rules may relate different type
14.92 @@ -1540,83 +1571,140 @@
14.93 @{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
14.94 @{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (prod_rel A B)"}
14.95
14.96 + \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
14.97 + of rules, which specify a domain of a transfer relation by a predicate.
14.98 + E.g., given the transfer relation @{text "ZN x n \<equiv> (x = int n)"},
14.99 + one can register the following transfer domain rule:
14.100 + @{text "Domainp ZN = (\<lambda>x. x \<ge> 0)"}. The rules allow the package to produce
14.101 + more readable transferred goals, e.g., when quantifiers are transferred.
14.102 +
14.103 \item @{attribute (HOL) relator_eq} attribute collects identity laws
14.104 for relators of various type constructors, e.g. @{text "list_all2
14.105 (op =) = (op =)"}. The @{method (HOL) transfer} method uses these
14.106 lemmas to infer transfer rules for non-polymorphic constants on
14.107 the fly.
14.108
14.109 + \item @{attribute_def (HOL) "relator_domain"} attribute collects rules
14.110 + describing domains of relators by predicators. E.g., @{text "Domainp A = P \<Longrightarrow>
14.111 + Domainp (list_all2 A) = (list_all P)"}. This allows the package to lift transfer
14.112 + domain rules through type constructors.
14.113 +
14.114 \end{description}
14.115
14.116 + Theoretical background can be found in \cite{Huffman-Kuncar:2013:lifting_transfer}.
14.117 *}
14.118
14.119
14.120 section {* Lifting package *}
14.121
14.122 text {*
14.123 + The Lifting package allows users to lift terms of the raw type to the abstract type, which is
14.124 + a necessary step in building a library for an abstract type. Lifting defines a new constant
14.125 + by combining coercion functions (Abs and Rep) with the raw term. It also proves an appropriate
14.126 + transfer rule for the Transfer package and, if possible, an equation for the code generator.
14.127 +
14.128 + The Lifting package provides two main commands: @{command (HOL) "setup_lifting"} for initializing
14.129 + the package to work with a new type, and @{command (HOL) "lift_definition"} for lifting constants.
14.130 + The Lifting package works with all four kinds of type abstraction: type copies, subtypes,
14.131 + total quotients and partial quotients.
14.132 +
14.133 + Theoretical background can be found in \cite{Huffman-Kuncar:2013:lifting_transfer}.
14.134 +
14.135 \begin{matharray}{rcl}
14.136 @{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
14.137 @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
14.138 + @{command_def (HOL) "lifting_forget"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
14.139 + @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
14.140 @{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
14.141 @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
14.142 @{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
14.143 @{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
14.144 @{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\
14.145 - @{attribute_def (HOL) "quot_del"} & : & @{text attribute}
14.146 + @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
14.147 + @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
14.148 + @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
14.149 + @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\
14.150 \end{matharray}
14.151
14.152 @{rail "
14.153 @@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \\
14.154 - @{syntax thmref} @{syntax thmref}?;
14.155 + @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
14.156 "}
14.157
14.158 @{rail "
14.159 @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \\
14.160 - 'is' @{syntax term};
14.161 + 'is' @{syntax term} (@'parametric' @{syntax thmref})?;
14.162 "}
14.163
14.164 + @{rail "
14.165 + @@{command (HOL) lifting_forget} @{syntax nameref};
14.166 + "}
14.167 +
14.168 + @{rail "
14.169 + @@{command (HOL) lifting_update} @{syntax nameref};
14.170 + "}
14.171 +
14.172 + @{rail "
14.173 + @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
14.174 + "}
14.175 +
14.176 \begin{description}
14.177
14.178 \item @{command (HOL) "setup_lifting"} Sets up the Lifting package
14.179 - to work with a user-defined type. The user must provide either a
14.180 - quotient theorem @{text "Quotient R Abs Rep T"} or a
14.181 - type_definition theorem @{text "type_definition Rep Abs A"}. The
14.182 - package configures transfer rules for equality and quantifiers on
14.183 - the type, and sets up the @{command_def (HOL) "lift_definition"}
14.184 - command to work with the type. In the case of a quotient theorem,
14.185 - an optional theorem @{text "reflp R"} can be provided as a second
14.186 - argument. This allows the package to generate stronger transfer
14.187 - rules.
14.188 -
14.189 - @{command (HOL) "setup_lifting"} is called automatically if a
14.190 - quotient type is defined by the command @{command (HOL)
14.191 - "quotient_type"} from the Quotient package.
14.192 -
14.193 - If @{command (HOL) "setup_lifting"} is called with a
14.194 - type_definition theorem, the abstract type implicitly defined by
14.195 - the theorem is declared as an abstract type in the code
14.196 - generator. This allows @{command (HOL) "lift_definition"} to
14.197 - register (generated) code certificate theorems as abstract code
14.198 - equations in the code generator. The option @{text "no_code"}
14.199 - of the command @{command (HOL) "setup_lifting"} can turn off that
14.200 - behavior and causes that code certificate theorems generated by
14.201 - @{command (HOL) "lift_definition"} are not registered as abstract
14.202 - code equations.
14.203 -
14.204 - \item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"}
14.205 + to work with a user-defined type.
14.206 + The command supports two modes. The first one is a low-level mode when
14.207 + the user must provide as a first
14.208 + argument of @{command (HOL) "setup_lifting"} a
14.209 + quotient theorem @{text "Quotient R Abs Rep T"}. The
14.210 + package configures a transfer rule for equality, a domain transfer
14.211 + rules and sets up the @{command_def (HOL) "lift_definition"}
14.212 + command to work with the abstract type. An optional theorem @{text "reflp R"}, which certifies that
14.213 + the equivalence relation R is total,
14.214 + can be provided as a second argument. This allows the package to generate stronger transfer
14.215 + rules. And finally, the parametricity theorem for R can be provided as a third argument.
14.216 + This allows the package to generate a stronger transfer rule for equality.
14.217 +
14.218 + Users generally will not prove the @{text Quotient} theorem manually for
14.219 + new types, as special commands exist to automate the process.
14.220 +
14.221 + When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL) "lift_definition"}
14.222 + can be used in its
14.223 + second mode, where only the type_definition theorem @{text "type_definition Rep Abs A"}
14.224 + is used as an argument of the command. The command internally proves the corresponding
14.225 + Quotient theorem and registers it with @{command (HOL) setup_lifting} using its first mode.
14.226 +
14.227 + For quotients, the command @{command (HOL) quotient_type} can be used. The command defines
14.228 + a new quotient type and similarly to the previous case, the corresponding Quotient theorem is proved
14.229 + and registered by @{command (HOL) setup_lifting}.
14.230 +
14.231 + The command @{command (HOL) "setup_lifting"} also sets up the code generator
14.232 + for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"},
14.233 + the Lifting package proves and registers a code equation (if there is one) for the new constant.
14.234 + If the option @{text "no_code"} is specified, the Lifting package does not set up the code
14.235 + generator and as a consequence no code equations involving an abstract type are registered
14.236 + by @{command (HOL) "lift_definition"}.
14.237 +
14.238 + \item @{command (HOL) "lift_definition"} @{text "f :: \<tau>"} @{keyword (HOL) "is"} @{text t}
14.239 Defines a new function @{text f} with an abstract type @{text \<tau>}
14.240 in terms of a corresponding operation @{text t} on a
14.241 - representation type. The term @{text t} doesn't have to be
14.242 - necessarily a constant but it can be any term.
14.243 -
14.244 - Users must discharge a respectfulness proof obligation when each
14.245 - constant is defined. For a type copy, i.e. a typedef with @{text
14.246 - UNIV}, the proof is discharged automatically. The obligation is
14.247 + representation type. More formally, if @{text "t :: \<sigma>"}, then
14.248 + the command builds a term @{text "F"} as a corresponding combination of abstraction
14.249 + and representation functions such that @{text "F :: \<sigma> \<Rightarrow> \<tau>" } and
14.250 + defines @{text f} is as @{text "f \<equiv> F t"}.
14.251 + The term @{text t} does not have to be necessarily a constant but it can be any term.
14.252 +
14.253 + The command opens a proof environment and the user must discharge
14.254 + a respectfulness proof obligation. For a type copy, i.e., a typedef with @{text
14.255 + UNIV}, the obligation is discharged automatically. The proof goal is
14.256 presented in a user-friendly, readable form. A respectfulness
14.257 theorem in the standard format @{text f.rsp} and a transfer rule
14.258 - @{text f.tranfer} for the Transfer package are generated by the
14.259 + @{text f.transfer} for the Transfer package are generated by the
14.260 package.
14.261
14.262 + The user can specify a parametricity theorem for @{text t} after the keyword
14.263 + @{keyword "parametric"}, which allows the command
14.264 + to generate a parametric transfer rule for @{text f}.
14.265 +
14.266 For each constant defined through trivial quotients (type copies or
14.267 subtypes) @{text f.rep_eq} is generated. The equation is a code certificate
14.268 that defines @{text f} using the representation function.
14.269 @@ -1625,14 +1713,36 @@
14.270 for total quotients. The equation defines @{text f} using
14.271 the abstraction function.
14.272
14.273 - Integration with code_abstype: For subtypes (e.g.,
14.274 + Integration with [@{attribute code} abstract]: For subtypes (e.g.,
14.275 corresponding to a datatype invariant, such as dlist), @{command
14.276 (HOL) "lift_definition"} uses a code certificate theorem
14.277 @{text f.rep_eq} as a code equation.
14.278
14.279 - Integration with code: For total quotients, @{command
14.280 + Integration with [@{attribute code} equation]: For total quotients, @{command
14.281 (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
14.282
14.283 + \item @{command (HOL) lifting_forget} and @{command (HOL) lifting_update}
14.284 + These two commands serve for storing and deleting the set-up of
14.285 + the Lifting package and corresponding transfer rules defined by this package.
14.286 + This is useful for hiding of type construction details of an abstract type
14.287 + when the construction is finished but it still allows additions to this construction
14.288 + when this is later necessary.
14.289 +
14.290 + Whenever the Lifting package is set up with a new abstract type @{text "\<tau>"} by
14.291 + @{command_def (HOL) "lift_definition"}, the package defines a new bundle
14.292 + that is called @{text "\<tau>.lifting"}. This bundle already includes set-up for the Lifting package.
14.293 + The new transfer rules
14.294 + introduced by @{command (HOL) "lift_definition"} can be stored in the bundle by
14.295 + the command @{command (HOL) "lifting_update"} @{text "\<tau>.lifting"}.
14.296 +
14.297 + The command @{command (HOL) "lifting_forget"} @{text "\<tau>.lifting"} deletes set-up of the Lifting
14.298 + package
14.299 + for @{text \<tau>} and deletes all the transfer rules that were introduced
14.300 + by @{command (HOL) "lift_definition"} using @{text \<tau>} as an abstract type.
14.301 +
14.302 + The stored set-up in a bundle can be reintroduced by the Isar commands for including a bundle
14.303 + (@{command "include"}, @{keyword "includes"} and @{command "including"}).
14.304 +
14.305 \item @{command (HOL) "print_quot_maps"} prints stored quotient map
14.306 theorems.
14.307
14.308 @@ -1640,9 +1750,11 @@
14.309 theorems.
14.310
14.311 \item @{attribute (HOL) quot_map} registers a quotient map
14.312 - theorem. For examples see @{file
14.313 - "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
14.314 - files.
14.315 + theorem. E.g., @{text "Quotient R Abs Rep T \<Longrightarrow>
14.316 + Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"}.
14.317 + For examples see @{file
14.318 + "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
14.319 + in the same directory.
14.320
14.321 \item @{attribute (HOL) invariant_commute} registers a theorem that
14.322 shows a relationship between the constant @{text
14.323 @@ -1650,20 +1762,54 @@
14.324 and a relator. Such theorems allows the package to hide @{text
14.325 Lifting.invariant} from a user in a user-readable form of a
14.326 respectfulness theorem. For examples see @{file
14.327 - "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
14.328 - files.
14.329 + "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
14.330
14.331 \item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
14.332 - that a relator respects reflexivity and left-totality. For examples
14.333 - see @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
14.334 - The property is used in generation of abstraction function equations.
14.335 + that a relator respects reflexivity, left-totality and left_uniqueness. For examples
14.336 + see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
14.337 + in the same directory.
14.338 + The property is used in a reflexivity prover, which is used for discharging respectfulness
14.339 + theorems for type copies and also for discharging assumptions of abstraction function equations.
14.340 +
14.341 + \item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.
14.342 + E.g., @{text "A \<le> B \<Longrightarrow> list_all2 A \<le> list_all2 B"}. For examples
14.343 + see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
14.344 + or Lifting_*.thy files in the same directory.
14.345 + This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
14.346 + when a parametricity theorem for the raw term is specified.
14.347 +
14.348 + \item @{attribute (HOL) "relator_distr"} registers a property describing a distributivity
14.349 + of the relation composition and a relator. E.g.,
14.350 + @{text "list_all2 R \<circ>\<circ> list_all2 S = list_all2 (R \<circ>\<circ> S)"}.
14.351 + This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
14.352 + when a parametricity theorem for the raw term is specified.
14.353 + When this equality does not hold unconditionally (e.g., for the function type), the user can specified
14.354 + each direction separately and also register multiple theorems with different set of assumptions.
14.355 + This attribute can be used only after the monotonicity property was already registered by
14.356 + @{attribute (HOL) "relator_mono"}. For examples
14.357 + see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
14.358 + or Lifting_*.thy files in the same directory.
14.359
14.360 \item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
14.361 from the Lifting infrastructure and thus de-register the corresponding quotient.
14.362 This effectively causes that @{command (HOL) lift_definition} will not
14.363 - do any lifting for the corresponding type. It serves mainly for hiding
14.364 - of type construction details when the construction is done. See for example
14.365 - @{file "~~/src/HOL/Int.thy"}.
14.366 + do any lifting for the corresponding type. This attribute is rather used for low-level
14.367 + manipulation with set-up of the Lifting package because @{command (HOL) lifting_forget} is
14.368 + preferred for normal usage.
14.369 +
14.370 + \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def pcr_cr_eq_thm"}
14.371 + registers the Quotient theorem @{text Quotient_thm} in the Lifting infrastructure
14.372 + and thus sets up lifting for an abstract type @{text \<tau>} (that is defined by @{text Quotient_thm}).
14.373 + Optional theorems @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register
14.374 + the parametrized
14.375 + correspondence relation for @{text \<tau>}. E.g., for @{text "'a dlist"}, @{text pcr_def} is
14.376 + @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ> cr_dlist"} and @{text pcr_cr_eq_thm} is
14.377 + @{text "pcr_dlist op= = op="}.
14.378 + This attribute is rather used for low-level
14.379 + manipulation with set-up of the Lifting package because using of the bundle @{text \<tau>.lifting}
14.380 + together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is
14.381 + preferred for normal usage.
14.382 +
14.383 \end{description}
14.384 *}
14.385
15.1 --- a/src/Doc/JEdit/Base.thy Mon Nov 11 18:25:13 2013 +0100
15.2 +++ b/src/Doc/JEdit/Base.thy Mon Nov 11 18:37:56 2013 +0100
15.3 @@ -1,5 +1,5 @@
15.4 theory Base
15.5 -imports Pure
15.6 +imports Main
15.7 begin
15.8
15.9 ML_file "../antiquote_setup.ML"
16.1 --- a/src/Doc/JEdit/JEdit.thy Mon Nov 11 18:25:13 2013 +0100
16.2 +++ b/src/Doc/JEdit/JEdit.thy Mon Nov 11 18:37:56 2013 +0100
16.3 @@ -8,268 +8,1135 @@
16.4
16.5 section {* Concepts and terminology *}
16.6
16.7 -text {* FIXME
16.8 +text {* Isabelle/jEdit is a Prover IDE that integrates \emph{parallel
16.9 + proof checking} \cite{Wenzel:2009,Wenzel:2013:ITP} with
16.10 + \emph{asynchronous user interaction}
16.11 + \cite{Wenzel:2010,Wenzel:2012:UITP-EPTCS}, based on a
16.12 + document-oriented approach to \emph{continuous proof processing}
16.13 + \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system
16.14 + components are fit together in order to make this work. The main
16.15 + building blocks are as follows.
16.16
16.17 -parallel proof checking \cite{Wenzel:2009} \cite{Wenzel:2013:ITP}
16.18 + \begin{description}
16.19
16.20 -asynchronous user interaction \cite{Wenzel:2010},
16.21 -\cite{Wenzel:2012:UITP-EPTCS}
16.22 + \item [PIDE] is a general framework for Prover IDEs based on
16.23 + Isabelle/Scala. It is built around a concept of parallel and
16.24 + asynchronous document processing, which is supported natively by the
16.25 + parallel proof engine that is implemented in Isabelle/ML. The prover
16.26 + discontinues the traditional TTY-based command loop, and supports
16.27 + direct editing of formal source text with rich formal markup for GUI
16.28 + rendering.
16.29
16.30 -document-oriented proof processing and Prover IDE \cite{Wenzel:2011:CICM}
16.31 -\cite{Wenzel:2012}
16.32 + \item [Isabelle/ML] is the implementation and extension language of
16.33 + Isabelle, see also \cite{isabelle-implementation}. It is integrated
16.34 + into the logical context of Isabelle/Isar and allows to manipulate
16.35 + logical entities directly. Arbitrary add-on tools may be implemented
16.36 + for object-logics such as Isabelle/HOL.
16.37
16.38 -\begin{description}
16.39 + \item [Isabelle/Scala] is the system programming language of
16.40 + Isabelle. It extends the pure logical environment of Isabelle/ML
16.41 + towards the ``real world'' of graphical user interfaces, text
16.42 + editors, IDE frameworks, web services etc. Special infrastructure
16.43 + allows to transfer algebraic datatypes and formatted text easily
16.44 + between ML and Scala, using asynchronous protocol commands.
16.45
16.46 -\item [PIDE] is a general framework for Prover IDEs based on the
16.47 -Isabelle/Scala. It is built around a concept of \emph{asynchronous document
16.48 -processing}, which is supported natively by the \emph{parallel proof engine}
16.49 -that is implemented in Isabelle/ML.
16.50 + \item [jEdit] is a sophisticated text editor implemented in
16.51 + Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
16.52 + by plugins written in languages that work on the JVM, e.g.\
16.53 + Scala\footnote{\url{http://www.scala-lang.org/}}.
16.54
16.55 -\item [jEdit] is a sophisticated text editor \url{http://www.jedit.org}
16.56 -implemented in Java. It is easily extensible by plugins written in any
16.57 -language that works on the JVM, e.g.\ Scala.
16.58 + \item [Isabelle/jEdit] is the main example application of the PIDE
16.59 + framework and the default user-interface for Isabelle. It targets
16.60 + both beginners and experts. Technically, Isabelle/jEdit combines a
16.61 + slightly modified version of the jEdit code base with a special
16.62 + plugin for Isabelle, integrated as standalone application for the
16.63 + main operating system platforms: Linux, Windows, Mac OS X.
16.64
16.65 -\item [Isabelle/jEdit] is the main example application of the PIDE framework
16.66 -and the default user-interface for Isabelle. It is targeted at beginners and
16.67 -experts alike.
16.68 + \end{description}
16.69
16.70 -\end{description}
16.71 -*}
16.72 + The subtle differences of Isabelle/ML versus Standard ML,
16.73 + Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
16.74 + taken into account when discussing any of these PIDE building blocks
16.75 + in public forums, mailing lists, or even scientific publications.
16.76 + *}
16.77
16.78
16.79 section {* The Isabelle/jEdit Prover IDE *}
16.80
16.81 text {*
16.82 + \begin{figure}[htb]
16.83 + \begin{center}
16.84 \includegraphics[width=\textwidth]{isabelle-jedit}
16.85 + \end{center}
16.86 + \caption{The Isabelle/jEdit Prover IDE}
16.87 + \label{fig:isabelle-jedit}
16.88 + \end{figure}
16.89
16.90 - Isabelle/jEdit consists of some plugins for the well-known jEdit text
16.91 - editor \url{http://www.jedit.org}, according to the following
16.92 - principles.
16.93 + Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
16.94 + plugins for the well-known jEdit text editor
16.95 + \url{http://www.jedit.org}, according to the following principles.
16.96
16.97 \begin{itemize}
16.98
16.99 - \item The original jEdit look-and-feel is generally preserved, although
16.100 - some default properties have been changed to accommodate Isabelle (e.g.\
16.101 - the text area font).
16.102 + \item The original jEdit look-and-feel is generally preserved,
16.103 + although some default properties are changed to accommodate Isabelle
16.104 + (e.g.\ the text area font).
16.105
16.106 - \item Formal Isabelle/Isar text is checked asynchronously while editing.
16.107 - The user is in full command of the editor, and the prover refrains from
16.108 - locking portions of the buffer.
16.109 + \item Formal Isabelle/Isar text is checked asynchronously while
16.110 + editing. The user is in full command of the editor, and the prover
16.111 + refrains from locking portions of the buffer.
16.112
16.113 \item Prover feedback works via colors, boxes, squiggly underline,
16.114 - hyperlinks, popup windows, icons, clickable output, all based on semantic
16.115 - markup produced by Isabelle in the background.
16.116 + hyperlinks, popup windows, icons, clickable output --- all based on
16.117 + semantic markup produced by Isabelle in the background.
16.118
16.119 - \item Using the mouse together with the modifier key @{verbatim CONTROL}
16.120 - (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes additional
16.121 - formal content via tooltips and/or hyperlinks.
16.122 + \item Using the mouse together with the modifier key @{verbatim
16.123 + CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
16.124 + additional formal content via tooltips and/or hyperlinks.
16.125
16.126 - \item Dockable panels (e.g. \emph{Output}, \emph{Symbols}) are managed as
16.127 - independent windows by jEdit, which also allows multiple instances.
16.128 + \item Formal output (in popups etc.) may be explored recursively,
16.129 + using the same techniques as in the editor source buffer.
16.130
16.131 - \item Formal output (in popups etc.) may be explored recursively, using
16.132 - the same techniques as in the editor source buffer.
16.133 + \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
16.134 + organized by the Dockable Window Manager of jEdit, which also allows
16.135 + multiple floating instances of each window class.
16.136
16.137 - \item The prover process and source files are managed on the editor side.
16.138 - The prover operates on timeless and stateless document content via
16.139 - Isabelle/Scala.
16.140 + \item The prover process and source files are managed on the editor
16.141 + side. The prover operates on timeless and stateless document
16.142 + content as provided via Isabelle/Scala.
16.143
16.144 - \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give access
16.145 - to a selection of Isabelle/Scala options and its persistence preferences,
16.146 - usually with immediate effect on the prover back-end or editor front-end.
16.147 + \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
16.148 + access to a selection of Isabelle/Scala options and its persistent
16.149 + preferences, usually with immediate effect on the prover back-end or
16.150 + editor front-end.
16.151
16.152 \item The logic image of the prover session may be specified within
16.153 - Isabelle/jEdit, but this requires restart. The new image is provided
16.154 - automatically by the Isabelle build process.
16.155 + Isabelle/jEdit. The new image is provided automatically by the
16.156 + Isabelle build tool after restart of the application.
16.157
16.158 \end{itemize}
16.159 *}
16.160
16.161
16.162 +subsection {* Documentation *}
16.163 +
16.164 +text {* Regular jEdit documentation is accessible via its @{verbatim
16.165 + Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
16.166 + \emph{User's Guide} and \emph{Frequently Asked Questions} for this
16.167 + sophisticated text editor.
16.168 +
16.169 + Most of this information about jEdit is relevant for Isabelle/jEdit
16.170 + as well, but one needs to keep in mind that defaults sometimes
16.171 + differ, and the official jEdit documentation does not know about the
16.172 + Isabelle plugin with its special support for theory editing.
16.173 +*}
16.174 +
16.175 +
16.176 +subsection {* Plugins *}
16.177 +
16.178 +text {* The \emph{Plugin Manager} of jEdit allows to augment editor
16.179 + functionality by JVM modules (jars) that are provided by the central
16.180 + plugin repository, which is accessible via various mirror sites.
16.181 +
16.182 + Connecting to the plugin server infrastructure of the jEdit project
16.183 + allows to update bundled plugins or to add further functionality.
16.184 + This needs to be done with the usual care for such an open bazaar of
16.185 + contributions. Arbitrary combinations of add-on features are apt to
16.186 + cause problems. It is advisable to start with the default
16.187 + configuration of Isabelle/jEdit and develop some understanding how
16.188 + it is supposed to work, before loading additional plugins at a grand
16.189 + scale.
16.190 +
16.191 + \medskip The main \emph{Isabelle} plugin is an integral part of
16.192 + Isabelle/jEdit and needs to remain active at all times! A few
16.193 + additional plugins are bundled with Isabelle/jEdit for convenience
16.194 + or out of necessity, notably \emph{Console} with its Isabelle/Scala
16.195 + sub-plugin and \emph{SideKick} with some Isabelle-specific parsers
16.196 + for document tree structure. The \emph{ErrorList} plugin is
16.197 + required by \emph{SideKick}, but not used specifically in
16.198 + Isabelle/jEdit. *}
16.199 +
16.200 +
16.201 +subsection {* Options *}
16.202 +
16.203 +text {* Both jEdit and Isabelle have distinctive management of
16.204 + persistent options.
16.205 +
16.206 + Regular jEdit options are accessible via the dialog for
16.207 + \emph{Plugins / Plugin Options}, which is also accessible via
16.208 + \emph{Utilities / Global Options}. Changed properties are stored in
16.209 + @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"}. In
16.210 + contrast, Isabelle system options are managed by Isabelle/Scala and
16.211 + changed values stored in @{file_unchecked
16.212 + "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit
16.213 + properties. See also \cite{isabelle-sys}, especially the coverage
16.214 + of sessions and command-line tools like @{tool build} or @{tool
16.215 + options}.
16.216 +
16.217 + Those Isabelle options that are declared as \textbf{public} are
16.218 + configurable in jEdit via \emph{Plugin Options / Isabelle /
16.219 + General}. Moreover, there are various options for rendering of
16.220 + document content, which are configurable via \emph{Plugin Options /
16.221 + Isabelle / Rendering}. Thus \emph{Plugin Options / Isabelle} in
16.222 + jEdit provides a view on a subset of Isabelle system options. Note
16.223 + that some of these options affect general parameters that are
16.224 + relevant outside Isabelle/jEdit as well, e.g.\ @{system_option
16.225 + threads} or @{system_option parallel_proofs} for the Isabelle build
16.226 + tool \cite{isabelle-sys}.
16.227 +
16.228 + \medskip All options are loaded on startup and saved on shutdown of
16.229 + Isabelle/jEdit. Editing the machine-generated @{file_unchecked
16.230 + "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
16.231 + "$ISABELLE_HOME_USER/etc/preferences"} manually while the
16.232 + application is running is likely to cause surprise due to lost
16.233 + update! *}
16.234 +
16.235 +
16.236 +subsection {* Keymaps *}
16.237 +
16.238 +text {* Keyboard shortcuts used to be managed as jEdit properties in
16.239 + the past, but recent versions (2013) have a separate concept of
16.240 + \emph{keymap} that is configurable via \emph{Global Options /
16.241 + Shortcuts}. The @{verbatim imported} keymap is derived from the
16.242 + initial environment of properties that is available at the first
16.243 + start of the editor; afterwards the keymap file takes precedence.
16.244 +
16.245 + This is relevant for Isabelle/jEdit due to various fine-tuning of
16.246 + default properties, and additional keyboard shortcuts for Isabelle
16.247 + specific functionality. Users may change their keymap later, but
16.248 + need to copy Isabelle-specific key bindings manually (see also
16.249 + @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}). *}
16.250 +
16.251 +
16.252 +subsection {* Look-and-feel *}
16.253 +
16.254 +text {* jEdit is a Java/AWT/Swing application with some ambition to
16.255 + support ``native'' look-and-feel on all platforms, within the limits
16.256 + of what Oracle as Java provider and major operating system
16.257 + distributors allow (see also \secref{sec:problems}).
16.258 +
16.259 + Isabelle/jEdit enables platform-specific look-and-feel by default as
16.260 + follows:
16.261 +
16.262 + \begin{description}
16.263 +
16.264 + \item[Linux] The platform-independent \emph{Nimbus} is used by
16.265 + default.
16.266 +
16.267 + \emph{GTK+} works under the side-condition that the overall GTK
16.268 + theme is selected in a Swing-friendly way.\footnote{GTK support in
16.269 + Java/Swing was once marketed aggressively by Sun, but never quite
16.270 + finished, and is today (2013) lagging a bit behind further
16.271 + development of Swing and GTK.}
16.272 +
16.273 + \item[Windows] Regular \emph{Windows} is used by default, but
16.274 + \emph{Windows Classic} also works.
16.275 +
16.276 + \item[Mac OS X] Regular \emph{Mac OS X} is used by default.
16.277 +
16.278 + Moreover the bundled \emph{MacOSX} plugin provides various functions
16.279 + that are expected from applications on that particular platform:
16.280 + quit from menu or dock, preferences menu, drag-and-drop of text
16.281 + files on the application, full-screen mode for main editor windows
16.282 + etc.
16.283 +
16.284 + \end{description}
16.285 +
16.286 + Users may experiment with different look-and-feels, but need to keep
16.287 + in mind that this extra variance of GUI functionality is unlikely to
16.288 + work in arbitrary combinations. The platform-independent
16.289 + \emph{Nimbus} and \emph{Metal} should always work. The historic
16.290 + \emph{CDE/Motif} is better avoided.
16.291 +
16.292 + After changing the look-and-feel in \emph{Global Options /
16.293 + Appearance}, it is advisable to restart Isabelle/jEdit in order to
16.294 + take full effect. *}
16.295 +
16.296 +
16.297 chapter {* Prover IDE functionality *}
16.298
16.299 -section {* Isabelle symbols and fonts *}
16.300 +section {* File-system access *}
16.301
16.302 -text {*
16.303 - Isabelle supports infinitely many symbols:
16.304 +text {* File specifications in jEdit follow various formats and
16.305 + conventions according to \emph{Virtual File Systems}, which may be
16.306 + also provided by additional plugins. This allows to access remote
16.307 + files via the @{verbatim "http:"} protocol prefix, for example.
16.308 + Isabelle/jEdit attempts to work with the file-system access model of
16.309 + jEdit as far as possible. In particular, theory sources are passed
16.310 + directly from the editor to the prover, without indirection via
16.311 + files.
16.312 +
16.313 + Despite the flexibility of URLs in jEdit, local files are
16.314 + particularly important and are accessible without protocol prefix.
16.315 + Here the path notation is that of the Java Virtual Machine on the
16.316 + underlying platform. On Windows the preferred form uses
16.317 + backslashes, but happens to accept Unix/POSIX forward slashes, too.
16.318 + Further differences arise due to drive letters and network shares.
16.319 +
16.320 + The Java notation for files needs to be distinguished from the one
16.321 + of Isabelle, which uses POSIX notation with forward slashes on
16.322 + \emph{all} platforms.\footnote{Isabelle on Windows uses Cygwin
16.323 + file-system access.} Moreover, environment variables from the
16.324 + Isabelle process may be used freely, e.g.\ @{file
16.325 + "$ISABELLE_HOME/etc/symbols"} or @{file
16.326 + "$ISABELLE_JDK_HOME/README.html"}. There are special shortcuts:
16.327 + @{file "~"} for @{file "$USER_HOME"} and @{file "~~"} for @{file
16.328 + "$ISABELLE_HOME"}.
16.329 +
16.330 + \medskip Since jEdit happens to support environment variables within
16.331 + file specifications as well, it is natural to use similar notation
16.332 + within the editor, e.g.\ in the file-browser. This does not work in
16.333 + full generality, though, due to the bias of jEdit towards
16.334 + platform-specific notation and of Isabelle towards POSIX. Moreover,
16.335 + the Isabelle settings environment is not yet active when starting
16.336 + Isabelle/jEdit via its standard application wrapper (in contrast to
16.337 + @{verbatim "isabelle jedit"} run from the command line).
16.338 +
16.339 + For convenience, Isabelle/jEdit imitates at least @{verbatim
16.340 + "$ISABELLE_HOME"} and @{verbatim "$ISABELLE_HOME_USER"} within the
16.341 + Java process environment, in order to allow easy access to these
16.342 + important places from the editor.
16.343 +
16.344 + Moreover note that path specifications in prover input or output
16.345 + usually include formal markup that turns it into a hyperlink (see
16.346 + also \secref{sec:tooltips-hyperlinks}). This allows to open the
16.347 + corresponding file in the text editor, independently of the path
16.348 + notation. *}
16.349 +
16.350 +
16.351 +section {* Text buffers and theories \label{sec:buffers-theories} *}
16.352 +
16.353 +text {* As regular text editor, jEdit maintains a collection of open
16.354 + \emph{text buffers} to store source files; each buffer may be
16.355 + associated with any number of visible \emph{text areas}. Buffers
16.356 + are subject to an \emph{edit mode} that is determined from the file
16.357 + type. Files with extension \texttt{.thy} are assigned to the mode
16.358 + \emph{isabelle} and treated specifically.
16.359 +
16.360 + \medskip Isabelle theory files are automatically added to the formal
16.361 + document model of Isabelle/Scala, which maintains a family of
16.362 + versions of all sources for the prover. The \emph{Theories} panel
16.363 + provides an overview of the status of continuous checking of theory
16.364 + sources. Unlike batch sessions \cite{isabelle-sys}, theory nodes
16.365 + are identified by full path names; this allows to work with multiple
16.366 + (disjoint) Isabelle sessions simultaneously within the same editor
16.367 + session.
16.368 +
16.369 + Certain events to open or update buffers with theory files cause
16.370 + Isabelle/jEdit to resolve dependencies of \emph{theory imports}.
16.371 + The system requests to load additional files into editor buffers, in
16.372 + order to be included in the theory document model for further
16.373 + checking. It is also possible to resolve dependencies
16.374 + automatically, depending on \emph{Plugin Options / Isabelle /
16.375 + General / Auto load}.
16.376 +
16.377 + \medskip The open text area views on theory buffers define the
16.378 + visible \emph{perspective} of Isabelle/jEdit. This is taken as a
16.379 + hint for document processing: the prover ensures that those parts of
16.380 + a theory where the user is looking are checked, while other parts
16.381 + that are presently not required are ignored. The perspective is
16.382 + changed by opening or closing text area windows, or scrolling within
16.383 + an editor window.
16.384 +
16.385 + The \emph{Theories} panel provides some further options to influence
16.386 + the process of continuous checking: it may be switched off globally
16.387 + to restrict the prover to superficial processing of command syntax.
16.388 + It is also possible to indicate theory nodes as \emph{required} for
16.389 + continuous checking: this means such nodes and all their imports are
16.390 + always processed independently of the visibility status (if
16.391 + continuous checking is enabled). Big theory libraries that are
16.392 + marked as required can have significant impact on performance,
16.393 + though.
16.394 +
16.395 + \medskip Formal markup of checked theory content is turned into GUI
16.396 + rendering, based on a standard repertoire known from IDEs for
16.397 + programming languages: colors, icons, highlighting, squiggly
16.398 + underline, tooltips, hyperlinks etc. For outer syntax of
16.399 + Isabelle/Isar there is some traditional syntax-highlighting via
16.400 + static keyword tables and tokenization within the editor. In
16.401 + contrast, the painting of inner syntax (term language etc.)\ uses
16.402 + semantic information that is reported dynamically from the logical
16.403 + context. Thus the prover can provide additional markup to help the
16.404 + user to understand the meaning of formal text, and to produce more
16.405 + text with some add-on tools (e.g.\ information messages by automated
16.406 + provers or disprovers running in the background).
16.407 +*}
16.408 +
16.409 +
16.410 +section {* Prover output \label{sec:prover-output} *}
16.411 +
16.412 +text {* Prover output consists of \emph{markup} and \emph{messages}.
16.413 + Both are directly attached to the corresponding positions in the
16.414 + original source text, and visualized in the text area, e.g.\ as text
16.415 + colours for free and bound variables, or as squiggly underline for
16.416 + warnings, errors etc.\ (see also \figref{fig:output}). In the
16.417 + latter case, the corresponding messages are shown by hovering with
16.418 + the mouse over the highlighted text --- although in many situations
16.419 + the user should already get some clue by looking at the position of
16.420 + the text highlighting.
16.421 +
16.422 + \begin{figure}[htb]
16.423 + \begin{center}
16.424 + \includegraphics[width=\textwidth]{output}
16.425 + \end{center}
16.426 + \caption{Multiple views on prover output: gutter area with icon,
16.427 + text area with popup, overview area, Theories panel, Output panel}
16.428 + \label{fig:output}
16.429 + \end{figure}
16.430 +
16.431 + The ``gutter area'' on the left-hand-side of the text area uses
16.432 + icons to provide a summary of the messages within the adjacent
16.433 + line of text. Message priorities are used to prefer errors over
16.434 + warnings, warnings over information messages etc. Plain output is
16.435 + ignored here.
16.436 +
16.437 + The ``overview area'' on the right-hand-side of the text area uses
16.438 + similar information to paint small rectangles for the overall status
16.439 + of the whole text buffer. The graphics is scaled to fit the logical
16.440 + buffer length into the given window height. Mouse clicks on the
16.441 + overview area position the cursor approximately to the corresponding
16.442 + line of text in the buffer. Repainting the overview in real-time
16.443 + causes problems with big theories, so it is restricted to part of
16.444 + the text according to \emph{Plugin Options / Isabelle / General /
16.445 + Text Overview Limit} (in characters).
16.446 +
16.447 + Another course-grained overview is provided by the \emph{Theories}
16.448 + panel, but without direct correspondence to text positions. A
16.449 + double-click on one of the theory entries with their status overview
16.450 + opens the corresponding text buffer, without changing the cursor
16.451 + position.
16.452 +
16.453 + \medskip In addition, the \emph{Output} panel displays prover
16.454 + messages that correspond to a given command, within a separate
16.455 + window.
16.456 +
16.457 + The cursor position in the presently active text area determines the
16.458 + prover commands whose cumulative message output is appended and
16.459 + shown in that window (in canonical order according to the processing
16.460 + of the command). There are also control elements to modify the
16.461 + update policy of the output wrt.\ continued editor movements. This
16.462 + is particularly useful with several independent instances of the
16.463 + \emph{Output} panel, which the Dockable Window Manager of jEdit can
16.464 + handle conveniently.
16.465 +
16.466 + Former users of the old TTY interaction model (e.g.\ Proof~General)
16.467 + might find a separate window for prover messages familiar, but it is
16.468 + important to understand that the main Prover IDE feedback happens
16.469 + elsewhere. It is possible to do meaningful proof editing
16.470 + efficiently, using secondary output windows only rarely.
16.471 +
16.472 + The main purpose of the output window is to ``debug'' unclear
16.473 + situations by inspecting internal state of the prover.\footnote{In
16.474 + that sense, unstructured tactic scripts depend on continuous
16.475 + debugging with internal state inspection.} Consequently, some
16.476 + special messages for \emph{tracing} or \emph{proof state} only
16.477 + appear here, and are not attached to the original source.
16.478 +
16.479 + \medskip In any case, prover messages also contain markup that may
16.480 + be explored recursively via tooltips or hyperlinks (see
16.481 + \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate
16.482 + certain actions (see \secref{sec:auto-tools} and
16.483 + \secref{sec:sledgehammer}). *}
16.484 +
16.485 +
16.486 +section {* Tooltips and hyperlinks \label{sec:tooltips-hyperlinks} *}
16.487 +
16.488 +text {* Formally processed text (prover input or output) contains rich
16.489 + markup information that can be explored further by using the
16.490 + @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim
16.491 + COMMAND} on Mac OS X. Hovering with the mouse while the modifier is
16.492 + pressed reveals a \emph{tooltip} (grey box over the text with a
16.493 + yellow popup) and/or a \emph{hyperlink} (black rectangle over the
16.494 + text); see also \figref{fig:tooltip}.
16.495 +
16.496 + \begin{figure}[htb]
16.497 + \begin{center}
16.498 + \includegraphics[scale=0.3]{popup1}
16.499 + \end{center}
16.500 + \caption{Tooltip and hyperlink for some formal entity}
16.501 + \label{fig:tooltip}
16.502 + \end{figure}
16.503 +
16.504 + Tooltip popups use the same rendering principles as the main text
16.505 + area, and further tooltips and/or hyperlinks may be exposed
16.506 + recursively by the same mechanism; see \figref{fig:nested-tooltips}.
16.507 +
16.508 + \begin{figure}[htb]
16.509 + \begin{center}
16.510 + \includegraphics[scale=0.3]{popup2}
16.511 + \end{center}
16.512 + \caption{Nested tooltips over formal entities}
16.513 + \label{fig:nested-tooltips}
16.514 + \end{figure}
16.515 +
16.516 + The tooltip popup window provides some controls to \emph{close} or
16.517 + \emph{detach} the window, turning it into a separate \emph{Info}
16.518 + window managed by jEdit. The @{verbatim ESCAPE} key closes
16.519 + \emph{all} popups, which is particularly relevant when nested
16.520 + tooltips are stacking up.
16.521 +
16.522 + \medskip A black rectangle in the text indicates a hyperlink that
16.523 + may be followed by a mouse click (while the @{verbatim CONTROL} or
16.524 + @{verbatim COMMAND} modifier key is still pressed). Presently
16.525 + (Isabelle2013-1) there is no systematic navigation within the
16.526 + editor to return to the original location.
16.527 +
16.528 + Also note that the link target may be a file that is itself not
16.529 + subject to formal document processing of the editor session and thus
16.530 + prevents further exploration: the chain of hyperlinks may end in
16.531 + some source file of the underlying logic image, or within the
16.532 + Isabelle/ML bootstrap sources of Isabelle/Pure. *}
16.533 +
16.534 +
16.535 +section {* Text completion \label{sec:completion} *}
16.536 +
16.537 +text {* \paragraph{Completion tables} are determined statically from
16.538 + the ``outer syntax'' of the underlying edit mode (for theory files
16.539 + this is the syntax of Isar commands), and specifications of Isabelle
16.540 + symbols (see also \secref{sec:symbols}).
16.541 +
16.542 + Symbols are completed in backslashed forms, e.g.\ @{verbatim
16.543 + "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the
16.544 + Isabelle symbol @{text "\<forall>"} in its Unicode rendering.\footnote{The
16.545 + extra backslash avoids overlap with keywords of the buffer syntax,
16.546 + and allows to produce Isabelle symbols robustly in most syntactic
16.547 + contexts.} Alternatively, symbol abbreviations may be used as
16.548 + specified in @{file "$ISABELLE_HOME/etc/symbols"}.
16.549 +
16.550 + \paragraph{Completion popups} are required in situations of
16.551 + ambiguous completion results or where explicit confirmation is
16.552 + demanded before inserting completed text into the buffer.
16.553 +
16.554 + The popup is some minimally invasive GUI component over the text
16.555 + area. It interprets special keys @{verbatim TAB}, @{verbatim
16.556 + ESCAPE}, @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP},
16.557 + @{verbatim PAGE_DOWN}, but all other key events are passed to the
16.558 + underlying text area. This allows to ignore unwanted completions
16.559 + most of the time and continue typing quickly.
16.560 +
16.561 + The meaning of special keys is as follows:
16.562
16.563 \medskip
16.564 - \begin{tabular}{l}
16.565 - @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} \\
16.566 - @{text "\<forall>"}, @{text "\<exists>"}, @{text "\<or>"}, @{text "\<and>"}, @{text "\<longrightarrow>"}, @{text "\<longleftrightarrow>"}, @{text "\<dots>"} \\
16.567 - @{text "\<le>"}, @{text "\<ge>"}, @{text "\<sqinter>"}, @{text "\<squnion>"}, @{text "\<dots>"} \\
16.568 - @{text "\<aleph>"}, @{text "\<triangle>"}, @{text "\<nabla>"}, @{text "\<dots>"} \\
16.569 - @{verbatim "\<foo>"}, @{verbatim "\<bar>"}, @{verbatim "\<baz>"}, @{text "\<dots>"} \\
16.570 + \begin{tabular}{ll}
16.571 + \textbf{key} & \textbf{action} \\\hline
16.572 + @{verbatim "TAB"} & select completion \\
16.573 + @{verbatim "ESCAPE"} & dismiss popup \\
16.574 + @{verbatim "UP"} & move up one item \\
16.575 + @{verbatim "DOWN"} & move down one item \\
16.576 + @{verbatim "PAGE_UP"} & move up one page of items \\
16.577 + @{verbatim "PAGE_DOWN"} & move down one page of items \\
16.578 \end{tabular}
16.579 \medskip
16.580
16.581 - A default mapping relates some Isabelle symbols to Unicode points (see
16.582 - @{file "$ISABELLE_HOME/etc/symbols"} and @{verbatim
16.583 - "$ISABELLE_HOME_USER/etc/symbols"}.
16.584 + Movement within the popup is only active for multiple items.
16.585 + Otherwise the corresponding key event retains its standard meaning
16.586 + within the underlying text area.
16.587
16.588 - The \emph{IsabelleText} font ensures that Unicode points are actually seen
16.589 - on the screen (or printer).
16.590 + \paragraph{Explicit completion} is triggered by the keyboard
16.591 + shortcut @{verbatim "C+b"} (action @{verbatim "isabelle.complete"}).
16.592 + This overrides the original jEdit binding for action @{verbatim
16.593 + "complete-word"}, but the latter is used as fall-back for
16.594 + non-Isabelle edit modes. It is also possible to restore the
16.595 + original jEdit keyboard mapping of @{verbatim "complete-word"} via
16.596 + \emph{Global Options / Shortcuts}.
16.597
16.598 - \medskip
16.599 - Input methods:
16.600 + Replacement text is inserted immediately into the buffer, unless
16.601 + ambiguous results demand an explicit popup.
16.602 +
16.603 + \paragraph{Implicit completion} is triggered by regular keyboard
16.604 + input events during of the editing process in the main jEdit text
16.605 + area (and a few additional text fields like the search criteria of
16.606 + the Find panel, see \secref{sec:find}). Implicit completion depends
16.607 + on on further side-conditions:
16.608 +
16.609 \begin{enumerate}
16.610 - \item use the \emph{Symbols} dockable window
16.611 - \item copy/paste from decoded source files
16.612 - \item copy/paste from prover output
16.613 - \item completion provided by Isabelle plugin, e.g.\
16.614 +
16.615 + \item The system option @{system_option jedit_completion} needs to
16.616 + be enabled (default).
16.617 +
16.618 + \item Completion of syntax keywords requires at least 3 relevant
16.619 + characters in the text.
16.620 +
16.621 + \item The system option @{system_option jedit_completion_delay}
16.622 + determines an additional delay (0.0 by default), before opening a
16.623 + completion popup.
16.624 +
16.625 + \item The system option @{system_option
16.626 + jedit_completion_dismiss_delay} determines an additional delay (0.0
16.627 + by default), before dismissing an earlier completion popup. A value
16.628 + like 0.1 is occasionally useful to reduce the chance of loosing key
16.629 + strokes when the speed of typing exceeds that of repainting GUI
16.630 + components.
16.631 +
16.632 + \item The system option @{system_option jedit_completion_immediate}
16.633 + (disabled by default) controls whether replacement text should be
16.634 + inserted immediately without popup. This is restricted to Isabelle
16.635 + symbols and their abbreviations (\secref{sec:symbols}) --- plain
16.636 + keywords always demand a popup for clarity.
16.637 +
16.638 + \item Completion of symbol abbreviations with only one relevant
16.639 + character in the text always enforces an explicit popup,
16.640 + independently of @{system_option jedit_completion_immediate}.
16.641 +
16.642 + \end{enumerate}
16.643 +
16.644 + These completion options may be configured in \emph{Plugin Options /
16.645 + Isabelle / General / Completion}. The default is quite moderate in
16.646 + showing occasional popups and refraining from immediate insertion.
16.647 + An additional completion delay of 0.3 seconds will make it even less
16.648 + ambitious.
16.649 +
16.650 + In contrast, more aggressive completion works via @{system_option
16.651 + jedit_completion_delay}~@{verbatim "= 0.0"} and @{system_option
16.652 + jedit_completion_immediate}~@{verbatim "= true"}. Thus the editing
16.653 + process becomes dependent on the system guessing correctly what the
16.654 + user had in mind. It requires some practice (and study of the
16.655 + symbol abbreviation tables) to become productive in this advanced
16.656 + mode.
16.657 +
16.658 + In any case, unintended completions can be reverted by the regular
16.659 + @{verbatim undo} operation of jEdit. When editing embedded
16.660 + languages such as ML, it is better to disable either @{system_option
16.661 + jedit_completion} or @{system_option jedit_completion_immediate}
16.662 + temporarily. *}
16.663 +
16.664 +
16.665 +section {* Isabelle symbols \label{sec:symbols} *}
16.666 +
16.667 +text {* Isabelle sources consist of \emph{symbols} that extend plain
16.668 + ASCII to allow infinitely many mathematical symbols within the
16.669 + formal sources. This works without depending on particular
16.670 + encodings and varying Unicode standards
16.671 + \cite{Wenzel:2011:CICM}.\footnote{Raw Unicode characters within
16.672 + formal sources would compromise portability and reliability in the
16.673 + face of changing interpretation of special features of Unicode, such
16.674 + as Combining Characters or Bi-directional Text.}
16.675 +
16.676 + For the prover back-end, formal text consists of ASCII characters
16.677 + that are grouped according to some simple rules, e.g.\ as plain
16.678 + ``@{verbatim a}'' or symbolic ``@{verbatim "\<alpha>"}''.
16.679 +
16.680 + For the editor front-end, a certain subset of symbols is rendered
16.681 + physically via Unicode glyphs, in order to show ``@{verbatim "\<alpha>"}''
16.682 + as ``@{text "\<alpha>"}'', for example. This symbol interpretation is
16.683 + specified by the Isabelle system distribution in @{file
16.684 + "$ISABELLE_HOME/etc/symbols"} and may be augmented by the user in
16.685 + @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
16.686 +
16.687 + The appendix of \cite{isabelle-isar-ref} gives an overview of the
16.688 + standard interpretation of finitely many symbols from the infinite
16.689 + collection. Uninterpreted symbols are displayed literally, e.g.\
16.690 + ``@{verbatim "\<foobar>"}''. Overlap of Unicode characters used in
16.691 + symbol interpretation with informal ones (which might appear e.g.\
16.692 + in comments) needs to be avoided! Raw Unicode characters within
16.693 + prover source files should be restricted to informal parts, e.g.\ to
16.694 + write text in non-latin alphabets in comments.
16.695 +
16.696 + \medskip \paragraph{Encoding.} Technically, the Unicode view on
16.697 + Isabelle symbols is an \emph{encoding} in jEdit (not in the
16.698 + underlying JVM) that is called @{verbatim "UTF-8-Isabelle"}. It is
16.699 + provided by the Isabelle/jEdit plugin and enabled by default for all
16.700 + source files. Sometimes such defaults are reset accidentally, or
16.701 + malformed UTF-8 sequences in the text force jEdit to fall back on a
16.702 + different encoding like @{verbatim "ISO-8859-15"}. In that case,
16.703 + verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer
16.704 + instead of its Unicode rendering ``@{text "\<alpha>"}''. The jEdit menu
16.705 + operation \emph{File / Reload with Encoding / UTF-8-Isabelle} helps
16.706 + to resolve such problems, potentially after repairing malformed
16.707 + parts of the text.
16.708 +
16.709 + \medskip \paragraph{Font.} Correct rendering via Unicode requires a
16.710 + font that contains glyphs for the corresponding codepoints. Most
16.711 + system fonts lack that, so Isabelle/jEdit prefers its own
16.712 + application font @{verbatim IsabelleText}, which ensures that
16.713 + standard collection of Isabelle symbols are actually seen on the
16.714 + screen (or printer).
16.715 +
16.716 + Note that a Java/AWT/Swing application can load additional fonts
16.717 + only if they are not installed on the operating system already!
16.718 + Some old version of @{verbatim IsabelleText} that happens to be
16.719 + provided by the operating system would prevents Isabelle/jEdit from
16.720 + its bundled version. This could lead to missing glyphs (black
16.721 + rectangles), when the system version of @{verbatim IsabelleText} is
16.722 + older than the application version. This problem can be avoided by
16.723 + refraining to ``install'' any version of @{verbatim IsabelleText} in
16.724 + the first place (although it might be occasionally tempting to use
16.725 + the same font in other applications).
16.726 +
16.727 + \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
16.728 + could delegate the problem to produce Isabelle symbols in their
16.729 + Unicode rendering to the underlying operating system and its
16.730 + \emph{input methods}. Regular jEdit also provides various ways to
16.731 + work with \emph{abbreviations} to produce certain non-ASCII
16.732 + characters. Since none of these standard input methods work
16.733 + satisfactorily for the mathematical characters required for
16.734 + Isabelle, various specific Isabelle/jEdit mechanisms are provided.
16.735 +
16.736 + Here is a summary for practically relevant input methods for
16.737 + Isabelle symbols:
16.738 +
16.739 + \begin{enumerate}
16.740 +
16.741 + \item The \emph{Symbols} panel with some GUI buttons to insert
16.742 + certain symbols in the text buffer. There are also tooltips to
16.743 + reveal the official Isabelle representation with some additional
16.744 + information about \emph{symbol abbreviations} (see below).
16.745 +
16.746 + \item Copy / paste from decoded source files: text that is rendered
16.747 + as Unicode already can be re-used to produce further text. This
16.748 + also works between different applications, e.g.\ Isabelle/jEdit and
16.749 + some web browser or mail client, as long as the same Unicode view on
16.750 + Isabelle symbols is used uniformly.
16.751 +
16.752 + \item Copy / paste from prover output within Isabelle/jEdit. The
16.753 + same principles as for text buffers apply, but note that \emph{copy}
16.754 + in secondary Isabelle/jEdit windows works via the keyboard shortcut
16.755 + @{verbatim "C+c"}, while jEdit menu actions always refer to the
16.756 + primary text area!
16.757 +
16.758 + \item Completion provided by Isabelle plugin (see
16.759 + \secref{sec:completion}). Isabelle symbols have a canonical name
16.760 + and optional abbreviations. This can be used with the text
16.761 + completion mechanism of Isabelle/jEdit, to replace a prefix of the
16.762 + actual symbol like @{verbatim "\<lambda>"}, or its backslashed name
16.763 + @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
16.764 + @{verbatim "%"} by the Unicode rendering.
16.765 +
16.766 + The following table is an extract of the information provided by the
16.767 + standard @{file "$ISABELLE_HOME/etc/symbols"} file:
16.768
16.769 \medskip
16.770 \begin{tabular}{lll}
16.771 - \textbf{symbol} & \textbf{abbreviation} & \textbf{backslash escape} \\[1ex]
16.772 + \textbf{symbol} & \textbf{backslashed name} & \textbf{abbreviation} \\\hline
16.773 + @{text "\<lambda>"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\
16.774 + @{text "\<Rightarrow>"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\
16.775 + @{text "\<Longrightarrow>"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex]
16.776 + @{text "\<And>"} & @{verbatim "\\And"} & @{verbatim "!!"} \\
16.777 + @{text "\<equiv>"} & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex]
16.778 + @{text "\<forall>"} & @{verbatim "\\forall"} & @{verbatim "!"} \\
16.779 + @{text "\<exists>"} & @{verbatim "\\exists"} & @{verbatim "?"} \\
16.780 + @{text "\<longrightarrow>"} & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\
16.781 + @{text "\<and>"} & @{verbatim "\\and"} & @{verbatim "&"} \\
16.782 + @{text "\<or>"} & @{verbatim "\\or"} & @{verbatim "|"} \\
16.783 + @{text "\<not>"} & @{verbatim "\\not"} & @{verbatim "~"} \\
16.784 + @{text "\<noteq>"} & @{verbatim "\\noteq"} & @{verbatim "~="} \\
16.785 + @{text "\<in>"} & @{verbatim "\\in"} & @{verbatim ":"} \\
16.786 + @{text "\<notin>"} & @{verbatim "\\notin"} & @{verbatim "~:"} \\
16.787 + \end{tabular}
16.788 + \medskip
16.789
16.790 - @{text "\<lambda>"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\
16.791 - @{text "\<Rightarrow>"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\
16.792 - @{text "\<Longrightarrow>"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\
16.793 + Note that the above abbreviations refer to the input method. The
16.794 + logical notation provides ASCII alternatives that often coincide,
16.795 + but deviate occasionally. This occasionally causes user confusion
16.796 + with very old-fashioned Isabelle source that use ASCII replacement
16.797 + notation like @{verbatim "!"} or @{verbatim "ALL"} directly in the
16.798 + text.
16.799
16.800 - @{text "\<And>"} & @{verbatim "!!"} & @{verbatim "\\And"} \\
16.801 - @{text "\<equiv>"} & @{verbatim "=="} & @{verbatim "\\equiv"} \\
16.802 -
16.803 - @{text "\<forall>"} & @{verbatim "!"} & @{verbatim "\\forall"} \\
16.804 - @{text "\<exists>"} & @{verbatim "?"} & @{verbatim "\\exists"} \\
16.805 - @{text "\<longrightarrow>"} & @{verbatim "-->"} & @{verbatim "\\longrightarrow"} \\
16.806 - @{text "\<and>"} & @{verbatim "&"} & @{verbatim "\\and"} \\
16.807 - @{text "\<or>"} & @{verbatim "|"} & @{verbatim "\\or"} \\
16.808 - @{text "\<not>"} & @{verbatim "~"} & @{verbatim "\\not"} \\
16.809 - @{text "\<noteq>"} & @{verbatim "~="} & @{verbatim "\\noteq"} \\
16.810 - @{text "\<in>"} & @{verbatim ":"} & @{verbatim "\\in"} \\
16.811 - @{text "\<notin>"} & @{verbatim "~:"} & @{verbatim "\\notin"} \\
16.812 - \end{tabular}
16.813 + On the other hand, coincidence of symbol abbreviations with ASCII
16.814 + replacement syntax syntax helps to update old theory sources via
16.815 + explicit completion (see also @{verbatim "C+b"} explained in
16.816 + \secref{sec:completion}).
16.817
16.818 \end{enumerate}
16.819
16.820 - \paragraph{Notes:}
16.821 + \paragraph{Control symbols.} There are some special control symbols
16.822 + to modify the display style of a single symbol (without
16.823 + nesting). Control symbols may be applied to a region of selected
16.824 + text, either using the \emph{Symbols} panel or keyboard shortcuts or
16.825 + jEdit actions. These editor operations produce a separate control
16.826 + symbol for each symbol in the text, in order to make the whole text
16.827 + appear in a certain style.
16.828 +
16.829 + \medskip
16.830 + \begin{tabular}{llll}
16.831 + \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
16.832 + superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{verbatim "isabelle.control-sup"} \\
16.833 + subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{verbatim "isabelle.control-sub"} \\
16.834 + bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{verbatim "isabelle.control-bold"} \\
16.835 + reset & & @{verbatim "C+e LEFT"} & @{verbatim "isabelle.control-reset"} \\
16.836 + \end{tabular}
16.837 + \medskip
16.838 +
16.839 + To produce a single control symbol, it is also possible to complete
16.840 + on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub},
16.841 + @{verbatim "\\"}@{verbatim bold} as for regular symbols. *}
16.842 +
16.843 +
16.844 +section {* Automatically tried tools \label{sec:auto-tools} *}
16.845 +
16.846 +text {* Continuous document processing works asynchronously in the
16.847 + background. Visible document source that has been evaluated already
16.848 + may get augmented by additional results of \emph{asynchronous print
16.849 + functions}. The canonical example is proof state output, which is
16.850 + always enabled. More heavy-weight print functions may be applied,
16.851 + in order to prove or disprove parts of the formal text by other
16.852 + means.
16.853 +
16.854 + Isabelle/HOL provides various automatically tried tools that operate
16.855 + on outermost goal statements (e.g.\ @{command lemma}, @{command
16.856 + theorem}), independently of the state of the current proof attempt.
16.857 + They work implicitly without any arguments. Results are output as
16.858 + \emph{information messages}, which are indicated in the text area by
16.859 + blue squiggles and a blue information sign in the gutter (see
16.860 + \figref{fig:auto-tools}). The message content may be shown as for
16.861 + other output (see also \secref{sec:prover-output}). Some tools
16.862 + produce output with \emph{sendback} markup, which means that
16.863 + clicking on certain parts of the output inserts that text into the
16.864 + source in the proper place.
16.865 +
16.866 + \begin{figure}[htb]
16.867 + \begin{center}
16.868 + \includegraphics[scale=0.3]{auto-tools}
16.869 + \end{center}
16.870 + \caption{Results of automatically tried tools}
16.871 + \label{fig:auto-tools}
16.872 + \end{figure}
16.873 +
16.874 + \medskip The following Isabelle system options control the behavior
16.875 + of automatically tried tools (see also the jEdit dialog window
16.876 + \emph{Plugin Options / Isabelle / General / Automatically tried
16.877 + tools}):
16.878 +
16.879 \begin{itemize}
16.880
16.881 - \item The above abbreviations refer to the input method. The logical
16.882 - notation provides ASCII alternatives that often coincide, but deviate
16.883 - occasionally.
16.884 + \item @{system_option auto_methods} controls automatic use of a
16.885 + combination of standard proof methods (@{method auto}, @{method
16.886 + simp}, @{method blast}, etc.). This corresponds to the Isar command
16.887 + @{command "try0"}.
16.888
16.889 - \item Generic jEdit abbreviations or plugins perform similar source
16.890 - replacement operations; this works for Isabelle as long as the Unicode
16.891 - sequences coincide with the symbol mapping.
16.892 + The tool is disabled by default, since unparameterized invocation of
16.893 + standard proof methods often consumes substantial CPU resources
16.894 + without leading to success.
16.895
16.896 - \item Raw Unicode characters within prover source files should be
16.897 - restricted to informal parts, e.g.\ to write text in non-latin alphabets.
16.898 - Mathematical symbols should be defined via the official rendering tables.
16.899 + \item @{system_option auto_nitpick} controls a slightly reduced
16.900 + version of @{command nitpick}, which tests for counterexamples using
16.901 + first-order relational logic. See also the Nitpick manual
16.902 + \cite{isabelle-nitpick}.
16.903 +
16.904 + This tool is disabled by default, due to the extra overhead of
16.905 + invoking an external Java process for each attempt to disprove a
16.906 + subgoal.
16.907 +
16.908 + \item @{system_option auto_quickcheck} controls automatic use of
16.909 + @{command quickcheck}, which tests for counterexamples using a
16.910 + series of assignments for free variables of a subgoal.
16.911 +
16.912 + This tool is \emph{enabled} by default. It requires little
16.913 + overhead, but is a bit weaker than @{command nitpick}.
16.914 +
16.915 + \item @{system_option auto_sledgehammer} controls a significantly
16.916 + reduced version of @{command sledgehammer}, which attempts to prove
16.917 + a subgoal using external automatic provers. See also the
16.918 + Sledgehammer manual \cite{isabelle-sledgehammer}.
16.919 +
16.920 + This tool is disabled by default, due to the relatively heavy nature
16.921 + of Sledgehammer.
16.922 +
16.923 + \item @{system_option auto_solve_direct} controls automatic use of
16.924 + @{command solve_direct}, which checks whether the current subgoals
16.925 + can be solved directly by an existing theorem. This also helps to
16.926 + detect duplicate lemmas.
16.927 +
16.928 + This tool is \emph{enabled} by default.
16.929
16.930 \end{itemize}
16.931
16.932 - \paragraph{Control symbols.} There are some special control symbols to
16.933 - modify the style of a \emph{single} symbol (without nesting). Control
16.934 - symbols may be applied to a region of selected text, either using the
16.935 - \emph{Symbols} dockable window or keyboard shortcuts.
16.936 + Invocation of automatically tried tools is subject to some global
16.937 + policies of parallel execution, which may be configured as follows:
16.938
16.939 - \medskip
16.940 - \begin{tabular}{lll}
16.941 - \textbf{symbol} & style & keyboard shortcure \\
16.942 - @{verbatim "\<sup>"} & superscript & @{verbatim "C+e UP"} \\
16.943 - @{verbatim "\<sub>"} & subscript & @{verbatim "C+e DOWN"} \\
16.944 - @{verbatim "\<bold>"} & bold face & @{verbatim "C+e RIGHT"} \\
16.945 - & reset & @{verbatim "C+e LEFT"} \\
16.946 - \end{tabular}
16.947 + \begin{itemize}
16.948 +
16.949 + \item @{system_option auto_time_limit} (default 2.0) determines the
16.950 + timeout (in seconds) for each tool execution.
16.951 +
16.952 + \item @{system_option auto_time_start} (default 1.0) determines the
16.953 + start delay (in seconds) for automatically tried tools, after the
16.954 + main command evaluation is finished.
16.955 +
16.956 + \end{itemize}
16.957 +
16.958 + Each tool is submitted independently to the pool of parallel
16.959 + execution tasks in Isabelle/ML, using hardwired priorities according
16.960 + to its relative ``heaviness''. The main stages of evaluation and
16.961 + printing of proof states take precedence, but an already running
16.962 + tool is not canceled and may thus reduce reactivity of proof
16.963 + document processing.
16.964 +
16.965 + Users should experiment how the available CPU resources (number of
16.966 + cores) are best invested to get additional feedback from prover in
16.967 + the background, by using a selection of weaker or stronger tools.
16.968 *}
16.969
16.970
16.971 -section {* Text completion *}
16.972 +section {* Sledgehammer \label{sec:sledgehammer} *}
16.973
16.974 -text {*
16.975 - Text completion works via some light-weight GUI popup, which is triggered by
16.976 - keyboard events during the normal editing process in the main jEdit text
16.977 - area and a few additional text fields. The popup interprets special keys:
16.978 - @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
16.979 - @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
16.980 - to the jEdit text area --- this allows to ignore unwanted completions most
16.981 - of the time and continue typing quickly.
16.982 +text {* The \emph{Sledgehammer} panel (\figref{fig:sledgehammer})
16.983 + provides a view on some independent execution of the Isar command
16.984 + @{command sledgehammer}, with process indicator (spinning wheel) and
16.985 + GUI elements for important Sledgehammer arguments and options. Any
16.986 + number of Sledgehammer panels may be active, according to the
16.987 + standard policies of Dockable Window Management in jEdit. Closing
16.988 + such windows also cancels the corresponding prover tasks.
16.989
16.990 - Various Isabelle plugin options control the popup behavior and immediate
16.991 - insertion into buffer.
16.992 + \begin{figure}[htb]
16.993 + \begin{center}
16.994 + \includegraphics[scale=0.3]{sledgehammer}
16.995 + \end{center}
16.996 + \caption{An instance of the Sledgehammer panel}
16.997 + \label{fig:sledgehammer}
16.998 + \end{figure}
16.999
16.1000 - Isabelle Symbols are completed in backslashed forms, e.g. @{verbatim
16.1001 - "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
16.1002 - symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
16.1003 - abbreviations may be used as specified in @{file
16.1004 - "$ISABELLE_HOME/etc/symbols"}.
16.1005 + The \emph{Apply} button attaches a fresh invocation of @{command
16.1006 + sledgehammer} to the command where the cursor is pointing in the
16.1007 + text --- this should be some pending proof problem. Further buttons
16.1008 + like \emph{Cancel} and \emph{Locate} help to manage the running
16.1009 + process.
16.1010
16.1011 - \emph{Explicit completion} works via standard jEdit shortcut @{verbatim
16.1012 - "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
16.1013 - fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
16.1014 + Results appear incrementally in the output window of the panel.
16.1015 + Proposed proof snippets are marked-up as \emph{sendback}, which
16.1016 + means a single mouse click inserts the text into a suitable place of
16.1017 + the original source. Some manual editing may be required
16.1018 + nonetheless, say to remove earlier proof attempts. *}
16.1019
16.1020 - \emph{Implicit completion} works via keyboard input on text area, with popup
16.1021 - or immediate insertion into buffer. Plain words require at least 3
16.1022 - characters to be completed.
16.1023
16.1024 - \emph{Immediate completion} means the (unique) replacement text is inserted
16.1025 - into the buffer without popup. This mode ignores plain words and requires
16.1026 - more than one characters for symbol abbreviations. Otherwise it falls back
16.1027 - on completion popup.
16.1028 +section {* Find theorems \label{sec:find} *}
16.1029 +
16.1030 +text {* The \emph{Find} panel (\figref{fig:find}) provides an
16.1031 + independent view for the Isar command @{command find_theorems}. The
16.1032 + main text field accepts search criteria according to the syntax
16.1033 + @{syntax thmcriterium} given in \cite{isabelle-isar-ref}. Further
16.1034 + options of @{command find_theorems} are available via GUI elements.
16.1035 +
16.1036 + \begin{figure}[htb]
16.1037 + \begin{center}
16.1038 + \includegraphics[scale=0.3]{find}
16.1039 + \end{center}
16.1040 + \caption{An instance of the Find panel}
16.1041 + \label{fig:find}
16.1042 + \end{figure}
16.1043 +
16.1044 + The \emph{Apply} button attaches a fresh invocation of @{command
16.1045 + find_theorems} to the current context of the command where the
16.1046 + cursor is pointing in the text, unless an alternative theory context
16.1047 + (from the underlying logic image) is specified explicitly. *}
16.1048 +
16.1049 +
16.1050 +chapter {* Miscellaneous tools *}
16.1051 +
16.1052 +section {* SideKick *}
16.1053 +
16.1054 +text {* The \emph{SideKick} plugin of jEdit provides some general
16.1055 + services to display buffer structure in a tree view.
16.1056 +
16.1057 + Isabelle/jEdit provides SideKick parsers for its main mode for
16.1058 + theory files, as well as some minor modes for the @{verbatim NEWS}
16.1059 + file, session @{verbatim ROOT} files, and system @{verbatim
16.1060 + options}.
16.1061 +
16.1062 + Moreover, the special SideKick parser @{verbatim "isabelle-markup"}
16.1063 + provides access to the full (uninterpreted) markup tree of the PIDE
16.1064 + document model of the current buffer. This is occasionally useful
16.1065 + for informative purposes, but the amount of displayed information
16.1066 + might cause problems for large buffers, both for the human and the
16.1067 + machine.
16.1068 *}
16.1069
16.1070
16.1071 -chapter {* Known problems and workarounds *}
16.1072 +section {* Timing *}
16.1073 +
16.1074 +text {* Managed evaluation of commands within PIDE documents includes
16.1075 + timing information, which consists of elapsed (wall-clock) time, CPU
16.1076 + time, and GC (garbage collection) time. Note that in a
16.1077 + multithreaded system it is difficult to measure execution time
16.1078 + precisely: elapsed time is closer to the real requirements of
16.1079 + runtime resources than CPU or GC time, which are both subject to
16.1080 + influences from the parallel environment that are outside the scope
16.1081 + of the current command transaction.
16.1082 +
16.1083 + The \emph{Timing} panel provides an overview of cumulative command
16.1084 + timings for each document node. Commands with elapsed time below
16.1085 + the given threshold are ignored in the grand total. Nodes are
16.1086 + sorted according to their overall timing. For the document node
16.1087 + that corresponds to the current buffer, individual command timings
16.1088 + are shown as well. A double-click on a theory node or command moves
16.1089 + the editor focus to that particular source position.
16.1090 +
16.1091 + It is also possible to reveal individual timing information via some
16.1092 + tooltip for the corresponding command keyword, using the technique
16.1093 + of mouse hovering with @{verbatim CONTROL}/@{verbatim COMMAND}
16.1094 + modifier key as explained in \secref{sec:tooltips-hyperlinks}.
16.1095 + Actual display of timing depends on the global option
16.1096 + @{system_option jedit_timing_threshold}, which can be configured in
16.1097 + "Plugin Options / Isabelle / General".
16.1098 +
16.1099 + \medskip The \emph{Monitor} panel provides a general impression of
16.1100 + recent activity of the farm of worker threads in Isabelle/ML. Its
16.1101 + display is continuously updated according to @{system_option
16.1102 + editor_chart_delay}. Note that the painting of the chart takes
16.1103 + considerable runtime itself --- on the Java Virtual Machine that
16.1104 + runs Isabelle/Scala, not Isabelle/ML. Internally, the
16.1105 + Isabelle/Scala module @{verbatim isabelle.ML_Statistics} provides
16.1106 + further access to statistics of Isabelle/ML. *}
16.1107 +
16.1108 +
16.1109 +section {* Isabelle/Scala console *}
16.1110 +
16.1111 +text {* The \emph{Console} plugin of jEdit manages various shells
16.1112 + (command interpreters), e.g.\ \emph{BeanShell}, which is the
16.1113 + official jEdit scripting language, and the cross-platform
16.1114 + \emph{System} shell. Thus the console provides similar
16.1115 + functionality than the special buffers @{verbatim "*scratch*"} and
16.1116 + @{verbatim "*shell*"} in Emacs.
16.1117 +
16.1118 + Isabelle/jEdit extends the repertoire of the console by
16.1119 + \emph{Scala}, which is the regular Scala toplevel loop running
16.1120 + inside the \emph{same} JVM process as Isabelle/jEdit itself. This
16.1121 + means the Scala command interpreter has access to the JVM name space
16.1122 + and state of the running Prover IDE application: the main entry
16.1123 + points are @{verbatim view} (the current editor view of jEdit) and
16.1124 + @{verbatim PIDE} (the Isabelle/jEdit plugin object).
16.1125 +
16.1126 + For example, the subsequent Scala snippet gets the PIDE document
16.1127 + model of the current buffer within the current editor view:
16.1128 +
16.1129 + \begin{center}
16.1130 + @{verbatim "PIDE.document_model(view.getBuffer).get"}
16.1131 + \end{center}
16.1132 +
16.1133 + This helps to explore Isabelle/Scala functionality interactively.
16.1134 + Some care is required to avoid interference with the internals of
16.1135 + the running application, especially in production use. *}
16.1136 +
16.1137 +
16.1138 +section {* Low-level output *}
16.1139 +
16.1140 +text {* Prover output is normally shown directly in the main text area
16.1141 + or secondary \emph{Output} panels, as explained in
16.1142 + \secref{sec:prover-output}.
16.1143 +
16.1144 + Beyond this, it is occasionally useful to inspect low-level output
16.1145 + channels via some of the following additional panels:
16.1146 +
16.1147 + \begin{itemize}
16.1148 +
16.1149 + \item \emph{Protocol} shows internal messages between the
16.1150 + Isabelle/Scala and Isabelle/ML side of the PIDE editing protocol.
16.1151 + Recording of messages starts with the first activation of the
16.1152 + corresponding dockable window; earlier messages are lost.
16.1153 +
16.1154 + Actual display of protocol messages causes considerable slowdown, so
16.1155 + it is important to undock all \emph{Protocol} panels for production
16.1156 + work.
16.1157 +
16.1158 + \item \emph{Raw Output} shows chunks of text from the @{verbatim
16.1159 + stdout} and @{verbatim stderr} channels of the prover process.
16.1160 + Recording of output starts with the first activation of the
16.1161 + corresponding dockable window; earlier output is lost.
16.1162 +
16.1163 + The implicit stateful nature of physical I/O channels makes it
16.1164 + difficult to relate raw output to the actual command from where it
16.1165 + was originating. Parallel execution may add to the confusion.
16.1166 + Peeking at physical process I/O is only the last resort to diagnose
16.1167 + problems with tools that are not fully PIDE compliant.
16.1168 +
16.1169 + Under normal circumstances, prover output always works via managed
16.1170 + message channels (corresponding to @{ML writeln}, @{ML warning},
16.1171 + @{ML error} etc.\ in Isabelle/ML), which are displayed by regular
16.1172 + means within the document model (\secref{sec:prover-output}).
16.1173 +
16.1174 + \item \emph{Syslog} shows system messages that might be relevant to
16.1175 + diagnose problems with the startup or shutdown phase of the prover
16.1176 + process; this also includes raw output on @{verbatim stderr}.
16.1177 +
16.1178 + A limited amount of syslog messages are buffered, independently of
16.1179 + the docking state of the \emph{Syslog} panel. This allows to
16.1180 + diagnose serious problems with Isabelle/PIDE process management,
16.1181 + outside of the actual protocol layer.
16.1182 +
16.1183 + Under normal situations, such low-level system output can be
16.1184 + ignored.
16.1185 +
16.1186 + \end{itemize}
16.1187 +*}
16.1188 +
16.1189 +
16.1190 +chapter {* Known problems and workarounds \label{sec:problems} *}
16.1191
16.1192 text {*
16.1193 \begin{itemize}
16.1194
16.1195 + \item \textbf{Problem:} Lack of dependency management for auxiliary files
16.1196 + that contribute to a theory (e.g.\ @{command ML_file}).
16.1197 +
16.1198 + \textbf{Workaround:} Re-load files manually within the prover, by
16.1199 + editing corresponding command in the text.
16.1200 +
16.1201 + \item \textbf{Problem:} Odd behavior of some diagnostic commands with
16.1202 + global side-effects, like writing a physical file.
16.1203 +
16.1204 + \textbf{Workaround:} Copy / paste complete command text from
16.1205 + elsewhere, or discontinue continuous checking temporarily.
16.1206 +
16.1207 + \item \textbf{Problem:} No way to delete document nodes from the overall
16.1208 + collection of theories.
16.1209 +
16.1210 + \textbf{Workaround:} Ignore unused files. Restart whole
16.1211 + Isabelle/jEdit session in worst-case situation.
16.1212 +
16.1213 \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
16.1214 @{verbatim "C+MINUS"} for adjusting the editor font size depend on
16.1215 platform details and national keyboards.
16.1216
16.1217 - \textbf{Workaround:} Use numeric keypad or rebind keys in the
16.1218 - jEdit Shortcuts options dialog.
16.1219 + \textbf{Workaround:} Rebind keys via \emph{Global Options /
16.1220 + Shortcuts}.
16.1221
16.1222 - \item \textbf{Problem:} Lack of dependency management for auxiliary files
16.1223 - that contribute to a theory (e.g.\ @{command ML_file}).
16.1224 + \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
16.1225 + "COMMAND+COMMA"} for application \emph{Preferences} is in conflict
16.1226 + with the jEdit default shortcut for \emph{Incremental Search Bar}
16.1227 + (action @{verbatim "quick-search"}).
16.1228
16.1229 - \textbf{Workaround:} Re-load files manually within the prover.
16.1230 + \textbf{Workaround:} Rebind key via \emph{Global Options /
16.1231 + Shortcuts} according to national keyboard, e.g.\ @{verbatim
16.1232 + "COMMAND+SLASH"} on English ones.
16.1233
16.1234 - \item \textbf{Problem:} Odd behavior of some diagnostic commands with
16.1235 - global side-effects, like writing a physical file.
16.1236 + \item \textbf{Problem:} Mac OS X system fonts sometimes lead to
16.1237 + character drop-outs in the main text area.
16.1238
16.1239 - \textbf{Workaround:} Avoid such commands.
16.1240 + \textbf{Workaround:} Use the default @{verbatim IsabelleText} font.
16.1241 + (Do not install that font on the system.)
16.1242
16.1243 - \item \textbf{Problem:} No way to delete document nodes from the overall
16.1244 - collection of theories.
16.1245 -
16.1246 - \textbf{Workaround:} Restart whole Isabelle/jEdit session in worst-case
16.1247 - situation.
16.1248 -
16.1249 - \item \textbf{Problem:} Linux: some desktop environments with extreme
16.1250 - animation effects may disrupt Java 7 window placement and/or keyboard
16.1251 - focus.
16.1252 -
16.1253 - \textbf{Workaround:} Disable such effects.
16.1254 -
16.1255 - \item \textbf{Problem:} Linux: some X11 input methods such as IBus tend
16.1256 - to disrupt key event handling of Java/Swing.
16.1257 + \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
16.1258 + tend to disrupt key event handling of Java/AWT/Swing.
16.1259
16.1260 \textbf{Workaround:} Do not use input methods, reset the environment
16.1261 variable @{verbatim XMODIFIERS} within Isabelle settings (default in
16.1262 Isabelle2013-1).
16.1263
16.1264 - \item \textbf{Problem:} Linux: some X11 window managers that are not
16.1265 - ``re-parenting'' cause problems with additional windows opened by the Java
16.1266 - VM. This affects either historic or neo-minimalistic window managers like
16.1267 - ``@{verbatim awesome}'' or ``@{verbatim xmonad}''.
16.1268 + \item \textbf{Problem:} Some Linux / X11 window managers that are
16.1269 + not ``re-parenting'' cause problems with additional windows opened
16.1270 + by Java. This affects either historic or neo-minimalistic window
16.1271 + managers like @{verbatim awesome} or @{verbatim xmonad}.
16.1272
16.1273 \textbf{Workaround:} Use regular re-parenting window manager.
16.1274
16.1275 - \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
16.1276 - "COMMAND+COMMA"} for Preferences is in conflict with the jEdit default
16.1277 - binding for @{verbatim "quick-search"}.
16.1278 + \item \textbf{Problem:} Recent forks of Linux / X11 window managers
16.1279 + and desktop environments (variants of Gnome) disrupt the handling of
16.1280 + menu popups and mouse positions of Java/AWT/Swing.
16.1281
16.1282 - \textbf{Workaround:} Remap in jEdit manually according to national
16.1283 - keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
16.1284 + \textbf{Workaround:} Use mainstream versions of Linux desktops.
16.1285
16.1286 - \item \textbf{Problem:} Mac OS X: Java 7 is officially supported on Lion
16.1287 - and Mountain Lion, but not Snow Leopard. It usually works on the latter,
16.1288 - although with a small risk of instabilities.
16.1289 + \item \textbf{Problem:} Full-screen mode via jEdit action @{verbatim
16.1290 + "toggle-full-screen"} (default shortcut @{verbatim F11}) works on
16.1291 + Windows, but not on Mac OS X or various Linux / X11 window managers.
16.1292
16.1293 - \textbf{Workaround:} Update to OS X Mountain Lion, or later.
16.1294 + \textbf{Workaround:} Use native full-screen control of the window
16.1295 + manager (notably on Mac OS X).
16.1296 +
16.1297 + \item \textbf{Problem:} Full-screen mode and dockable windows in
16.1298 + \emph{floating} state may lead to confusion about window placement
16.1299 + (depending on platform characteristics).
16.1300 +
16.1301 + \textbf{Workaround:} Avoid this combination.
16.1302
16.1303 \end{itemize}
16.1304 *}
17.1 Binary file src/Doc/JEdit/document/auto-tools.png has changed
18.1 Binary file src/Doc/JEdit/document/find.png has changed
19.1 Binary file src/Doc/JEdit/document/output.png has changed
20.1 Binary file src/Doc/JEdit/document/popup1.png has changed
21.1 Binary file src/Doc/JEdit/document/popup2.png has changed
22.1 --- a/src/Doc/JEdit/document/root.tex Mon Nov 11 18:25:13 2013 +0100
22.2 +++ b/src/Doc/JEdit/document/root.tex Mon Nov 11 18:37:56 2013 +0100
22.3 @@ -57,7 +57,7 @@
22.4 Research and implementation of concepts around PIDE and Isabelle/jEdit has
22.5 started around 2008 and was kindly supported by:
22.6 \begin{itemize}
22.7 -\item TU M\"unchen \url{http://in.tum.de}
22.8 +\item TU M\"unchen \url{http://www.in.tum.de}
22.9 \item BMBF \url{http://www.bmbf.de}
22.10 \item Universit\'e Paris-Sud \url{http://www.u-psud.fr}
22.11 \item Digiteo \url{http://www.digiteo.fr}
22.12 @@ -65,7 +65,10 @@
22.13 \end{itemize}
22.14
22.15
22.16 -\pagenumbering{roman} \tableofcontents \clearfirst
22.17 +\pagenumbering{roman}
22.18 +\tableofcontents
22.19 +\listoffigures
22.20 +\clearfirst
22.21
22.22 \input{JEdit.tex}
22.23
23.1 Binary file src/Doc/JEdit/document/sledgehammer.png has changed
24.1 --- a/src/Doc/ROOT Mon Nov 11 18:25:13 2013 +0100
24.2 +++ b/src/Doc/ROOT Mon Nov 11 18:37:56 2013 +0100
24.3 @@ -143,21 +143,24 @@
24.4 "document/showsymbols"
24.5 "document/style.sty"
24.6
24.7 -session JEdit (doc) in "JEdit" = Pure +
24.8 +session JEdit (doc) in "JEdit" = HOL +
24.9 options [document_variants = "jedit", thy_output_source]
24.10 theories
24.11 JEdit
24.12 files
24.13 + "../IsarRef/document/style.sty"
24.14 + "../extra.sty"
24.15 + "../iman.sty"
24.16 + "../isar.sty"
24.17 + "../manual.bib"
24.18 + "../pdfsetup.sty"
24.19 "../prepare_document"
24.20 - "../IsarRef/document/style.sty"
24.21 - "../pdfsetup.sty"
24.22 - "../iman.sty"
24.23 - "../extra.sty"
24.24 - "../isar.sty"
24.25 "../ttbox.sty"
24.26 "../underscore.sty"
24.27 - "../manual.bib"
24.28 "document/build"
24.29 + "document/isabelle-jedit.png"
24.30 + "document/popup1.png"
24.31 + "document/popup2.png"
24.32 "document/root.tex"
24.33
24.34 session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
25.1 --- a/src/Doc/System/Sessions.thy Mon Nov 11 18:25:13 2013 +0100
25.2 +++ b/src/Doc/System/Sessions.thy Mon Nov 11 18:37:56 2013 +0100
25.3 @@ -249,6 +249,8 @@
25.4 \secref{sec:tool-build}.
25.5
25.6 Option @{verbatim "-g"} prints the value of the given option.
25.7 + Option @{verbatim "-l"} lists all options with their declaration and
25.8 + current value.
25.9
25.10 Option @{verbatim "-x"} specifies a file to export the result in
25.11 YXML format, instead of printing it in human-readable form.
26.1 --- a/src/Doc/antiquote_setup.ML Mon Nov 11 18:25:13 2013 +0100
26.2 +++ b/src/Doc/antiquote_setup.ML Mon Nov 11 18:37:56 2013 +0100
26.3 @@ -47,6 +47,22 @@
26.4 (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
26.5
26.6
26.7 +(* unchecked file *)
26.8 +
26.9 +val file_unchecked_setup =
26.10 + Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
26.11 + (fn {context = ctxt, ...} => fn (name, pos) =>
26.12 + let
26.13 + val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt);
26.14 + val path = Path.append dir (Path.explode name);
26.15 + val _ = Position.report pos (Markup.path name);
26.16 + in
26.17 + space_explode "/" name
26.18 + |> map Thy_Output.verb_text
26.19 + |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
26.20 + end);
26.21 +
26.22 +
26.23 (* ML text *)
26.24
26.25 local
26.26 @@ -233,6 +249,7 @@
26.27
26.28 val setup =
26.29 verbatim_setup #>
26.30 + file_unchecked_setup #>
26.31 index_ml_setup #>
26.32 named_thms_setup #>
26.33 thy_file_setup #>
27.1 --- a/src/Doc/manual.bib Mon Nov 11 18:25:13 2013 +0100
27.2 +++ b/src/Doc/manual.bib Mon Nov 11 18:37:56 2013 +0100
27.3 @@ -794,6 +794,16 @@
27.4 pages = {205-216},
27.5 publisher = {Elsevier}}
27.6
27.7 +@inproceedings{Huffman-Kuncar:2013:lifting_transfer,
27.8 + author = {Brian Huffman and Ond\v{r}ej Kun\v{c}ar},
27.9 + title = {{Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL}},
27.10 + booktitle = {Certified Programs and Proofs (CPP 2013)},
27.11 + year = 2013,
27.12 + publisher = Springer,
27.13 + series = {Lecture Notes in Computer Science},
27.14 + volume = {8307},
27.15 +}
27.16 +
27.17 @Book{Huth-Ryan-book,
27.18 author = {Michael Huth and Mark Ryan},
27.19 title = {Logic in Computer Science. Modelling and reasoning about systems},
27.20 @@ -1683,13 +1693,15 @@
27.21 year = 2007,
27.22 publisher = Springer}
27.23
27.24 -@unpublished{traytel-berghofer-nipkow-2011,
27.25 - author = {D. Traytel and S. Berghofer and T. Nipkow},
27.26 - title = {Extending Hindley-Milner Type Inference with Coercive
27.27 - Subtyping (long version)},
27.28 +@inproceedings{traytel-berghofer-nipkow-2011,
27.29 + author = {Dmitriy Traytel and Stefan Berghofer and Tobias Nipkow},
27.30 + title = {{Extending Hindley-Milner Type Inference with Coercive Structural Subtyping}},
27.31 year = 2011,
27.32 - note = {Submitted,
27.33 - \url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
27.34 + editor = {Hongseok Yang},
27.35 + booktitle = "APLAS 2011",
27.36 + series = LNCS,
27.37 + volume = {7078},
27.38 + pages = "89--104"}
27.39
27.40 @inproceedings{traytel-et-al-2012,
27.41 author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette",
28.1 --- a/src/HOL/BNF/Tools/coinduction.ML Mon Nov 11 18:25:13 2013 +0100
28.2 +++ b/src/HOL/BNF/Tools/coinduction.ML Mon Nov 11 18:37:56 2013 +0100
28.3 @@ -75,7 +75,7 @@
28.4 map3 (fn name => fn T => fn (_, rhs) =>
28.5 HOLogic.mk_eq (Free (name, T), rhs))
28.6 names Ts raw_eqs;
28.7 - val phi = map (HOLogic.dest_Trueprop o prop_of) prems @ eqs
28.8 + val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
28.9 |> try (Library.foldr1 HOLogic.mk_conj)
28.10 |> the_default @{term True}
28.11 |> list_exists_free vars
28.12 @@ -89,8 +89,8 @@
28.13 HEADGOAL (EVERY' [rtac thm,
28.14 EVERY' (map (fn var =>
28.15 rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
28.16 - EVERY' (map (fn prem => rtac conjI THEN' rtac prem) prems),
28.17 - CONJ_WRAP' (K (rtac refl)) eqs,
28.18 + if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
28.19 + else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
28.20 K (ALLGOALS_SKIP skip
28.21 (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
28.22 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
28.23 @@ -100,11 +100,11 @@
28.24 let
28.25 val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
28.26 val inv_thms = init @ [last];
28.27 - val eqs = drop p inv_thms;
28.28 + val eqs = take e inv_thms;
28.29 fun is_local_var t =
28.30 member (fn (t, (_, t')) => t aconv (term_of t')) params t;
28.31 val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
28.32 - val assms = assms' @ take p inv_thms
28.33 + val assms = assms' @ drop e inv_thms
28.34 in
28.35 HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
28.36 unfold_thms_tac ctxt eqs
29.1 --- a/src/HOL/Quotient_Examples/FSet.thy Mon Nov 11 18:25:13 2013 +0100
29.2 +++ b/src/HOL/Quotient_Examples/FSet.thy Mon Nov 11 18:37:56 2013 +0100
29.3 @@ -5,6 +5,13 @@
29.4 Type of finite sets.
29.5 *)
29.6
29.7 +(********************************************************************
29.8 + WARNING: There is a formalization of 'a fset as a subtype of sets in
29.9 + HOL/Library/FSet.thy using Lifting/Transfer. The user should use
29.10 + that file rather than this file unless there are some very specific
29.11 + reasons.
29.12 +*********************************************************************)
29.13 +
29.14 theory FSet
29.15 imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List"
29.16 begin
30.1 --- a/src/HOL/String.thy Mon Nov 11 18:25:13 2013 +0100
30.2 +++ b/src/HOL/String.thy Mon Nov 11 18:37:56 2013 +0100
30.3 @@ -425,8 +425,13 @@
30.4 definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
30.5 where [simp, code del]: "abort _ f = f ()"
30.6
30.7 +lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
30.8 +by simp
30.9 +
30.10 setup {* Sign.map_naming Name_Space.parent_path *}
30.11
30.12 +setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *}
30.13 +
30.14 code_printing constant Code.abort \<rightharpoonup>
30.15 (SML) "!(raise/ Fail/ _)"
30.16 and (OCaml) "failwith"
31.1 --- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Nov 11 18:25:13 2013 +0100
31.2 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Nov 11 18:37:56 2013 +0100
31.3 @@ -50,7 +50,15 @@
31.4 SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
31.5 handle ERROR _ => NONE
31.6
31.7 -(* Generation of a transfer rule *)
31.8 +(*
31.9 + Generates a parametrized transfer rule.
31.10 + transfer_rule - of the form T t f
31.11 + parametric_transfer_rule - of the form par_R t' t
31.12 +
31.13 + Result: par_T t' f, after substituing op= for relations in par_T that relate
31.14 + a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
31.15 + using Lifting_Term.merge_transfer_relations
31.16 +*)
31.17
31.18 fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
31.19 let
31.20 @@ -400,6 +408,7 @@
31.21 rhs - a term representing the new constant on the raw level
31.22 rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'),
31.23 i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
31.24 + par_thms - a parametricity theorem for rhs
31.25 *)
31.26
31.27 fun add_lift_def var qty rhs rsp_thm par_thms lthy =
32.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 11 18:25:13 2013 +0100
32.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 11 18:37:56 2013 +0100
32.3 @@ -477,6 +477,7 @@
32.4 quot_thm - a quotient theorem (Quotient R Abs Rep T)
32.5 opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
32.6 (in the form "reflp R")
32.7 + opt_par_thm - a parametricity theorem for R
32.8 *)
32.9
32.10 fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
32.11 @@ -758,7 +759,11 @@
32.12 fun setup_typedef () =
32.13 case opt_reflp_xthm of
32.14 SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
32.15 - | NONE => setup_by_typedef_thm gen_code input_thm lthy
32.16 + | NONE => (
32.17 + case opt_par_xthm of
32.18 + SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
32.19 + | NONE => setup_by_typedef_thm gen_code input_thm lthy
32.20 + )
32.21 in
32.22 case input_term of
32.23 (Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
32.24 @@ -848,6 +853,10 @@
32.25 @ (map (Pretty.string_of o Pretty.item o single) errs)))
32.26 end
32.27
32.28 +(*
32.29 + Registers the data in qinfo in the Lifting infrastructure.
32.30 +*)
32.31 +
32.32 fun lifting_restore qinfo ctxt =
32.33 let
32.34 val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
33.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Nov 11 18:25:13 2013 +0100
33.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Nov 11 18:37:56 2013 +0100
33.3 @@ -289,9 +289,17 @@
33.4 quot_thm
33.5 end
33.6
33.7 +(*
33.8 + Computes the composed abstraction function for rty and qty.
33.9 +*)
33.10 +
33.11 fun abs_fun ctxt (rty, qty) =
33.12 quot_thm_abs (prove_quot_thm ctxt (rty, qty))
33.13
33.14 +(*
33.15 + Computes the composed equivalence relation for rty and qty.
33.16 +*)
33.17 +
33.18 fun equiv_relation ctxt (rty, qty) =
33.19 quot_thm_rel (prove_quot_thm ctxt (rty, qty))
33.20
33.21 @@ -324,6 +332,16 @@
33.22 end
33.23 end
33.24
33.25 +(*
33.26 + For the given type, it proves a composed Quotient map theorem, where for each type variable
33.27 + extra Quotient assumption is generated. E.g., for 'a list it generates exactly
33.28 + the Quotient map theorem for the list type. The function generalizes this for the whole
33.29 + type universe. New fresh variables in the assumptions are fixed in the returned context.
33.30 +
33.31 + Returns: the composed Quotient map theorem and list mapping each type variable in ty
33.32 + to the corresponding assumption in the returned theorem.
33.33 +*)
33.34 +
33.35 fun prove_param_quot_thm ctxt ty =
33.36 let
33.37 fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) =
33.38 @@ -360,6 +378,13 @@
33.39 end
33.40 handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg)
33.41
33.42 +(*
33.43 + It computes a parametrized relator for the given type ty. E.g., for 'a dlist:
33.44 + list_all2 ?R OO cr_dlist with parameters [?R].
33.45 +
33.46 + Returns: the definitional term and list of parameters (relations).
33.47 +*)
33.48 +
33.49 fun generate_parametrized_relator ctxt ty =
33.50 let
33.51 val orig_ctxt = ctxt
33.52 @@ -412,6 +437,15 @@
33.53 map_interrupt' f l []
33.54 end
33.55 in
33.56 +
33.57 + (*
33.58 + ctm - of the form (par_R OO T) t f, where par_R is a parametricity transfer relation for t
33.59 + and T is a transfer relation between t and f.
33.60 +
33.61 + The function merges par_R OO T using definitions of parametrized correspondence relations
33.62 + (e.g., rel_T R OO cr_T == pcr_T R).
33.63 + *)
33.64 +
33.65 fun merge_transfer_relations ctxt ctm =
33.66 let
33.67 val ctm = Thm.dest_arg ctm
33.68 @@ -488,6 +522,14 @@
33.69 handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
33.70 end
33.71
33.72 +(*
33.73 + It replaces cr_T by pcr_T op= in the transfer relation. For composed
33.74 + abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized
33.75 + correspondce relation does not exist, the original relation is kept.
33.76 +
33.77 + thm - a transfer rule
33.78 +*)
33.79 +
33.80 fun parametrize_transfer_rule ctxt thm =
33.81 let
33.82 fun parametrize_relation_conv ctm =
34.1 --- a/src/Pure/Concurrent/future.ML Mon Nov 11 18:25:13 2013 +0100
34.2 +++ b/src/Pure/Concurrent/future.ML Mon Nov 11 18:37:56 2013 +0100
34.3 @@ -68,6 +68,7 @@
34.4 val join_result: 'a future -> 'a Exn.result
34.5 val joins: 'a future list -> 'a list
34.6 val join: 'a future -> 'a
34.7 + val join_tasks: task list -> unit
34.8 val value_result: 'a Exn.result -> 'a future
34.9 val value: 'a -> 'a future
34.10 val cond_forks: params -> (unit -> 'a) list -> 'a future list
34.11 @@ -76,6 +77,7 @@
34.12 val promise: (unit -> unit) -> 'a future
34.13 val fulfill_result: 'a future -> 'a Exn.result -> unit
34.14 val fulfill: 'a future -> 'a -> unit
34.15 + val group_snapshot: group -> task list
34.16 val terminate: group -> unit
34.17 val shutdown: unit -> unit
34.18 end;
34.19 @@ -575,6 +577,14 @@
34.20 fun joins xs = Par_Exn.release_all (join_results xs);
34.21 fun join x = Exn.release (join_result x);
34.22
34.23 +fun join_tasks tasks =
34.24 + if null tasks then ()
34.25 + else
34.26 + (singleton o forks)
34.27 + {name = "join_tasks", group = SOME (new_group NONE),
34.28 + deps = tasks, pri = 0, interrupts = false} I
34.29 + |> join;
34.30 +
34.31
34.32 (* fast-path operations -- bypass task queue if possible *)
34.33
34.34 @@ -663,22 +673,20 @@
34.35 fun fulfill x res = fulfill_result x (Exn.Res res);
34.36
34.37
34.38 +(* group snapshot *)
34.39 +
34.40 +fun group_snapshot group =
34.41 + SYNCHRONIZED "group_snapshot" (fn () =>
34.42 + Task_Queue.group_tasks (! queue) group);
34.43 +
34.44 +
34.45 (* terminate *)
34.46
34.47 fun terminate group =
34.48 - let
34.49 - val tasks =
34.50 - SYNCHRONIZED "terminate" (fn () =>
34.51 - let val _ = cancel_group_unsynchronized group;
34.52 - in Task_Queue.group_tasks (! queue) group end);
34.53 - in
34.54 - if null tasks then ()
34.55 - else
34.56 - (singleton o forks)
34.57 - {name = "terminate", group = SOME (new_group NONE),
34.58 - deps = tasks, pri = 0, interrupts = false} I
34.59 - |> join
34.60 - end;
34.61 + SYNCHRONIZED "terminate" (fn () =>
34.62 + let val _ = cancel_group_unsynchronized group;
34.63 + in Task_Queue.group_tasks (! queue) group end)
34.64 + |> join_tasks;
34.65
34.66
34.67 (* shutdown *)
35.1 --- a/src/Pure/GUI/gui.scala Mon Nov 11 18:25:13 2013 +0100
35.2 +++ b/src/Pure/GUI/gui.scala Mon Nov 11 18:37:56 2013 +0100
35.3 @@ -168,10 +168,11 @@
35.4 def font_metrics(font: Font): LineMetrics =
35.5 font.getLineMetrics("", new FontRenderContext(null, false, false))
35.6
35.7 - def imitate_font(family: String, font: Font): Font =
35.8 + def imitate_font(family: String, font: Font, scale: Double = 1.0): Font =
35.9 {
35.10 val font1 = new Font(family, font.getStyle, font.getSize)
35.11 - font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
35.12 + val size = scale * (font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
35.13 + font1.deriveFont(size.round.toInt)
35.14 }
35.15
35.16 def transform_font(font: Font, transform: AffineTransform): Font =
36.1 --- a/src/Pure/GUI/system_dialog.scala Mon Nov 11 18:25:13 2013 +0100
36.2 +++ b/src/Pure/GUI/system_dialog.scala Mon Nov 11 18:37:56 2013 +0100
36.3 @@ -1,5 +1,4 @@
36.4 /* Title: Pure/GUI/system_dialog.scala
36.5 - Module: PIDE-GUI
36.6 Author: Makarius
36.7
36.8 Dialog for system processes, with optional output window.
37.1 --- a/src/Pure/General/socket_io.ML Mon Nov 11 18:25:13 2013 +0100
37.2 +++ b/src/Pure/General/socket_io.ML Mon Nov 11 18:37:56 2013 +0100
37.3 @@ -25,7 +25,7 @@
37.4 val rd =
37.5 BinPrimIO.RD {
37.6 name = name,
37.7 - chunkSize = Socket.Ctl.getRCVBUF socket,
37.8 + chunkSize = io_buffer_size,
37.9 readVec = SOME (fn n => Socket.recvVec (socket, n)),
37.10 readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
37.11 readVecNB = NONE,
37.12 @@ -44,7 +44,7 @@
37.13 val wr =
37.14 BinPrimIO.WR {
37.15 name = name,
37.16 - chunkSize = Socket.Ctl.getSNDBUF socket,
37.17 + chunkSize = io_buffer_size,
37.18 writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
37.19 writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
37.20 writeVecNB = NONE,
37.21 @@ -81,6 +81,7 @@
37.22 | _ => err ());
37.23 val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
37.24 val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
37.25 + val _ = INetSock.TCP.setNODELAY (socket, true);
37.26 in make_streams socket end;
37.27
37.28 end;
38.1 --- a/src/Pure/ML-Systems/polyml.ML Mon Nov 11 18:25:13 2013 +0100
38.2 +++ b/src/Pure/ML-Systems/polyml.ML Mon Nov 11 18:37:56 2013 +0100
38.3 @@ -51,6 +51,8 @@
38.4 val raw_explode = SML90.explode;
38.5 val implode = SML90.implode;
38.6
38.7 +val io_buffer_size = 4096;
38.8 +
38.9 fun quit () = exit 0;
38.10
38.11
39.1 --- a/src/Pure/ML-Systems/smlnj.ML Mon Nov 11 18:25:13 2013 +0100
39.2 +++ b/src/Pure/ML-Systems/smlnj.ML Mon Nov 11 18:37:56 2013 +0100
39.3 @@ -3,6 +3,7 @@
39.4 Compatibility file for Standard ML of New Jersey.
39.5 *)
39.6
39.7 +val io_buffer_size = 4096;
39.8 use "ML-Systems/proper_int.ML";
39.9
39.10 exception Interrupt;
40.1 --- a/src/Pure/PIDE/document.scala Mon Nov 11 18:25:13 2013 +0100
40.2 +++ b/src/Pure/PIDE/document.scala Mon Nov 11 18:37:56 2013 +0100
40.3 @@ -416,7 +416,7 @@
40.4 case Some(st) =>
40.5 val command = st.command
40.6 val node = version.nodes(command.node_name)
40.7 - Some((node, command))
40.8 + if (node.commands.contains(command)) Some((node, command)) else None
40.9 }
40.10
40.11 def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
41.1 --- a/src/Pure/PIDE/query_operation.scala Mon Nov 11 18:25:13 2013 +0100
41.2 +++ b/src/Pure/PIDE/query_operation.scala Mon Nov 11 18:37:56 2013 +0100
41.3 @@ -53,8 +53,12 @@
41.4
41.5 private def remove_overlay()
41.6 {
41.7 - current_location.foreach(command =>
41.8 - editor.remove_overlay(command, operation_name, instance :: current_query))
41.9 + current_location match {
41.10 + case None =>
41.11 + case Some(command) =>
41.12 + editor.remove_overlay(command, operation_name, instance :: current_query)
41.13 + editor.flush()
41.14 + }
41.15 }
41.16
41.17
41.18 @@ -129,10 +133,8 @@
41.19 if (current_status != new_status) {
41.20 current_status = new_status
41.21 consume_status(new_status)
41.22 - if (new_status == Query_Operation.Status.REMOVED) {
41.23 + if (new_status == Query_Operation.Status.REMOVED)
41.24 remove_overlay()
41.25 - editor.flush()
41.26 - }
41.27 }
41.28 }
41.29 }
41.30 @@ -153,13 +155,15 @@
41.31 remove_overlay()
41.32 reset_state()
41.33 consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
41.34 - editor.current_command(editor_context, snapshot) match {
41.35 - case Some(command) =>
41.36 - current_location = Some(command)
41.37 - current_query = query
41.38 - current_status = Query_Operation.Status.WAITING
41.39 - editor.insert_overlay(command, operation_name, instance :: query)
41.40 - case None =>
41.41 + if (!snapshot.is_outdated) {
41.42 + editor.current_command(editor_context, snapshot) match {
41.43 + case Some(command) =>
41.44 + current_location = Some(command)
41.45 + current_query = query
41.46 + current_status = Query_Operation.Status.WAITING
41.47 + editor.insert_overlay(command, operation_name, instance :: query)
41.48 + case None =>
41.49 + }
41.50 }
41.51 consume_status(current_status)
41.52 editor.flush()
41.53 @@ -206,5 +210,8 @@
41.54 def deactivate() {
41.55 editor.session.commands_changed -= main_actor
41.56 remove_overlay()
41.57 + reset_state()
41.58 + consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
41.59 + consume_status(current_status)
41.60 }
41.61 }
42.1 --- a/src/Pure/System/options.scala Mon Nov 11 18:25:13 2013 +0100
42.2 +++ b/src/Pure/System/options.scala Mon Nov 11 18:37:56 2013 +0100
42.3 @@ -162,7 +162,10 @@
42.4 {
42.5 override def toString: String = options.iterator.mkString("Options (", ",", ")")
42.6
42.7 - def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
42.8 + private def print_opt(opt: Options.Opt): String =
42.9 + if (opt.public) "public " + opt.print else opt.print
42.10 +
42.11 + def print: String = cat_lines(options.toList.sortBy(_._1).map(p => print_opt(p._2)))
42.12
42.13 def description(name: String): String = check_name(name).description
42.14
43.1 --- a/src/Pure/System/system_channel.ML Mon Nov 11 18:25:13 2013 +0100
43.2 +++ b/src/Pure/System/system_channel.ML Mon Nov 11 18:37:56 2013 +0100
43.3 @@ -68,7 +68,9 @@
43.4 in
43.5 System_Channel
43.6 {input_line = fn () => read_line in_stream,
43.7 - inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)),
43.8 + inputN = fn n =>
43.9 + if n = 0 then "" (*workaround for polyml-5.5.1 or earlier*)
43.10 + else Byte.bytesToString (BinIO.inputN (in_stream, n)),
43.11 output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
43.12 flush = fn () => BinIO.flushOut out_stream}
43.13 end;
44.1 --- a/src/Pure/System/system_channel.scala Mon Nov 11 18:25:13 2013 +0100
44.2 +++ b/src/Pure/System/system_channel.scala Mon Nov 11 18:37:56 2013 +0100
44.3 @@ -15,7 +15,7 @@
44.4
44.5 object System_Channel
44.6 {
44.7 - def apply(use_socket: Boolean = false): System_Channel =
44.8 + def apply(): System_Channel =
44.9 if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
44.10 }
44.11
44.12 @@ -86,6 +86,7 @@
44.13 def rendezvous(): (OutputStream, InputStream) =
44.14 {
44.15 val socket = server.accept
44.16 + socket.setTcpNoDelay(true)
44.17 (socket.getOutputStream, socket.getInputStream)
44.18 }
44.19
45.1 --- a/src/Pure/Thy/html.scala Mon Nov 11 18:25:13 2013 +0100
45.2 +++ b/src/Pure/Thy/html.scala Mon Nov 11 18:37:56 2013 +0100
45.3 @@ -1,4 +1,5 @@
45.4 /* Title: Pure/Thy/html.scala
45.5 + Module: PIDE-GUI
45.6 Author: Makarius
45.7
45.8 HTML presentation elements.
46.1 --- a/src/Pure/Thy/thy_info.ML Mon Nov 11 18:25:13 2013 +0100
46.2 +++ b/src/Pure/Thy/thy_info.ML Mon Nov 11 18:37:56 2013 +0100
46.3 @@ -177,9 +177,12 @@
46.4 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
46.5
46.6 fun join_theory (Result {theory, exec_id, ...}) =
46.7 - Exn.capture Thm.join_theory_proofs theory ::
46.8 - map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id));
46.9 -
46.10 + let
46.11 + (*toplevel proofs and diags*)
46.12 + val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
46.13 + (*fully nested proofs*)
46.14 + val res = Exn.capture Thm.join_theory_proofs theory;
46.15 + in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
46.16
46.17 datatype task =
46.18 Task of string list * (theory list -> result) |
46.19 @@ -236,7 +239,7 @@
46.20 val results3 = futures
46.21 |> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
46.22
46.23 - (* FIXME avoid global reset_futures (!??) *)
46.24 + (* FIXME avoid global Execution.reset (!??) *)
46.25 val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
46.26
46.27 val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
47.1 --- a/src/Pure/Tools/main.scala Mon Nov 11 18:25:13 2013 +0100
47.2 +++ b/src/Pure/Tools/main.scala Mon Nov 11 18:37:56 2013 +0100
47.3 @@ -225,11 +225,17 @@
47.4 val update =
47.5 {
47.6 val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
47.7 + val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
47.8 val upd =
47.9 if (Platform.is_windows)
47.10 - List("ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home), "INI_DIR" -> "")
47.11 + List(
47.12 + "ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home),
47.13 + "ISABELLE_HOME_USER" -> Isabelle_System.jvm_path(isabelle_home_user),
47.14 + "INI_DIR" -> "")
47.15 else
47.16 - List("ISABELLE_HOME" -> isabelle_home)
47.17 + List(
47.18 + "ISABELLE_HOME" -> isabelle_home,
47.19 + "ISABELLE_HOME_USER" -> isabelle_home_user)
47.20
47.21 (env0: Any) => {
47.22 val env = env0.asInstanceOf[java.util.Map[String, String]]
48.1 --- a/src/Tools/Code/code_target.ML Mon Nov 11 18:25:13 2013 +0100
48.2 +++ b/src/Tools/Code/code_target.ML Mon Nov 11 18:37:56 2013 +0100
48.3 @@ -639,12 +639,13 @@
48.4 val set_identifiers = gen_set_identifiers cert_name_decls;
48.5 val set_identifiers_cmd = gen_set_identifiers read_name_decls;
48.6
48.7 -fun add_module_alias_cmd target aliasses =
48.8 +fun add_module_alias_cmd target aliasses thy =
48.9 let
48.10 val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\"";
48.11 in
48.12 fold (fn (sym, name) => set_identifier
48.13 - (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))) aliasses
48.14 + (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name))))
48.15 + aliasses thy
48.16 end;
48.17
48.18
49.1 --- a/src/Tools/jEdit/etc/options Mon Nov 11 18:25:13 2013 +0100
49.2 +++ b/src/Tools/jEdit/etc/options Mon Nov 11 18:37:56 2013 +0100
49.3 @@ -42,6 +42,9 @@
49.4 public option jedit_completion_delay : real = 0.0
49.5 -- "delay for completion popup (seconds)"
49.6
49.7 +public option jedit_completion_dismiss_delay : real = 0.0
49.8 + -- "delay for dismissing obsolete completion popup (seconds)"
49.9 +
49.10 public option jedit_completion_immediate : bool = false
49.11 -- "insert unique completion immediately into buffer (if delay = 0)"
49.12
50.1 --- a/src/Tools/jEdit/etc/settings Mon Nov 11 18:25:13 2013 +0100
50.2 +++ b/src/Tools/jEdit/etc/settings Mon Nov 11 18:37:56 2013 +0100
50.3 @@ -7,7 +7,7 @@
50.4 #JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
50.5 JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
50.6 #JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
50.7 -JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dscala.repl.no-threads=true"
50.8 +JEDIT_SYSTEM_OPTIONS="-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dscala.repl.no-threads=true"
50.9
50.10 ISABELLE_JEDIT_OPTIONS=""
50.11
51.1 --- a/src/Tools/jEdit/src/completion_popup.scala Mon Nov 11 18:25:13 2013 +0100
51.2 +++ b/src/Tools/jEdit/src/completion_popup.scala Mon Nov 11 18:37:56 2013 +0100
51.3 @@ -488,11 +488,18 @@
51.4 list_view.requestFocus
51.5 }
51.6
51.7 + private val hide_popup_delay =
51.8 + Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
51.9 + popup.hide
51.10 + }
51.11 +
51.12 private def hide_popup()
51.13 {
51.14 - val had_focus = list_view.peer.isFocusOwner
51.15 - popup.hide
51.16 - if (had_focus) refocus()
51.17 + if (list_view.peer.isFocusOwner) refocus()
51.18 +
51.19 + if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero)
51.20 + popup.hide
51.21 + else hide_popup_delay.invoke()
51.22 }
51.23 }
51.24
52.1 --- a/src/Tools/jEdit/src/document_model.scala Mon Nov 11 18:25:13 2013 +0100
52.2 +++ b/src/Tools/jEdit/src/document_model.scala Mon Nov 11 18:37:56 2013 +0100
52.3 @@ -100,10 +100,11 @@
52.4 Swing_Thread.require()
52.5
52.6 if (Isabelle.continuous_checking) {
52.7 + val snapshot = this.snapshot()
52.8 Document.Node.Perspective(node_required, Text.Perspective(
52.9 for {
52.10 doc_view <- PIDE.document_views(buffer)
52.11 - range <- doc_view.perspective().ranges
52.12 + range <- doc_view.perspective(snapshot).ranges
52.13 } yield range), PIDE.editor.node_overlays(node_name))
52.14 }
52.15 else empty_perspective
53.1 --- a/src/Tools/jEdit/src/document_view.scala Mon Nov 11 18:25:13 2013 +0100
53.2 +++ b/src/Tools/jEdit/src/document_view.scala Mon Nov 11 18:37:56 2013 +0100
53.3 @@ -77,14 +77,25 @@
53.4
53.5 /* perspective */
53.6
53.7 - def perspective(): Text.Perspective =
53.8 + def perspective(snapshot: Document.Snapshot): Text.Perspective =
53.9 {
53.10 Swing_Thread.require()
53.11
53.12 - val active_caret =
53.13 - if (text_area.getView != null && text_area.getView.getTextArea == text_area)
53.14 - List(JEdit_Lib.point_range(model.buffer, text_area.getCaretPosition))
53.15 + val active_command =
53.16 + {
53.17 + val view = text_area.getView
53.18 + if (view != null && view.getTextArea == text_area) {
53.19 + PIDE.editor.current_command(view, snapshot) match {
53.20 + case Some(command) =>
53.21 + snapshot.node.command_start(command) match {
53.22 + case Some(start) => List(command.proper_range + start)
53.23 + case None => Nil
53.24 + }
53.25 + case None => Nil
53.26 + }
53.27 + }
53.28 else Nil
53.29 + }
53.30
53.31 val buffer_range = JEdit_Lib.buffer_range(model.buffer)
53.32 val visible_lines =
53.33 @@ -98,7 +109,7 @@
53.34 }
53.35 yield range).toList
53.36
53.37 - Text.Perspective(active_caret ::: visible_lines)
53.38 + Text.Perspective(active_command ::: visible_lines)
53.39 }
53.40
53.41 private def update_perspective = new TextAreaExtension
54.1 --- a/src/Tools/jEdit/src/find_dockable.scala Mon Nov 11 18:25:13 2013 +0100
54.2 +++ b/src/Tools/jEdit/src/find_dockable.scala Mon Nov 11 18:37:56 2013 +0100
54.3 @@ -105,7 +105,11 @@
54.4 }
54.5
54.6 private val query_label = new Label("Search criteria:") {
54.7 - tooltip = "Search criteria for find operation"
54.8 + tooltip =
54.9 + GUI.tooltip_lines(List(
54.10 + "Search criteria for find operation, e.g.",
54.11 + "",
54.12 + " \"_ = _\" \"op +\" name: Group -name: monoid"))
54.13 }
54.14
54.15 private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
54.16 @@ -117,7 +121,7 @@
54.17 { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
54.18 setColumns(40)
54.19 setToolTipText(query_label.tooltip)
54.20 - setFont(GUI.imitate_font(Rendering.font_family(), getFont))
54.21 + setFont(GUI.imitate_font(Rendering.font_family(), getFont, 1.2))
54.22 }
54.23
54.24 private case class Context_Entry(val name: String, val description: String)
55.1 --- a/src/Tools/jEdit/src/jEdit.props Mon Nov 11 18:25:13 2013 +0100
55.2 +++ b/src/Tools/jEdit/src/jEdit.props Mon Nov 11 18:37:56 2013 +0100
55.3 @@ -9,6 +9,7 @@
55.4 buffer.sidekick.keystroke-parse=false
55.5 buffer.tabSize=2
55.6 close-docking-area.shortcut2=C+e C+CIRCUMFLEX
55.7 +complete-word.shortcut=
55.8 console.dock-position=floating
55.9 console.encoding=UTF-8
55.10 console.font=IsabelleText
55.11 @@ -190,8 +191,8 @@
55.12 isabelle-sledgehammer.dock-position=bottom
55.13 isabelle-symbols.dock-position=bottom
55.14 isabelle-theories.dock-position=right
55.15 -isabelle.complete.label=Complete text
55.16 -isabelle.complete.shortcut=C+b
55.17 +isabelle.complete.label=Complete Isabelle text
55.18 +isabelle.complete.shortcut2=C+b
55.19 isabelle.control-bold.label=Control bold
55.20 isabelle.control-bold.shortcut=C+e RIGHT
55.21 isabelle.control-reset.label=Control reset
55.22 @@ -211,7 +212,6 @@
55.23 isabelle.increase-font-size2.shortcut=C+EQUALS
55.24 isabelle.reset-continuous-checking.label=Reset continuous checking
55.25 isabelle.reset-font-size.label=Reset font size
55.26 -isabelle.reset-font-size.shortcut=C+0
55.27 isabelle.reset-node-required.label=Reset node required
55.28 isabelle.set-continuous-checking.label=Set continuous checking
55.29 isabelle.set-node-required.label=Set node required
56.1 --- a/src/Tools/jEdit/src/jedit_editor.scala Mon Nov 11 18:25:13 2013 +0100
56.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Nov 11 18:37:56 2013 +0100
56.3 @@ -66,24 +66,21 @@
56.4 {
56.5 Swing_Thread.require()
56.6
56.7 - if (snapshot.is_outdated) None
56.8 - else {
56.9 - val text_area = view.getTextArea
56.10 - PIDE.document_view(text_area) match {
56.11 - case Some(doc_view) =>
56.12 - val node = snapshot.version.nodes(doc_view.model.node_name)
56.13 - val caret = text_area.getCaretPosition
56.14 - if (caret < text_area.getBuffer.getLength) {
56.15 - val caret_commands = node.command_range(caret)
56.16 - if (caret_commands.hasNext) {
56.17 - val (cmd0, _) = caret_commands.next
56.18 - node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
56.19 - }
56.20 - else None
56.21 + val text_area = view.getTextArea
56.22 + PIDE.document_view(text_area) match {
56.23 + case Some(doc_view) =>
56.24 + val node = snapshot.version.nodes(doc_view.model.node_name)
56.25 + val caret = snapshot.revert(text_area.getCaretPosition)
56.26 + if (caret < text_area.getBuffer.getLength) {
56.27 + val caret_commands = node.command_range(caret)
56.28 + if (caret_commands.hasNext) {
56.29 + val (cmd0, _) = caret_commands.next
56.30 + node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
56.31 }
56.32 - else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
56.33 - case None => None
56.34 - }
56.35 + else None
56.36 + }
56.37 + else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
56.38 + case None => None
56.39 }
56.40 }
56.41
57.1 --- a/src/Tools/jEdit/src/plugin.scala Mon Nov 11 18:25:13 2013 +0100
57.2 +++ b/src/Tools/jEdit/src/plugin.scala Mon Nov 11 18:37:56 2013 +0100
57.3 @@ -228,26 +228,6 @@
57.4 }
57.5
57.6
57.7 - /* Mac OS X application hooks */
57.8 -
57.9 - def handleQuit(): Boolean =
57.10 - {
57.11 - jEdit.exit(jEdit.getActiveView(), true)
57.12 - false
57.13 - }
57.14 -
57.15 - def handlePreferences()
57.16 - {
57.17 - CombinedOptions.combinedOptions(jEdit.getActiveView())
57.18 - }
57.19 -
57.20 - def handleAbout(): Boolean =
57.21 - {
57.22 - new AboutDialog(jEdit.getActiveView())
57.23 - true
57.24 - }
57.25 -
57.26 -
57.27 /* main plugin plumbing */
57.28
57.29 override def handleMessage(message: EBMessage)
58.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Nov 11 18:25:13 2013 +0100
58.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Nov 11 18:37:56 2013 +0100
58.3 @@ -115,13 +115,13 @@
58.4 deactivate()
58.5 hierarchy(tip) match {
58.6 case Some((old, _ :: rest)) =>
58.7 - old.foreach(_.hide_popup)
58.8 - tip.hide_popup
58.9 - stack = rest
58.10 rest match {
58.11 case top :: _ => top.request_focus
58.12 case Nil => JEdit_Lib.request_focus_view
58.13 }
58.14 + old.foreach(_.hide_popup)
58.15 + tip.hide_popup
58.16 + stack = rest
58.17 case _ =>
58.18 }
58.19 }
58.20 @@ -131,9 +131,9 @@
58.21 deactivate()
58.22 if (stack.isEmpty) false
58.23 else {
58.24 + JEdit_Lib.request_focus_view
58.25 stack.foreach(_.hide_popup)
58.26 stack = Nil
58.27 - JEdit_Lib.request_focus_view
58.28 true
58.29 }
58.30 }
59.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Nov 11 18:25:13 2013 +0100
59.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Nov 11 18:37:56 2013 +0100
59.3 @@ -136,7 +136,11 @@
59.4 }
59.5
59.6 private val provers_label = new Label("Provers:") {
59.7 - tooltip = "Automatic provers as space-separated list (e.g. \"e spass remote_vampire\")"
59.8 + tooltip =
59.9 + GUI.tooltip_lines(List(
59.10 + "Automatic provers as space-separated list, e.g.",
59.11 + "",
59.12 + " e spass remote_vampire"))
59.13 }
59.14
59.15 private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {