--- a/.hgtags Mon Nov 11 18:25:13 2013 +0100
+++ b/.hgtags Mon Nov 11 18:37:56 2013 +0100
@@ -26,3 +26,4 @@
76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1
21c42b095c841d1a7508c143d6b6e98d95dbfa69 Isabelle2012
d90218288d517942cfbc80a6b2654ecb22735e5c Isabelle2013
+9c1f2136532626c7cb5fae14a2aeac53be3aeb67 Isabelle2013-1
--- a/Admin/Linux/Isabelle Mon Nov 11 18:25:13 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Main Isabelle application wrapper.
-
-# dereference executable
-if [ -L "$0" ]; then
- TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
- exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
-fi
-
-
-# minimal Isabelle environment
-
-ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
-source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
-
-
-# main
-
-#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
-unset XMODIFIERS
-
-exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bin/java" \
- "-Disabelle.home=$ISABELLE_HOME" \
- {JAVA_ARGS} \
- -classpath "{CLASSPATH}" \
- isabelle.Main "$@"
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Linux/Isabelle.c Mon Nov 11 18:37:56 2013 +0100
@@ -0,0 +1,41 @@
+/* Author: Makarius
+
+Main Isabelle application executable.
+*/
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <sys/types.h>
+#include <unistd.h>
+
+
+static void fail(const char *msg)
+{
+ fprintf(stderr, "%s\n", msg);
+ exit(2);
+}
+
+
+int main(int argc, char *argv[])
+{
+ char **cmd_line = NULL;
+ int i = 0;
+
+ cmd_line = malloc(sizeof(char *) * (argc + 1));
+ if (cmd_line == NULL) fail("Failed to allocate command line");
+
+ cmd_line[0] = malloc(strlen(argv[0]) + 5);
+ if (cmd_line[0] == NULL) fail("Failed to allocate command line");
+
+ strcpy(cmd_line[0], argv[0]);
+ strcat(cmd_line[0], ".run");
+
+ for (i = 1; i < argc; i++) cmd_line[i] = argv[i];
+
+ cmd_line[argc] = NULL;
+
+ execvp(cmd_line[0], cmd_line);
+ fail("Failed to execute application script");
+}
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Linux/Isabelle.run Mon Nov 11 18:37:56 2013 +0100
@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Main Isabelle application script.
+
+# dereference executable
+if [ -L "$0" ]; then
+ TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+ exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
+fi
+
+
+# minimal Isabelle environment
+
+ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; pwd)"
+source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
+
+
+# main
+
+#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
+unset XMODIFIERS
+
+exec "$ISABELLE_HOME/contrib/jdk/${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}/bin/java" \
+ "-Disabelle.home=$ISABELLE_HOME" \
+ {JAVA_ARGS} \
+ -classpath "{CLASSPATH}" \
+ isabelle.Main "$@"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/Linux/build Mon Nov 11 18:37:56 2013 +0100
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+cc -static -m32 Isabelle.c -o Isabelle
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/bundled-linux Mon Nov 11 18:37:56 2013 +0100
@@ -0,0 +1,2 @@
+#additional components to be bundled for release
+linux_app-20131007
--- a/Admin/components/components.sha1 Mon Nov 11 18:25:13 2013 +0100
+++ b/Admin/components/components.sha1 Mon Nov 11 18:37:56 2013 +0100
@@ -38,16 +38,19 @@
87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz
c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz
65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz
+30ca171f745adf12b65c798c660ac77f9c0f9b4b jedit_build-20131106.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
5f95c96bb99927f3a026050f85bd056f37a9189e kodkodi-1.5.2.tar.gz
+377e36efb8608e6c828c7718d890e97fde2006a4 linux_app-20131007.tar.gz
0aab4f73ff7f5e36f33276547e10897e1e56fb1d macos_app-20130716.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
b3d776e6744f0cd2773d467bc2cfe1de3d1ca2fd polyml-5.5.0-3.tar.gz
1812e9fa6d163f63edb93e37d1217640a166cf3e polyml-5.5.0.tar.gz
+36f5b8224f484721749682a3655c796a55a2718d polyml-5.5.1-1.tar.gz
36f78f27291a9ceb13bf1120b62a45625afd44a6 polyml-5.5.1.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
--- a/Admin/components/main Mon Nov 11 18:25:13 2013 +0100
+++ b/Admin/components/main Mon Nov 11 18:37:56 2013 +0100
@@ -4,10 +4,10 @@
exec_process-1.0.3
Haskabelle-2013
jdk-7u40
-jedit_build-20130926
+jedit_build-20131106
jfreechart-1.0.14-1
kodkodi-1.5.2
-polyml-5.5.1
+polyml-5.5.1-1
scala-2.10.3
spass-3.8ds
z3-3.2
--- a/Admin/lib/Tools/makedist_bundle Mon Nov 11 18:25:13 2013 +0100
+++ b/Admin/lib/Tools/makedist_bundle Mon Nov 11 18:37:56 2013 +0100
@@ -160,10 +160,13 @@
LINUX_CLASSPATH="$LINUX_CLASSPATH:\\\$ISABELLE_HOME/$ENTRY"
fi
done
- cat "$ISABELLE_HOME/Admin/Linux/Isabelle" | \
- perl -p > "$ISABELLE_TARGET/$ISABELLE_NAME" \
+ cat "$ISABELLE_HOME/Admin/Linux/Isabelle.run" | \
+ perl -p > "$ISABELLE_TARGET/${ISABELLE_NAME}.run" \
-e "s,{JAVA_ARGS},$JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS,g; s,{CLASSPATH},$LINUX_CLASSPATH,;"
- chmod +x "$ISABELLE_TARGET/$ISABELLE_NAME"
+ chmod +x "$ISABELLE_TARGET/${ISABELLE_NAME}.run"
+
+ mv "$ISABELLE_TARGET/contrib/linux_app" "$TMP/."
+ cp "$TMP/linux_app/Isabelle" "$ISABELLE_TARGET/$ISABELLE_NAME"
;;
macos)
purge_contrib '-name "x86*-linux" -o -name "x86*-cygwin" -o -name "x86*-windows"'
--- a/CONTRIBUTORS Mon Nov 11 18:25:13 2013 +0100
+++ b/CONTRIBUTORS Mon Nov 11 18:37:56 2013 +0100
@@ -10,6 +10,12 @@
Contributions to Isabelle2013-1
-------------------------------
+* September 2013: Lars Noschinski, TUM
+ Conversion between function definitions as list of equations and
+ case expressions in HOL.
+ New library Simps_Case_Conv with commands case_of_simps,
+ simps_of_case.
+
* September 2013: Nik Sultana, University of Cambridge
Improvements to HOL/TPTP parser and import facilities.
--- a/NEWS Mon Nov 11 18:25:13 2013 +0100
+++ b/NEWS Mon Nov 11 18:37:56 2013 +0100
@@ -125,7 +125,10 @@
normal editing and checking process.
* Dockable window "Timing" provides an overview of relevant command
-timing information.
+timing information, depending on option jedit_timing_threshold. The
+same timing information is shown in the extended tooltip of the
+command keyword, when hovering the mouse over it while the CONTROL or
+COMMAND modifier is pressed.
* Improved dockable window "Theories": Continuous checking of proof
document (visible and required parts) may be controlled explicitly,
@@ -133,14 +136,22 @@
be marked explicitly as required and checked in full, using check box
or shortcut "C+e SPACE".
+* Improved completion mechanism, which is now managed by the
+Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle
+symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
+
+* Standard jEdit keyboard shortcut C+b complete-word is remapped to
+isabelle.complete for explicit completion in Isabelle sources.
+INCOMPATIBILITY wrt. jEdit defaults, may have to invent new shortcuts
+to resolve conflict.
+
+* Improved support of various "minor modes" for Isabelle NEWS,
+options, session ROOT etc., with completion and SideKick tree view.
+
* Strictly monotonic document update, without premature cancellation of
running transactions that are still needed: avoid reset/restart of
such command executions while editing.
-* Improved completion mechanism, which is now managed by the
-Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle
-symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
-
* Support for asynchronous print functions, as overlay to existing
document content.
@@ -148,12 +159,13 @@
toplevel theorem statements.
* Action isabelle.reset-font-size resets main text area font size
-according to Isabelle/Scala plugin option "jedit_font_reset_size"
-(cf. keyboard shortcut C+0).
+according to Isabelle/Scala plugin option "jedit_font_reset_size" (see
+also "Plugin Options / Isabelle / General"). It can be bound to some
+keyboard shortcut by the user (e.g. C+0 and/or C+NUMPAD0).
* File specifications in jEdit (e.g. file browser) may refer to
-$ISABELLE_HOME on all platforms. Discontinued obsolete
-$ISABELLE_HOME_WINDOWS variable.
+$ISABELLE_HOME and $ISABELLE_HOME_USER on all platforms. Discontinued
+obsolete $ISABELLE_HOME_WINDOWS variable.
* Improved support for Linux look-and-feel "GTK+", see also "Utilities
/ Global Options / Appearance".
@@ -250,7 +262,7 @@
* Lifting:
- parametrized correspondence relations are now supported:
- + parametricity theorems for the raw term can be specified in
+ + parametricity theorems for the raw term can be specified in
the command lift_definition, which allow us to generate stronger
transfer rules
+ setup_lifting generates stronger transfer rules if parametric
@@ -264,15 +276,15 @@
- ===> and --> are now local. The symbols can be introduced
by interpreting the locale lifting_syntax (typically in an
anonymous context)
- - Lifting/Transfer relevant parts of Library/Quotient_* are now in
+ - Lifting/Transfer relevant parts of Library/Quotient_* are now in
Main. Potential INCOMPATIBILITY
- new commands for restoring and deleting Lifting/Transfer context:
lifting_forget, lifting_update
- - the command print_quotmaps was renamed to print_quot_maps.
+ - the command print_quotmaps was renamed to print_quot_maps.
INCOMPATIBILITY
* Transfer:
- - better support for domains in Transfer: replace Domainp T
+ - better support for domains in Transfer: replace Domainp T
by the actual invariant in a transferred goal
- transfer rules can have as assumptions other transfer rules
- Experimental support for transferring from the raw level to the
--- a/etc/settings Mon Nov 11 18:25:13 2013 +0100
+++ b/etc/settings Mon Nov 11 18:37:56 2013 +0100
@@ -106,7 +106,7 @@
PDF_VIEWER="xdg-open"
;;
macos)
- PDF_VIEWER="open -W -n -a Safari"
+ PDF_VIEWER="open -W -n -F"
;;
windows)
PDF_VIEWER="cygstart"
--- a/src/Doc/IsarRef/Document_Preparation.thy Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy Mon Nov 11 18:37:56 2013 +0100
@@ -5,17 +5,17 @@
chapter {* Document preparation \label{ch:document-prep} *}
text {* Isabelle/Isar provides a simple document preparation system
- based on regular {PDF-\LaTeX} technology, with support for
- hyper-links and bookmarks within that format. Thus the results are
- well suited for WWW browsing and as printed copies.
+ based on {PDF-\LaTeX}, with support for hyperlinks and bookmarks
+ within that format. This allows to produce papers, books, theses
+ etc.\ from Isabelle theory sources.
{\LaTeX} output is generated while processing a \emph{session} in
batch mode, as explained in the \emph{The Isabelle System Manual}
\cite{isabelle-sys}. The main Isabelle tools to get started with
- document prepation are @{tool_ref mkroot} and @{tool_ref build}.
+ document preparation are @{tool_ref mkroot} and @{tool_ref build}.
- The Isabelle/HOL tutorial \cite{isabelle-hol-book} also covers
- theory presentation to some extent. *}
+ The classic Isabelle/HOL tutorial \cite{isabelle-hol-book} also
+ explains some aspects of theory presentation. *}
section {* Markup commands \label{sec:markup} *}
@@ -302,8 +302,8 @@
subsection {* General options *}
text {* The following options are available to tune the printed output
- of antiquotations. Note that many of these coincide with global ML
- flags of the same names.
+ of antiquotations. Note that many of these coincide with system and
+ configuration options of the same names.
\begin{description}
--- a/src/Doc/IsarRef/HOL_Specific.thy Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Mon Nov 11 18:37:56 2013 +0100
@@ -1259,17 +1259,18 @@
\end{matharray}
The quotient package defines a new quotient type given a raw type
- and a partial equivalence relation. It also includes automation for
- transporting definitions and theorems. It can automatically produce
- definitions and theorems on the quotient type, given the
- corresponding constants and facts on the raw type.
+ and a partial equivalence relation. The package also historically
+ includes automation for transporting definitions and theorems.
+ But most of this automation was superseded by the Lifting and Transfer
+ packages. The user should consider using these two new packages for
+ lifting definitions and transporting theorems.
@{rail "
@@{command (HOL) quotient_type} (spec);
spec: @{syntax typespec} @{syntax mixfix}? '=' \\
@{syntax type} '/' ('partial' ':')? @{syntax term} \\
- (@'morphisms' @{syntax name} @{syntax name})?;
+ (@'morphisms' @{syntax name} @{syntax name})? (@'parametric' @{syntax thmref})?;
"}
@{rail "
@@ -1289,9 +1290,9 @@
\begin{description}
- \item @{command (HOL) "quotient_type"} defines quotient types. The
+ \item @{command (HOL) "quotient_type"} defines a new quotient type @{text \<tau>}. The
injection from a quotient type to a raw type is called @{text
- rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)
+ rep_\<tau>}, its inverse @{text abs_\<tau>} unless explicit @{keyword (HOL)
"morphisms"} specification provides alternative names. @{command
(HOL) "quotient_type"} requires the user to prove that the relation
is an equivalence relation (predicate @{text equivp}), unless the
@@ -1300,6 +1301,22 @@
partial} is weaker in the sense that less things can be proved
automatically.
+ The command internally proves a Quotient theorem and sets up the Lifting
+ package by the command @{command (HOL) setup_lifting}. Thus the Lifting
+ and Transfer packages can be used also with quotient types defined by
+ @{command (HOL) "quotient_type"} without any extra set-up. The parametricity
+ theorem for the equivalence relation R can be provided as an extra argument
+ of the command and is passed to the corresponding internal call of @{command (HOL) setup_lifting}.
+ This theorem allows the Lifting package to generate a stronger transfer rule for equality.
+
+ \end{description}
+
+ The most of the rest of the package was superseded by the Lifting and Transfer
+ packages. The user should consider using these two new packages for
+ lifting definitions and transporting theorems.
+
+ \begin{description}
+
\item @{command (HOL) "quotient_definition"} defines a constant on
the quotient type.
@@ -1497,8 +1514,12 @@
@{method_def (HOL) "transfer"} & : & @{text method} \\
@{method_def (HOL) "transfer'"} & : & @{text method} \\
@{method_def (HOL) "transfer_prover"} & : & @{text method} \\
+ @{attribute_def (HOL) "Transfer.transferred"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "untransferred"} & : & @{text attribute} \\
@{attribute_def (HOL) "transfer_rule"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "transfer_domain_rule"} & : & @{text attribute} \\
@{attribute_def (HOL) "relator_eq"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "relator_domain"} & : & @{text attribute} \\
\end{matharray}
\begin{description}
@@ -1524,6 +1545,16 @@
rules. It should be applied after unfolding the constant
definitions.
+ \item @{attribute (HOL) "untransferred"} proves the same equivalent theorem
+ as @{method (HOL) "transfer"} internally does.
+
+ \item @{attribute (HOL) Transfer.transferred} works in the opposite
+ direction than @{method (HOL) "transfer'"}. E.g., given the transfer
+ relation @{text "ZN x n \<equiv> (x = int n)"}, corresponding transfer rules and the theorem
+ @{text "\<forall>x::int \<in> {0..}. x < x + 1"}, the attribute would prove
+ @{text "\<forall>n::nat. n < n + 1"}. The attribute is still in experimental
+ phase of development.
+
\item @{attribute (HOL) "transfer_rule"} attribute maintains a
collection of transfer rules, which relate constants at two
different types. Typical transfer rules may relate different type
@@ -1540,83 +1571,140 @@
@{text "bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct"}\\
@{text "\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (prod_rel A B)"}
+ \item @{attribute (HOL) "transfer_domain_rule"} attribute maintains a collection
+ of rules, which specify a domain of a transfer relation by a predicate.
+ E.g., given the transfer relation @{text "ZN x n \<equiv> (x = int n)"},
+ one can register the following transfer domain rule:
+ @{text "Domainp ZN = (\<lambda>x. x \<ge> 0)"}. The rules allow the package to produce
+ more readable transferred goals, e.g., when quantifiers are transferred.
+
\item @{attribute (HOL) relator_eq} attribute collects identity laws
for relators of various type constructors, e.g. @{text "list_all2
(op =) = (op =)"}. The @{method (HOL) transfer} method uses these
lemmas to infer transfer rules for non-polymorphic constants on
the fly.
+ \item @{attribute_def (HOL) "relator_domain"} attribute collects rules
+ describing domains of relators by predicators. E.g., @{text "Domainp A = P \<Longrightarrow>
+ Domainp (list_all2 A) = (list_all P)"}. This allows the package to lift transfer
+ domain rules through type constructors.
+
\end{description}
+ Theoretical background can be found in \cite{Huffman-Kuncar:2013:lifting_transfer}.
*}
section {* Lifting package *}
text {*
+ The Lifting package allows users to lift terms of the raw type to the abstract type, which is
+ a necessary step in building a library for an abstract type. Lifting defines a new constant
+ by combining coercion functions (Abs and Rep) with the raw term. It also proves an appropriate
+ transfer rule for the Transfer package and, if possible, an equation for the code generator.
+
+ The Lifting package provides two main commands: @{command (HOL) "setup_lifting"} for initializing
+ the package to work with a new type, and @{command (HOL) "lift_definition"} for lifting constants.
+ The Lifting package works with all four kinds of type abstraction: type copies, subtypes,
+ total quotients and partial quotients.
+
+ Theoretical background can be found in \cite{Huffman-Kuncar:2013:lifting_transfer}.
+
\begin{matharray}{rcl}
@{command_def (HOL) "setup_lifting"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
@{command_def (HOL) "lift_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
+ @{command_def (HOL) "lifting_forget"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
+ @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \<rightarrow> local_theory"}\\
@{command_def (HOL) "print_quot_maps"} & : & @{text "context \<rightarrow>"}\\
@{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
@{attribute_def (HOL) "quot_map"} & : & @{text attribute} \\
@{attribute_def (HOL) "invariant_commute"} & : & @{text attribute} \\
@{attribute_def (HOL) "reflexivity_rule"} & : & @{text attribute} \\
- @{attribute_def (HOL) "quot_del"} & : & @{text attribute}
+ @{attribute_def (HOL) "relator_mono"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "relator_distr"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "quot_del"} & : & @{text attribute} \\
+ @{attribute_def (HOL) "lifting_restore"} & : & @{text attribute} \\
\end{matharray}
@{rail "
@@{command (HOL) setup_lifting} ('(' 'no_code' ')')? \\
- @{syntax thmref} @{syntax thmref}?;
+ @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
"}
@{rail "
@@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type} @{syntax mixfix}? \\
- 'is' @{syntax term};
+ 'is' @{syntax term} (@'parametric' @{syntax thmref})?;
+ "}
+
+ @{rail "
+ @@{command (HOL) lifting_forget} @{syntax nameref};
+ "}
+
+ @{rail "
+ @@{command (HOL) lifting_update} @{syntax nameref};
+ "}
+
+ @{rail "
+ @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
"}
\begin{description}
\item @{command (HOL) "setup_lifting"} Sets up the Lifting package
- to work with a user-defined type. The user must provide either a
- quotient theorem @{text "Quotient R Abs Rep T"} or a
- type_definition theorem @{text "type_definition Rep Abs A"}. The
- package configures transfer rules for equality and quantifiers on
- the type, and sets up the @{command_def (HOL) "lift_definition"}
- command to work with the type. In the case of a quotient theorem,
- an optional theorem @{text "reflp R"} can be provided as a second
- argument. This allows the package to generate stronger transfer
- rules.
-
- @{command (HOL) "setup_lifting"} is called automatically if a
- quotient type is defined by the command @{command (HOL)
- "quotient_type"} from the Quotient package.
-
- If @{command (HOL) "setup_lifting"} is called with a
- type_definition theorem, the abstract type implicitly defined by
- the theorem is declared as an abstract type in the code
- generator. This allows @{command (HOL) "lift_definition"} to
- register (generated) code certificate theorems as abstract code
- equations in the code generator. The option @{text "no_code"}
- of the command @{command (HOL) "setup_lifting"} can turn off that
- behavior and causes that code certificate theorems generated by
- @{command (HOL) "lift_definition"} are not registered as abstract
- code equations.
-
- \item @{command (HOL) "lift_definition"} @{text "f :: \<tau> is t"}
+ to work with a user-defined type.
+ The command supports two modes. The first one is a low-level mode when
+ the user must provide as a first
+ argument of @{command (HOL) "setup_lifting"} a
+ quotient theorem @{text "Quotient R Abs Rep T"}. The
+ package configures a transfer rule for equality, a domain transfer
+ rules and sets up the @{command_def (HOL) "lift_definition"}
+ command to work with the abstract type. An optional theorem @{text "reflp R"}, which certifies that
+ the equivalence relation R is total,
+ can be provided as a second argument. This allows the package to generate stronger transfer
+ rules. And finally, the parametricity theorem for R can be provided as a third argument.
+ This allows the package to generate a stronger transfer rule for equality.
+
+ Users generally will not prove the @{text Quotient} theorem manually for
+ new types, as special commands exist to automate the process.
+
+ When a new subtype is defined by @{command (HOL) typedef}, @{command (HOL) "lift_definition"}
+ can be used in its
+ second mode, where only the type_definition theorem @{text "type_definition Rep Abs A"}
+ is used as an argument of the command. The command internally proves the corresponding
+ Quotient theorem and registers it with @{command (HOL) setup_lifting} using its first mode.
+
+ For quotients, the command @{command (HOL) quotient_type} can be used. The command defines
+ a new quotient type and similarly to the previous case, the corresponding Quotient theorem is proved
+ and registered by @{command (HOL) setup_lifting}.
+
+ The command @{command (HOL) "setup_lifting"} also sets up the code generator
+ for the new type. Later on, when a new constant is defined by @{command (HOL) "lift_definition"},
+ the Lifting package proves and registers a code equation (if there is one) for the new constant.
+ If the option @{text "no_code"} is specified, the Lifting package does not set up the code
+ generator and as a consequence no code equations involving an abstract type are registered
+ by @{command (HOL) "lift_definition"}.
+
+ \item @{command (HOL) "lift_definition"} @{text "f :: \<tau>"} @{keyword (HOL) "is"} @{text t}
Defines a new function @{text f} with an abstract type @{text \<tau>}
in terms of a corresponding operation @{text t} on a
- representation type. The term @{text t} doesn't have to be
- necessarily a constant but it can be any term.
-
- Users must discharge a respectfulness proof obligation when each
- constant is defined. For a type copy, i.e. a typedef with @{text
- UNIV}, the proof is discharged automatically. The obligation is
+ representation type. More formally, if @{text "t :: \<sigma>"}, then
+ the command builds a term @{text "F"} as a corresponding combination of abstraction
+ and representation functions such that @{text "F :: \<sigma> \<Rightarrow> \<tau>" } and
+ defines @{text f} is as @{text "f \<equiv> F t"}.
+ The term @{text t} does not have to be necessarily a constant but it can be any term.
+
+ The command opens a proof environment and the user must discharge
+ a respectfulness proof obligation. For a type copy, i.e., a typedef with @{text
+ UNIV}, the obligation is discharged automatically. The proof goal is
presented in a user-friendly, readable form. A respectfulness
theorem in the standard format @{text f.rsp} and a transfer rule
- @{text f.tranfer} for the Transfer package are generated by the
+ @{text f.transfer} for the Transfer package are generated by the
package.
+ The user can specify a parametricity theorem for @{text t} after the keyword
+ @{keyword "parametric"}, which allows the command
+ to generate a parametric transfer rule for @{text f}.
+
For each constant defined through trivial quotients (type copies or
subtypes) @{text f.rep_eq} is generated. The equation is a code certificate
that defines @{text f} using the representation function.
@@ -1625,14 +1713,36 @@
for total quotients. The equation defines @{text f} using
the abstraction function.
- Integration with code_abstype: For subtypes (e.g.,
+ Integration with [@{attribute code} abstract]: For subtypes (e.g.,
corresponding to a datatype invariant, such as dlist), @{command
(HOL) "lift_definition"} uses a code certificate theorem
@{text f.rep_eq} as a code equation.
- Integration with code: For total quotients, @{command
+ Integration with [@{attribute code} equation]: For total quotients, @{command
(HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
+ \item @{command (HOL) lifting_forget} and @{command (HOL) lifting_update}
+ These two commands serve for storing and deleting the set-up of
+ the Lifting package and corresponding transfer rules defined by this package.
+ This is useful for hiding of type construction details of an abstract type
+ when the construction is finished but it still allows additions to this construction
+ when this is later necessary.
+
+ Whenever the Lifting package is set up with a new abstract type @{text "\<tau>"} by
+ @{command_def (HOL) "lift_definition"}, the package defines a new bundle
+ that is called @{text "\<tau>.lifting"}. This bundle already includes set-up for the Lifting package.
+ The new transfer rules
+ introduced by @{command (HOL) "lift_definition"} can be stored in the bundle by
+ the command @{command (HOL) "lifting_update"} @{text "\<tau>.lifting"}.
+
+ The command @{command (HOL) "lifting_forget"} @{text "\<tau>.lifting"} deletes set-up of the Lifting
+ package
+ for @{text \<tau>} and deletes all the transfer rules that were introduced
+ by @{command (HOL) "lift_definition"} using @{text \<tau>} as an abstract type.
+
+ The stored set-up in a bundle can be reintroduced by the Isar commands for including a bundle
+ (@{command "include"}, @{keyword "includes"} and @{command "including"}).
+
\item @{command (HOL) "print_quot_maps"} prints stored quotient map
theorems.
@@ -1640,9 +1750,11 @@
theorems.
\item @{attribute (HOL) quot_map} registers a quotient map
- theorem. For examples see @{file
- "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
- files.
+ theorem. E.g., @{text "Quotient R Abs Rep T \<Longrightarrow>
+ Quotient (list_all2 R) (map Abs) (map Rep) (list_all2 T)"}.
+ For examples see @{file
+ "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
+ in the same directory.
\item @{attribute (HOL) invariant_commute} registers a theorem that
shows a relationship between the constant @{text
@@ -1650,20 +1762,54 @@
and a relator. Such theorems allows the package to hide @{text
Lifting.invariant} from a user in a user-readable form of a
respectfulness theorem. For examples see @{file
- "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
- files.
+ "~~/src/HOL/List.thy"} or Lifting_*.thy files in the same directory.
\item @{attribute (HOL) reflexivity_rule} registers a theorem that shows
- that a relator respects reflexivity and left-totality. For examples
- see @{file "~~/src/HOL/Library/Quotient_List.thy"} or other Quotient_*.thy
- The property is used in generation of abstraction function equations.
+ that a relator respects reflexivity, left-totality and left_uniqueness. For examples
+ see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"} or Lifting_*.thy files
+ in the same directory.
+ The property is used in a reflexivity prover, which is used for discharging respectfulness
+ theorems for type copies and also for discharging assumptions of abstraction function equations.
+
+ \item @{attribute (HOL) "relator_mono"} registers a property describing a monotonicity of a relator.
+ E.g., @{text "A \<le> B \<Longrightarrow> list_all2 A \<le> list_all2 B"}. For examples
+ see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
+ or Lifting_*.thy files in the same directory.
+ This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
+ when a parametricity theorem for the raw term is specified.
+
+ \item @{attribute (HOL) "relator_distr"} registers a property describing a distributivity
+ of the relation composition and a relator. E.g.,
+ @{text "list_all2 R \<circ>\<circ> list_all2 S = list_all2 (R \<circ>\<circ> S)"}.
+ This property is needed for proving a stronger transfer rule in @{command_def (HOL) "lift_definition"}
+ when a parametricity theorem for the raw term is specified.
+ When this equality does not hold unconditionally (e.g., for the function type), the user can specified
+ each direction separately and also register multiple theorems with different set of assumptions.
+ This attribute can be used only after the monotonicity property was already registered by
+ @{attribute (HOL) "relator_mono"}. For examples
+ see @{file "~~/src/HOL/List.thy"} or @{file "~~/src/HOL/Lifting.thy"}
+ or Lifting_*.thy files in the same directory.
\item @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem
from the Lifting infrastructure and thus de-register the corresponding quotient.
This effectively causes that @{command (HOL) lift_definition} will not
- do any lifting for the corresponding type. It serves mainly for hiding
- of type construction details when the construction is done. See for example
- @{file "~~/src/HOL/Int.thy"}.
+ do any lifting for the corresponding type. This attribute is rather used for low-level
+ manipulation with set-up of the Lifting package because @{command (HOL) lifting_forget} is
+ preferred for normal usage.
+
+ \item @{attribute (HOL) lifting_restore} @{text "Quotient_thm pcr_def pcr_cr_eq_thm"}
+ registers the Quotient theorem @{text Quotient_thm} in the Lifting infrastructure
+ and thus sets up lifting for an abstract type @{text \<tau>} (that is defined by @{text Quotient_thm}).
+ Optional theorems @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register
+ the parametrized
+ correspondence relation for @{text \<tau>}. E.g., for @{text "'a dlist"}, @{text pcr_def} is
+ @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ> cr_dlist"} and @{text pcr_cr_eq_thm} is
+ @{text "pcr_dlist op= = op="}.
+ This attribute is rather used for low-level
+ manipulation with set-up of the Lifting package because using of the bundle @{text \<tau>.lifting}
+ together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is
+ preferred for normal usage.
+
\end{description}
*}
--- a/src/Doc/JEdit/Base.thy Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/JEdit/Base.thy Mon Nov 11 18:37:56 2013 +0100
@@ -1,5 +1,5 @@
theory Base
-imports Pure
+imports Main
begin
ML_file "../antiquote_setup.ML"
--- a/src/Doc/JEdit/JEdit.thy Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy Mon Nov 11 18:37:56 2013 +0100
@@ -8,268 +8,1135 @@
section {* Concepts and terminology *}
-text {* FIXME
+text {* Isabelle/jEdit is a Prover IDE that integrates \emph{parallel
+ proof checking} \cite{Wenzel:2009,Wenzel:2013:ITP} with
+ \emph{asynchronous user interaction}
+ \cite{Wenzel:2010,Wenzel:2012:UITP-EPTCS}, based on a
+ document-oriented approach to \emph{continuous proof processing}
+ \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system
+ components are fit together in order to make this work. The main
+ building blocks are as follows.
-parallel proof checking \cite{Wenzel:2009} \cite{Wenzel:2013:ITP}
+ \begin{description}
-asynchronous user interaction \cite{Wenzel:2010},
-\cite{Wenzel:2012:UITP-EPTCS}
+ \item [PIDE] is a general framework for Prover IDEs based on
+ Isabelle/Scala. It is built around a concept of parallel and
+ asynchronous document processing, which is supported natively by the
+ parallel proof engine that is implemented in Isabelle/ML. The prover
+ discontinues the traditional TTY-based command loop, and supports
+ direct editing of formal source text with rich formal markup for GUI
+ rendering.
-document-oriented proof processing and Prover IDE \cite{Wenzel:2011:CICM}
-\cite{Wenzel:2012}
-
-\begin{description}
+ \item [Isabelle/ML] is the implementation and extension language of
+ Isabelle, see also \cite{isabelle-implementation}. It is integrated
+ into the logical context of Isabelle/Isar and allows to manipulate
+ logical entities directly. Arbitrary add-on tools may be implemented
+ for object-logics such as Isabelle/HOL.
-\item [PIDE] is a general framework for Prover IDEs based on the
-Isabelle/Scala. It is built around a concept of \emph{asynchronous document
-processing}, which is supported natively by the \emph{parallel proof engine}
-that is implemented in Isabelle/ML.
+ \item [Isabelle/Scala] is the system programming language of
+ Isabelle. It extends the pure logical environment of Isabelle/ML
+ towards the ``real world'' of graphical user interfaces, text
+ editors, IDE frameworks, web services etc. Special infrastructure
+ allows to transfer algebraic datatypes and formatted text easily
+ between ML and Scala, using asynchronous protocol commands.
+
+ \item [jEdit] is a sophisticated text editor implemented in
+ Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
+ by plugins written in languages that work on the JVM, e.g.\
+ Scala\footnote{\url{http://www.scala-lang.org/}}.
-\item [jEdit] is a sophisticated text editor \url{http://www.jedit.org}
-implemented in Java. It is easily extensible by plugins written in any
-language that works on the JVM, e.g.\ Scala.
+ \item [Isabelle/jEdit] is the main example application of the PIDE
+ framework and the default user-interface for Isabelle. It targets
+ both beginners and experts. Technically, Isabelle/jEdit combines a
+ slightly modified version of the jEdit code base with a special
+ plugin for Isabelle, integrated as standalone application for the
+ main operating system platforms: Linux, Windows, Mac OS X.
-\item [Isabelle/jEdit] is the main example application of the PIDE framework
-and the default user-interface for Isabelle. It is targeted at beginners and
-experts alike.
+ \end{description}
-\end{description}
-*}
+ The subtle differences of Isabelle/ML versus Standard ML,
+ Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
+ taken into account when discussing any of these PIDE building blocks
+ in public forums, mailing lists, or even scientific publications.
+ *}
section {* The Isabelle/jEdit Prover IDE *}
text {*
+ \begin{figure}[htb]
+ \begin{center}
\includegraphics[width=\textwidth]{isabelle-jedit}
+ \end{center}
+ \caption{The Isabelle/jEdit Prover IDE}
+ \label{fig:isabelle-jedit}
+ \end{figure}
- Isabelle/jEdit consists of some plugins for the well-known jEdit text
- editor \url{http://www.jedit.org}, according to the following
- principles.
+ Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
+ plugins for the well-known jEdit text editor
+ \url{http://www.jedit.org}, according to the following principles.
\begin{itemize}
- \item The original jEdit look-and-feel is generally preserved, although
- some default properties have been changed to accommodate Isabelle (e.g.\
- the text area font).
+ \item The original jEdit look-and-feel is generally preserved,
+ although some default properties are changed to accommodate Isabelle
+ (e.g.\ the text area font).
- \item Formal Isabelle/Isar text is checked asynchronously while editing.
- The user is in full command of the editor, and the prover refrains from
- locking portions of the buffer.
+ \item Formal Isabelle/Isar text is checked asynchronously while
+ editing. The user is in full command of the editor, and the prover
+ refrains from locking portions of the buffer.
\item Prover feedback works via colors, boxes, squiggly underline,
- hyperlinks, popup windows, icons, clickable output, all based on semantic
- markup produced by Isabelle in the background.
+ hyperlinks, popup windows, icons, clickable output --- all based on
+ semantic markup produced by Isabelle in the background.
- \item Using the mouse together with the modifier key @{verbatim CONTROL}
- (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes additional
- formal content via tooltips and/or hyperlinks.
+ \item Using the mouse together with the modifier key @{verbatim
+ CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
+ additional formal content via tooltips and/or hyperlinks.
- \item Dockable panels (e.g. \emph{Output}, \emph{Symbols}) are managed as
- independent windows by jEdit, which also allows multiple instances.
+ \item Formal output (in popups etc.) may be explored recursively,
+ using the same techniques as in the editor source buffer.
- \item Formal output (in popups etc.) may be explored recursively, using
- the same techniques as in the editor source buffer.
+ \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
+ organized by the Dockable Window Manager of jEdit, which also allows
+ multiple floating instances of each window class.
- \item The prover process and source files are managed on the editor side.
- The prover operates on timeless and stateless document content via
- Isabelle/Scala.
+ \item The prover process and source files are managed on the editor
+ side. The prover operates on timeless and stateless document
+ content as provided via Isabelle/Scala.
- \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give access
- to a selection of Isabelle/Scala options and its persistence preferences,
- usually with immediate effect on the prover back-end or editor front-end.
+ \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
+ access to a selection of Isabelle/Scala options and its persistent
+ preferences, usually with immediate effect on the prover back-end or
+ editor front-end.
\item The logic image of the prover session may be specified within
- Isabelle/jEdit, but this requires restart. The new image is provided
- automatically by the Isabelle build process.
+ Isabelle/jEdit. The new image is provided automatically by the
+ Isabelle build tool after restart of the application.
\end{itemize}
*}
+subsection {* Documentation *}
+
+text {* Regular jEdit documentation is accessible via its @{verbatim
+ Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
+ \emph{User's Guide} and \emph{Frequently Asked Questions} for this
+ sophisticated text editor.
+
+ Most of this information about jEdit is relevant for Isabelle/jEdit
+ as well, but one needs to keep in mind that defaults sometimes
+ differ, and the official jEdit documentation does not know about the
+ Isabelle plugin with its special support for theory editing.
+*}
+
+
+subsection {* Plugins *}
+
+text {* The \emph{Plugin Manager} of jEdit allows to augment editor
+ functionality by JVM modules (jars) that are provided by the central
+ plugin repository, which is accessible via various mirror sites.
+
+ Connecting to the plugin server infrastructure of the jEdit project
+ allows to update bundled plugins or to add further functionality.
+ This needs to be done with the usual care for such an open bazaar of
+ contributions. Arbitrary combinations of add-on features are apt to
+ cause problems. It is advisable to start with the default
+ configuration of Isabelle/jEdit and develop some understanding how
+ it is supposed to work, before loading additional plugins at a grand
+ scale.
+
+ \medskip The main \emph{Isabelle} plugin is an integral part of
+ Isabelle/jEdit and needs to remain active at all times! A few
+ additional plugins are bundled with Isabelle/jEdit for convenience
+ or out of necessity, notably \emph{Console} with its Isabelle/Scala
+ sub-plugin and \emph{SideKick} with some Isabelle-specific parsers
+ for document tree structure. The \emph{ErrorList} plugin is
+ required by \emph{SideKick}, but not used specifically in
+ Isabelle/jEdit. *}
+
+
+subsection {* Options *}
+
+text {* Both jEdit and Isabelle have distinctive management of
+ persistent options.
+
+ Regular jEdit options are accessible via the dialog for
+ \emph{Plugins / Plugin Options}, which is also accessible via
+ \emph{Utilities / Global Options}. Changed properties are stored in
+ @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"}. In
+ contrast, Isabelle system options are managed by Isabelle/Scala and
+ changed values stored in @{file_unchecked
+ "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit
+ properties. See also \cite{isabelle-sys}, especially the coverage
+ of sessions and command-line tools like @{tool build} or @{tool
+ options}.
+
+ Those Isabelle options that are declared as \textbf{public} are
+ configurable in jEdit via \emph{Plugin Options / Isabelle /
+ General}. Moreover, there are various options for rendering of
+ document content, which are configurable via \emph{Plugin Options /
+ Isabelle / Rendering}. Thus \emph{Plugin Options / Isabelle} in
+ jEdit provides a view on a subset of Isabelle system options. Note
+ that some of these options affect general parameters that are
+ relevant outside Isabelle/jEdit as well, e.g.\ @{system_option
+ threads} or @{system_option parallel_proofs} for the Isabelle build
+ tool \cite{isabelle-sys}.
+
+ \medskip All options are loaded on startup and saved on shutdown of
+ Isabelle/jEdit. Editing the machine-generated @{file_unchecked
+ "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
+ "$ISABELLE_HOME_USER/etc/preferences"} manually while the
+ application is running is likely to cause surprise due to lost
+ update! *}
+
+
+subsection {* Keymaps *}
+
+text {* Keyboard shortcuts used to be managed as jEdit properties in
+ the past, but recent versions (2013) have a separate concept of
+ \emph{keymap} that is configurable via \emph{Global Options /
+ Shortcuts}. The @{verbatim imported} keymap is derived from the
+ initial environment of properties that is available at the first
+ start of the editor; afterwards the keymap file takes precedence.
+
+ This is relevant for Isabelle/jEdit due to various fine-tuning of
+ default properties, and additional keyboard shortcuts for Isabelle
+ specific functionality. Users may change their keymap later, but
+ need to copy Isabelle-specific key bindings manually (see also
+ @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}). *}
+
+
+subsection {* Look-and-feel *}
+
+text {* jEdit is a Java/AWT/Swing application with some ambition to
+ support ``native'' look-and-feel on all platforms, within the limits
+ of what Oracle as Java provider and major operating system
+ distributors allow (see also \secref{sec:problems}).
+
+ Isabelle/jEdit enables platform-specific look-and-feel by default as
+ follows:
+
+ \begin{description}
+
+ \item[Linux] The platform-independent \emph{Nimbus} is used by
+ default.
+
+ \emph{GTK+} works under the side-condition that the overall GTK
+ theme is selected in a Swing-friendly way.\footnote{GTK support in
+ Java/Swing was once marketed aggressively by Sun, but never quite
+ finished, and is today (2013) lagging a bit behind further
+ development of Swing and GTK.}
+
+ \item[Windows] Regular \emph{Windows} is used by default, but
+ \emph{Windows Classic} also works.
+
+ \item[Mac OS X] Regular \emph{Mac OS X} is used by default.
+
+ Moreover the bundled \emph{MacOSX} plugin provides various functions
+ that are expected from applications on that particular platform:
+ quit from menu or dock, preferences menu, drag-and-drop of text
+ files on the application, full-screen mode for main editor windows
+ etc.
+
+ \end{description}
+
+ Users may experiment with different look-and-feels, but need to keep
+ in mind that this extra variance of GUI functionality is unlikely to
+ work in arbitrary combinations. The platform-independent
+ \emph{Nimbus} and \emph{Metal} should always work. The historic
+ \emph{CDE/Motif} is better avoided.
+
+ After changing the look-and-feel in \emph{Global Options /
+ Appearance}, it is advisable to restart Isabelle/jEdit in order to
+ take full effect. *}
+
+
chapter {* Prover IDE functionality *}
-section {* Isabelle symbols and fonts *}
+section {* File-system access *}
+
+text {* File specifications in jEdit follow various formats and
+ conventions according to \emph{Virtual File Systems}, which may be
+ also provided by additional plugins. This allows to access remote
+ files via the @{verbatim "http:"} protocol prefix, for example.
+ Isabelle/jEdit attempts to work with the file-system access model of
+ jEdit as far as possible. In particular, theory sources are passed
+ directly from the editor to the prover, without indirection via
+ files.
+
+ Despite the flexibility of URLs in jEdit, local files are
+ particularly important and are accessible without protocol prefix.
+ Here the path notation is that of the Java Virtual Machine on the
+ underlying platform. On Windows the preferred form uses
+ backslashes, but happens to accept Unix/POSIX forward slashes, too.
+ Further differences arise due to drive letters and network shares.
+
+ The Java notation for files needs to be distinguished from the one
+ of Isabelle, which uses POSIX notation with forward slashes on
+ \emph{all} platforms.\footnote{Isabelle on Windows uses Cygwin
+ file-system access.} Moreover, environment variables from the
+ Isabelle process may be used freely, e.g.\ @{file
+ "$ISABELLE_HOME/etc/symbols"} or @{file
+ "$ISABELLE_JDK_HOME/README.html"}. There are special shortcuts:
+ @{file "~"} for @{file "$USER_HOME"} and @{file "~~"} for @{file
+ "$ISABELLE_HOME"}.
+
+ \medskip Since jEdit happens to support environment variables within
+ file specifications as well, it is natural to use similar notation
+ within the editor, e.g.\ in the file-browser. This does not work in
+ full generality, though, due to the bias of jEdit towards
+ platform-specific notation and of Isabelle towards POSIX. Moreover,
+ the Isabelle settings environment is not yet active when starting
+ Isabelle/jEdit via its standard application wrapper (in contrast to
+ @{verbatim "isabelle jedit"} run from the command line).
+
+ For convenience, Isabelle/jEdit imitates at least @{verbatim
+ "$ISABELLE_HOME"} and @{verbatim "$ISABELLE_HOME_USER"} within the
+ Java process environment, in order to allow easy access to these
+ important places from the editor.
+
+ Moreover note that path specifications in prover input or output
+ usually include formal markup that turns it into a hyperlink (see
+ also \secref{sec:tooltips-hyperlinks}). This allows to open the
+ corresponding file in the text editor, independently of the path
+ notation. *}
+
+
+section {* Text buffers and theories \label{sec:buffers-theories} *}
+
+text {* As regular text editor, jEdit maintains a collection of open
+ \emph{text buffers} to store source files; each buffer may be
+ associated with any number of visible \emph{text areas}. Buffers
+ are subject to an \emph{edit mode} that is determined from the file
+ type. Files with extension \texttt{.thy} are assigned to the mode
+ \emph{isabelle} and treated specifically.
+
+ \medskip Isabelle theory files are automatically added to the formal
+ document model of Isabelle/Scala, which maintains a family of
+ versions of all sources for the prover. The \emph{Theories} panel
+ provides an overview of the status of continuous checking of theory
+ sources. Unlike batch sessions \cite{isabelle-sys}, theory nodes
+ are identified by full path names; this allows to work with multiple
+ (disjoint) Isabelle sessions simultaneously within the same editor
+ session.
+
+ Certain events to open or update buffers with theory files cause
+ Isabelle/jEdit to resolve dependencies of \emph{theory imports}.
+ The system requests to load additional files into editor buffers, in
+ order to be included in the theory document model for further
+ checking. It is also possible to resolve dependencies
+ automatically, depending on \emph{Plugin Options / Isabelle /
+ General / Auto load}.
+
+ \medskip The open text area views on theory buffers define the
+ visible \emph{perspective} of Isabelle/jEdit. This is taken as a
+ hint for document processing: the prover ensures that those parts of
+ a theory where the user is looking are checked, while other parts
+ that are presently not required are ignored. The perspective is
+ changed by opening or closing text area windows, or scrolling within
+ an editor window.
+
+ The \emph{Theories} panel provides some further options to influence
+ the process of continuous checking: it may be switched off globally
+ to restrict the prover to superficial processing of command syntax.
+ It is also possible to indicate theory nodes as \emph{required} for
+ continuous checking: this means such nodes and all their imports are
+ always processed independently of the visibility status (if
+ continuous checking is enabled). Big theory libraries that are
+ marked as required can have significant impact on performance,
+ though.
+
+ \medskip Formal markup of checked theory content is turned into GUI
+ rendering, based on a standard repertoire known from IDEs for
+ programming languages: colors, icons, highlighting, squiggly
+ underline, tooltips, hyperlinks etc. For outer syntax of
+ Isabelle/Isar there is some traditional syntax-highlighting via
+ static keyword tables and tokenization within the editor. In
+ contrast, the painting of inner syntax (term language etc.)\ uses
+ semantic information that is reported dynamically from the logical
+ context. Thus the prover can provide additional markup to help the
+ user to understand the meaning of formal text, and to produce more
+ text with some add-on tools (e.g.\ information messages by automated
+ provers or disprovers running in the background).
+*}
+
+
+section {* Prover output \label{sec:prover-output} *}
+
+text {* Prover output consists of \emph{markup} and \emph{messages}.
+ Both are directly attached to the corresponding positions in the
+ original source text, and visualized in the text area, e.g.\ as text
+ colours for free and bound variables, or as squiggly underline for
+ warnings, errors etc.\ (see also \figref{fig:output}). In the
+ latter case, the corresponding messages are shown by hovering with
+ the mouse over the highlighted text --- although in many situations
+ the user should already get some clue by looking at the position of
+ the text highlighting.
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[width=\textwidth]{output}
+ \end{center}
+ \caption{Multiple views on prover output: gutter area with icon,
+ text area with popup, overview area, Theories panel, Output panel}
+ \label{fig:output}
+ \end{figure}
-text {*
- Isabelle supports infinitely many symbols:
+ The ``gutter area'' on the left-hand-side of the text area uses
+ icons to provide a summary of the messages within the adjacent
+ line of text. Message priorities are used to prefer errors over
+ warnings, warnings over information messages etc. Plain output is
+ ignored here.
+
+ The ``overview area'' on the right-hand-side of the text area uses
+ similar information to paint small rectangles for the overall status
+ of the whole text buffer. The graphics is scaled to fit the logical
+ buffer length into the given window height. Mouse clicks on the
+ overview area position the cursor approximately to the corresponding
+ line of text in the buffer. Repainting the overview in real-time
+ causes problems with big theories, so it is restricted to part of
+ the text according to \emph{Plugin Options / Isabelle / General /
+ Text Overview Limit} (in characters).
+
+ Another course-grained overview is provided by the \emph{Theories}
+ panel, but without direct correspondence to text positions. A
+ double-click on one of the theory entries with their status overview
+ opens the corresponding text buffer, without changing the cursor
+ position.
+
+ \medskip In addition, the \emph{Output} panel displays prover
+ messages that correspond to a given command, within a separate
+ window.
+
+ The cursor position in the presently active text area determines the
+ prover commands whose cumulative message output is appended and
+ shown in that window (in canonical order according to the processing
+ of the command). There are also control elements to modify the
+ update policy of the output wrt.\ continued editor movements. This
+ is particularly useful with several independent instances of the
+ \emph{Output} panel, which the Dockable Window Manager of jEdit can
+ handle conveniently.
+
+ Former users of the old TTY interaction model (e.g.\ Proof~General)
+ might find a separate window for prover messages familiar, but it is
+ important to understand that the main Prover IDE feedback happens
+ elsewhere. It is possible to do meaningful proof editing
+ efficiently, using secondary output windows only rarely.
+
+ The main purpose of the output window is to ``debug'' unclear
+ situations by inspecting internal state of the prover.\footnote{In
+ that sense, unstructured tactic scripts depend on continuous
+ debugging with internal state inspection.} Consequently, some
+ special messages for \emph{tracing} or \emph{proof state} only
+ appear here, and are not attached to the original source.
+
+ \medskip In any case, prover messages also contain markup that may
+ be explored recursively via tooltips or hyperlinks (see
+ \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate
+ certain actions (see \secref{sec:auto-tools} and
+ \secref{sec:sledgehammer}). *}
+
+
+section {* Tooltips and hyperlinks \label{sec:tooltips-hyperlinks} *}
+
+text {* Formally processed text (prover input or output) contains rich
+ markup information that can be explored further by using the
+ @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim
+ COMMAND} on Mac OS X. Hovering with the mouse while the modifier is
+ pressed reveals a \emph{tooltip} (grey box over the text with a
+ yellow popup) and/or a \emph{hyperlink} (black rectangle over the
+ text); see also \figref{fig:tooltip}.
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.3]{popup1}
+ \end{center}
+ \caption{Tooltip and hyperlink for some formal entity}
+ \label{fig:tooltip}
+ \end{figure}
+
+ Tooltip popups use the same rendering principles as the main text
+ area, and further tooltips and/or hyperlinks may be exposed
+ recursively by the same mechanism; see \figref{fig:nested-tooltips}.
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.3]{popup2}
+ \end{center}
+ \caption{Nested tooltips over formal entities}
+ \label{fig:nested-tooltips}
+ \end{figure}
+
+ The tooltip popup window provides some controls to \emph{close} or
+ \emph{detach} the window, turning it into a separate \emph{Info}
+ window managed by jEdit. The @{verbatim ESCAPE} key closes
+ \emph{all} popups, which is particularly relevant when nested
+ tooltips are stacking up.
+
+ \medskip A black rectangle in the text indicates a hyperlink that
+ may be followed by a mouse click (while the @{verbatim CONTROL} or
+ @{verbatim COMMAND} modifier key is still pressed). Presently
+ (Isabelle2013-1) there is no systematic navigation within the
+ editor to return to the original location.
+
+ Also note that the link target may be a file that is itself not
+ subject to formal document processing of the editor session and thus
+ prevents further exploration: the chain of hyperlinks may end in
+ some source file of the underlying logic image, or within the
+ Isabelle/ML bootstrap sources of Isabelle/Pure. *}
+
+
+section {* Text completion \label{sec:completion} *}
+
+text {* \paragraph{Completion tables} are determined statically from
+ the ``outer syntax'' of the underlying edit mode (for theory files
+ this is the syntax of Isar commands), and specifications of Isabelle
+ symbols (see also \secref{sec:symbols}).
+
+ Symbols are completed in backslashed forms, e.g.\ @{verbatim
+ "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the
+ Isabelle symbol @{text "\<forall>"} in its Unicode rendering.\footnote{The
+ extra backslash avoids overlap with keywords of the buffer syntax,
+ and allows to produce Isabelle symbols robustly in most syntactic
+ contexts.} Alternatively, symbol abbreviations may be used as
+ specified in @{file "$ISABELLE_HOME/etc/symbols"}.
+
+ \paragraph{Completion popups} are required in situations of
+ ambiguous completion results or where explicit confirmation is
+ demanded before inserting completed text into the buffer.
+
+ The popup is some minimally invasive GUI component over the text
+ area. It interprets special keys @{verbatim TAB}, @{verbatim
+ ESCAPE}, @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP},
+ @{verbatim PAGE_DOWN}, but all other key events are passed to the
+ underlying text area. This allows to ignore unwanted completions
+ most of the time and continue typing quickly.
+
+ The meaning of special keys is as follows:
\medskip
- \begin{tabular}{l}
- @{text "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} \\
- @{text "\<forall>"}, @{text "\<exists>"}, @{text "\<or>"}, @{text "\<and>"}, @{text "\<longrightarrow>"}, @{text "\<longleftrightarrow>"}, @{text "\<dots>"} \\
- @{text "\<le>"}, @{text "\<ge>"}, @{text "\<sqinter>"}, @{text "\<squnion>"}, @{text "\<dots>"} \\
- @{text "\<aleph>"}, @{text "\<triangle>"}, @{text "\<nabla>"}, @{text "\<dots>"} \\
- @{verbatim "\<foo>"}, @{verbatim "\<bar>"}, @{verbatim "\<baz>"}, @{text "\<dots>"} \\
+ \begin{tabular}{ll}
+ \textbf{key} & \textbf{action} \\\hline
+ @{verbatim "TAB"} & select completion \\
+ @{verbatim "ESCAPE"} & dismiss popup \\
+ @{verbatim "UP"} & move up one item \\
+ @{verbatim "DOWN"} & move down one item \\
+ @{verbatim "PAGE_UP"} & move up one page of items \\
+ @{verbatim "PAGE_DOWN"} & move down one page of items \\
\end{tabular}
\medskip
- A default mapping relates some Isabelle symbols to Unicode points (see
- @{file "$ISABELLE_HOME/etc/symbols"} and @{verbatim
- "$ISABELLE_HOME_USER/etc/symbols"}.
-
- The \emph{IsabelleText} font ensures that Unicode points are actually seen
- on the screen (or printer).
+ Movement within the popup is only active for multiple items.
+ Otherwise the corresponding key event retains its standard meaning
+ within the underlying text area.
- \medskip
- Input methods:
+ \paragraph{Explicit completion} is triggered by the keyboard
+ shortcut @{verbatim "C+b"} (action @{verbatim "isabelle.complete"}).
+ This overrides the original jEdit binding for action @{verbatim
+ "complete-word"}, but the latter is used as fall-back for
+ non-Isabelle edit modes. It is also possible to restore the
+ original jEdit keyboard mapping of @{verbatim "complete-word"} via
+ \emph{Global Options / Shortcuts}.
+
+ Replacement text is inserted immediately into the buffer, unless
+ ambiguous results demand an explicit popup.
+
+ \paragraph{Implicit completion} is triggered by regular keyboard
+ input events during of the editing process in the main jEdit text
+ area (and a few additional text fields like the search criteria of
+ the Find panel, see \secref{sec:find}). Implicit completion depends
+ on on further side-conditions:
+
\begin{enumerate}
- \item use the \emph{Symbols} dockable window
- \item copy/paste from decoded source files
- \item copy/paste from prover output
- \item completion provided by Isabelle plugin, e.g.\
- \medskip
- \begin{tabular}{lll}
- \textbf{symbol} & \textbf{abbreviation} & \textbf{backslash escape} \\[1ex]
+ \item The system option @{system_option jedit_completion} needs to
+ be enabled (default).
- @{text "\<lambda>"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\
- @{text "\<Rightarrow>"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\
- @{text "\<Longrightarrow>"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\
+ \item Completion of syntax keywords requires at least 3 relevant
+ characters in the text.
- @{text "\<And>"} & @{verbatim "!!"} & @{verbatim "\\And"} \\
- @{text "\<equiv>"} & @{verbatim "=="} & @{verbatim "\\equiv"} \\
+ \item The system option @{system_option jedit_completion_delay}
+ determines an additional delay (0.0 by default), before opening a
+ completion popup.
- @{text "\<forall>"} & @{verbatim "!"} & @{verbatim "\\forall"} \\
- @{text "\<exists>"} & @{verbatim "?"} & @{verbatim "\\exists"} \\
- @{text "\<longrightarrow>"} & @{verbatim "-->"} & @{verbatim "\\longrightarrow"} \\
- @{text "\<and>"} & @{verbatim "&"} & @{verbatim "\\and"} \\
- @{text "\<or>"} & @{verbatim "|"} & @{verbatim "\\or"} \\
- @{text "\<not>"} & @{verbatim "~"} & @{verbatim "\\not"} \\
- @{text "\<noteq>"} & @{verbatim "~="} & @{verbatim "\\noteq"} \\
- @{text "\<in>"} & @{verbatim ":"} & @{verbatim "\\in"} \\
- @{text "\<notin>"} & @{verbatim "~:"} & @{verbatim "\\notin"} \\
- \end{tabular}
+ \item The system option @{system_option
+ jedit_completion_dismiss_delay} determines an additional delay (0.0
+ by default), before dismissing an earlier completion popup. A value
+ like 0.1 is occasionally useful to reduce the chance of loosing key
+ strokes when the speed of typing exceeds that of repainting GUI
+ components.
+
+ \item The system option @{system_option jedit_completion_immediate}
+ (disabled by default) controls whether replacement text should be
+ inserted immediately without popup. This is restricted to Isabelle
+ symbols and their abbreviations (\secref{sec:symbols}) --- plain
+ keywords always demand a popup for clarity.
+
+ \item Completion of symbol abbreviations with only one relevant
+ character in the text always enforces an explicit popup,
+ independently of @{system_option jedit_completion_immediate}.
\end{enumerate}
- \paragraph{Notes:}
+ These completion options may be configured in \emph{Plugin Options /
+ Isabelle / General / Completion}. The default is quite moderate in
+ showing occasional popups and refraining from immediate insertion.
+ An additional completion delay of 0.3 seconds will make it even less
+ ambitious.
+
+ In contrast, more aggressive completion works via @{system_option
+ jedit_completion_delay}~@{verbatim "= 0.0"} and @{system_option
+ jedit_completion_immediate}~@{verbatim "= true"}. Thus the editing
+ process becomes dependent on the system guessing correctly what the
+ user had in mind. It requires some practice (and study of the
+ symbol abbreviation tables) to become productive in this advanced
+ mode.
+
+ In any case, unintended completions can be reverted by the regular
+ @{verbatim undo} operation of jEdit. When editing embedded
+ languages such as ML, it is better to disable either @{system_option
+ jedit_completion} or @{system_option jedit_completion_immediate}
+ temporarily. *}
+
+
+section {* Isabelle symbols \label{sec:symbols} *}
+
+text {* Isabelle sources consist of \emph{symbols} that extend plain
+ ASCII to allow infinitely many mathematical symbols within the
+ formal sources. This works without depending on particular
+ encodings and varying Unicode standards
+ \cite{Wenzel:2011:CICM}.\footnote{Raw Unicode characters within
+ formal sources would compromise portability and reliability in the
+ face of changing interpretation of special features of Unicode, such
+ as Combining Characters or Bi-directional Text.}
+
+ For the prover back-end, formal text consists of ASCII characters
+ that are grouped according to some simple rules, e.g.\ as plain
+ ``@{verbatim a}'' or symbolic ``@{verbatim "\<alpha>"}''.
+
+ For the editor front-end, a certain subset of symbols is rendered
+ physically via Unicode glyphs, in order to show ``@{verbatim "\<alpha>"}''
+ as ``@{text "\<alpha>"}'', for example. This symbol interpretation is
+ specified by the Isabelle system distribution in @{file
+ "$ISABELLE_HOME/etc/symbols"} and may be augmented by the user in
+ @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
+
+ The appendix of \cite{isabelle-isar-ref} gives an overview of the
+ standard interpretation of finitely many symbols from the infinite
+ collection. Uninterpreted symbols are displayed literally, e.g.\
+ ``@{verbatim "\<foobar>"}''. Overlap of Unicode characters used in
+ symbol interpretation with informal ones (which might appear e.g.\
+ in comments) needs to be avoided! Raw Unicode characters within
+ prover source files should be restricted to informal parts, e.g.\ to
+ write text in non-latin alphabets in comments.
+
+ \medskip \paragraph{Encoding.} Technically, the Unicode view on
+ Isabelle symbols is an \emph{encoding} in jEdit (not in the
+ underlying JVM) that is called @{verbatim "UTF-8-Isabelle"}. It is
+ provided by the Isabelle/jEdit plugin and enabled by default for all
+ source files. Sometimes such defaults are reset accidentally, or
+ malformed UTF-8 sequences in the text force jEdit to fall back on a
+ different encoding like @{verbatim "ISO-8859-15"}. In that case,
+ verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer
+ instead of its Unicode rendering ``@{text "\<alpha>"}''. The jEdit menu
+ operation \emph{File / Reload with Encoding / UTF-8-Isabelle} helps
+ to resolve such problems, potentially after repairing malformed
+ parts of the text.
+
+ \medskip \paragraph{Font.} Correct rendering via Unicode requires a
+ font that contains glyphs for the corresponding codepoints. Most
+ system fonts lack that, so Isabelle/jEdit prefers its own
+ application font @{verbatim IsabelleText}, which ensures that
+ standard collection of Isabelle symbols are actually seen on the
+ screen (or printer).
+
+ Note that a Java/AWT/Swing application can load additional fonts
+ only if they are not installed on the operating system already!
+ Some old version of @{verbatim IsabelleText} that happens to be
+ provided by the operating system would prevents Isabelle/jEdit from
+ its bundled version. This could lead to missing glyphs (black
+ rectangles), when the system version of @{verbatim IsabelleText} is
+ older than the application version. This problem can be avoided by
+ refraining to ``install'' any version of @{verbatim IsabelleText} in
+ the first place (although it might be occasionally tempting to use
+ the same font in other applications).
+
+ \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
+ could delegate the problem to produce Isabelle symbols in their
+ Unicode rendering to the underlying operating system and its
+ \emph{input methods}. Regular jEdit also provides various ways to
+ work with \emph{abbreviations} to produce certain non-ASCII
+ characters. Since none of these standard input methods work
+ satisfactorily for the mathematical characters required for
+ Isabelle, various specific Isabelle/jEdit mechanisms are provided.
+
+ Here is a summary for practically relevant input methods for
+ Isabelle symbols:
+
+ \begin{enumerate}
+
+ \item The \emph{Symbols} panel with some GUI buttons to insert
+ certain symbols in the text buffer. There are also tooltips to
+ reveal the official Isabelle representation with some additional
+ information about \emph{symbol abbreviations} (see below).
+
+ \item Copy / paste from decoded source files: text that is rendered
+ as Unicode already can be re-used to produce further text. This
+ also works between different applications, e.g.\ Isabelle/jEdit and
+ some web browser or mail client, as long as the same Unicode view on
+ Isabelle symbols is used uniformly.
+
+ \item Copy / paste from prover output within Isabelle/jEdit. The
+ same principles as for text buffers apply, but note that \emph{copy}
+ in secondary Isabelle/jEdit windows works via the keyboard shortcut
+ @{verbatim "C+c"}, while jEdit menu actions always refer to the
+ primary text area!
+
+ \item Completion provided by Isabelle plugin (see
+ \secref{sec:completion}). Isabelle symbols have a canonical name
+ and optional abbreviations. This can be used with the text
+ completion mechanism of Isabelle/jEdit, to replace a prefix of the
+ actual symbol like @{verbatim "\<lambda>"}, or its backslashed name
+ @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
+ @{verbatim "%"} by the Unicode rendering.
+
+ The following table is an extract of the information provided by the
+ standard @{file "$ISABELLE_HOME/etc/symbols"} file:
+
+ \medskip
+ \begin{tabular}{lll}
+ \textbf{symbol} & \textbf{backslashed name} & \textbf{abbreviation} \\\hline
+ @{text "\<lambda>"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\
+ @{text "\<Rightarrow>"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\
+ @{text "\<Longrightarrow>"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex]
+ @{text "\<And>"} & @{verbatim "\\And"} & @{verbatim "!!"} \\
+ @{text "\<equiv>"} & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex]
+ @{text "\<forall>"} & @{verbatim "\\forall"} & @{verbatim "!"} \\
+ @{text "\<exists>"} & @{verbatim "\\exists"} & @{verbatim "?"} \\
+ @{text "\<longrightarrow>"} & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\
+ @{text "\<and>"} & @{verbatim "\\and"} & @{verbatim "&"} \\
+ @{text "\<or>"} & @{verbatim "\\or"} & @{verbatim "|"} \\
+ @{text "\<not>"} & @{verbatim "\\not"} & @{verbatim "~"} \\
+ @{text "\<noteq>"} & @{verbatim "\\noteq"} & @{verbatim "~="} \\
+ @{text "\<in>"} & @{verbatim "\\in"} & @{verbatim ":"} \\
+ @{text "\<notin>"} & @{verbatim "\\notin"} & @{verbatim "~:"} \\
+ \end{tabular}
+ \medskip
+
+ Note that the above abbreviations refer to the input method. The
+ logical notation provides ASCII alternatives that often coincide,
+ but deviate occasionally. This occasionally causes user confusion
+ with very old-fashioned Isabelle source that use ASCII replacement
+ notation like @{verbatim "!"} or @{verbatim "ALL"} directly in the
+ text.
+
+ On the other hand, coincidence of symbol abbreviations with ASCII
+ replacement syntax syntax helps to update old theory sources via
+ explicit completion (see also @{verbatim "C+b"} explained in
+ \secref{sec:completion}).
+
+ \end{enumerate}
+
+ \paragraph{Control symbols.} There are some special control symbols
+ to modify the display style of a single symbol (without
+ nesting). Control symbols may be applied to a region of selected
+ text, either using the \emph{Symbols} panel or keyboard shortcuts or
+ jEdit actions. These editor operations produce a separate control
+ symbol for each symbol in the text, in order to make the whole text
+ appear in a certain style.
+
+ \medskip
+ \begin{tabular}{llll}
+ \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
+ superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{verbatim "isabelle.control-sup"} \\
+ subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{verbatim "isabelle.control-sub"} \\
+ bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{verbatim "isabelle.control-bold"} \\
+ reset & & @{verbatim "C+e LEFT"} & @{verbatim "isabelle.control-reset"} \\
+ \end{tabular}
+ \medskip
+
+ To produce a single control symbol, it is also possible to complete
+ on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub},
+ @{verbatim "\\"}@{verbatim bold} as for regular symbols. *}
+
+
+section {* Automatically tried tools \label{sec:auto-tools} *}
+
+text {* Continuous document processing works asynchronously in the
+ background. Visible document source that has been evaluated already
+ may get augmented by additional results of \emph{asynchronous print
+ functions}. The canonical example is proof state output, which is
+ always enabled. More heavy-weight print functions may be applied,
+ in order to prove or disprove parts of the formal text by other
+ means.
+
+ Isabelle/HOL provides various automatically tried tools that operate
+ on outermost goal statements (e.g.\ @{command lemma}, @{command
+ theorem}), independently of the state of the current proof attempt.
+ They work implicitly without any arguments. Results are output as
+ \emph{information messages}, which are indicated in the text area by
+ blue squiggles and a blue information sign in the gutter (see
+ \figref{fig:auto-tools}). The message content may be shown as for
+ other output (see also \secref{sec:prover-output}). Some tools
+ produce output with \emph{sendback} markup, which means that
+ clicking on certain parts of the output inserts that text into the
+ source in the proper place.
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.3]{auto-tools}
+ \end{center}
+ \caption{Results of automatically tried tools}
+ \label{fig:auto-tools}
+ \end{figure}
+
+ \medskip The following Isabelle system options control the behavior
+ of automatically tried tools (see also the jEdit dialog window
+ \emph{Plugin Options / Isabelle / General / Automatically tried
+ tools}):
+
\begin{itemize}
- \item The above abbreviations refer to the input method. The logical
- notation provides ASCII alternatives that often coincide, but deviate
- occasionally.
+ \item @{system_option auto_methods} controls automatic use of a
+ combination of standard proof methods (@{method auto}, @{method
+ simp}, @{method blast}, etc.). This corresponds to the Isar command
+ @{command "try0"}.
+
+ The tool is disabled by default, since unparameterized invocation of
+ standard proof methods often consumes substantial CPU resources
+ without leading to success.
+
+ \item @{system_option auto_nitpick} controls a slightly reduced
+ version of @{command nitpick}, which tests for counterexamples using
+ first-order relational logic. See also the Nitpick manual
+ \cite{isabelle-nitpick}.
+
+ This tool is disabled by default, due to the extra overhead of
+ invoking an external Java process for each attempt to disprove a
+ subgoal.
- \item Generic jEdit abbreviations or plugins perform similar source
- replacement operations; this works for Isabelle as long as the Unicode
- sequences coincide with the symbol mapping.
+ \item @{system_option auto_quickcheck} controls automatic use of
+ @{command quickcheck}, which tests for counterexamples using a
+ series of assignments for free variables of a subgoal.
+
+ This tool is \emph{enabled} by default. It requires little
+ overhead, but is a bit weaker than @{command nitpick}.
- \item Raw Unicode characters within prover source files should be
- restricted to informal parts, e.g.\ to write text in non-latin alphabets.
- Mathematical symbols should be defined via the official rendering tables.
+ \item @{system_option auto_sledgehammer} controls a significantly
+ reduced version of @{command sledgehammer}, which attempts to prove
+ a subgoal using external automatic provers. See also the
+ Sledgehammer manual \cite{isabelle-sledgehammer}.
+
+ This tool is disabled by default, due to the relatively heavy nature
+ of Sledgehammer.
+
+ \item @{system_option auto_solve_direct} controls automatic use of
+ @{command solve_direct}, which checks whether the current subgoals
+ can be solved directly by an existing theorem. This also helps to
+ detect duplicate lemmas.
+
+ This tool is \emph{enabled} by default.
\end{itemize}
- \paragraph{Control symbols.} There are some special control symbols to
- modify the style of a \emph{single} symbol (without nesting). Control
- symbols may be applied to a region of selected text, either using the
- \emph{Symbols} dockable window or keyboard shortcuts.
+ Invocation of automatically tried tools is subject to some global
+ policies of parallel execution, which may be configured as follows:
+
+ \begin{itemize}
+
+ \item @{system_option auto_time_limit} (default 2.0) determines the
+ timeout (in seconds) for each tool execution.
+
+ \item @{system_option auto_time_start} (default 1.0) determines the
+ start delay (in seconds) for automatically tried tools, after the
+ main command evaluation is finished.
- \medskip
- \begin{tabular}{lll}
- \textbf{symbol} & style & keyboard shortcure \\
- @{verbatim "\<sup>"} & superscript & @{verbatim "C+e UP"} \\
- @{verbatim "\<sub>"} & subscript & @{verbatim "C+e DOWN"} \\
- @{verbatim "\<bold>"} & bold face & @{verbatim "C+e RIGHT"} \\
- & reset & @{verbatim "C+e LEFT"} \\
- \end{tabular}
+ \end{itemize}
+
+ Each tool is submitted independently to the pool of parallel
+ execution tasks in Isabelle/ML, using hardwired priorities according
+ to its relative ``heaviness''. The main stages of evaluation and
+ printing of proof states take precedence, but an already running
+ tool is not canceled and may thus reduce reactivity of proof
+ document processing.
+
+ Users should experiment how the available CPU resources (number of
+ cores) are best invested to get additional feedback from prover in
+ the background, by using a selection of weaker or stronger tools.
*}
-section {* Text completion *}
+section {* Sledgehammer \label{sec:sledgehammer} *}
+
+text {* The \emph{Sledgehammer} panel (\figref{fig:sledgehammer})
+ provides a view on some independent execution of the Isar command
+ @{command sledgehammer}, with process indicator (spinning wheel) and
+ GUI elements for important Sledgehammer arguments and options. Any
+ number of Sledgehammer panels may be active, according to the
+ standard policies of Dockable Window Management in jEdit. Closing
+ such windows also cancels the corresponding prover tasks.
-text {*
- Text completion works via some light-weight GUI popup, which is triggered by
- keyboard events during the normal editing process in the main jEdit text
- area and a few additional text fields. The popup interprets special keys:
- @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
- @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
- to the jEdit text area --- this allows to ignore unwanted completions most
- of the time and continue typing quickly.
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.3]{sledgehammer}
+ \end{center}
+ \caption{An instance of the Sledgehammer panel}
+ \label{fig:sledgehammer}
+ \end{figure}
- Various Isabelle plugin options control the popup behavior and immediate
- insertion into buffer.
+ The \emph{Apply} button attaches a fresh invocation of @{command
+ sledgehammer} to the command where the cursor is pointing in the
+ text --- this should be some pending proof problem. Further buttons
+ like \emph{Cancel} and \emph{Locate} help to manage the running
+ process.
+
+ Results appear incrementally in the output window of the panel.
+ Proposed proof snippets are marked-up as \emph{sendback}, which
+ means a single mouse click inserts the text into a suitable place of
+ the original source. Some manual editing may be required
+ nonetheless, say to remove earlier proof attempts. *}
+
+
+section {* Find theorems \label{sec:find} *}
- Isabelle Symbols are completed in backslashed forms, e.g. @{verbatim
- "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
- symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
- abbreviations may be used as specified in @{file
- "$ISABELLE_HOME/etc/symbols"}.
+text {* The \emph{Find} panel (\figref{fig:find}) provides an
+ independent view for the Isar command @{command find_theorems}. The
+ main text field accepts search criteria according to the syntax
+ @{syntax thmcriterium} given in \cite{isabelle-isar-ref}. Further
+ options of @{command find_theorems} are available via GUI elements.
+
+ \begin{figure}[htb]
+ \begin{center}
+ \includegraphics[scale=0.3]{find}
+ \end{center}
+ \caption{An instance of the Find panel}
+ \label{fig:find}
+ \end{figure}
+
+ The \emph{Apply} button attaches a fresh invocation of @{command
+ find_theorems} to the current context of the command where the
+ cursor is pointing in the text, unless an alternative theory context
+ (from the underlying logic image) is specified explicitly. *}
- \emph{Explicit completion} works via standard jEdit shortcut @{verbatim
- "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
- fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
+
+chapter {* Miscellaneous tools *}
+
+section {* SideKick *}
+
+text {* The \emph{SideKick} plugin of jEdit provides some general
+ services to display buffer structure in a tree view.
- \emph{Implicit completion} works via keyboard input on text area, with popup
- or immediate insertion into buffer. Plain words require at least 3
- characters to be completed.
+ Isabelle/jEdit provides SideKick parsers for its main mode for
+ theory files, as well as some minor modes for the @{verbatim NEWS}
+ file, session @{verbatim ROOT} files, and system @{verbatim
+ options}.
- \emph{Immediate completion} means the (unique) replacement text is inserted
- into the buffer without popup. This mode ignores plain words and requires
- more than one characters for symbol abbreviations. Otherwise it falls back
- on completion popup.
+ Moreover, the special SideKick parser @{verbatim "isabelle-markup"}
+ provides access to the full (uninterpreted) markup tree of the PIDE
+ document model of the current buffer. This is occasionally useful
+ for informative purposes, but the amount of displayed information
+ might cause problems for large buffers, both for the human and the
+ machine.
*}
-chapter {* Known problems and workarounds *}
+section {* Timing *}
+
+text {* Managed evaluation of commands within PIDE documents includes
+ timing information, which consists of elapsed (wall-clock) time, CPU
+ time, and GC (garbage collection) time. Note that in a
+ multithreaded system it is difficult to measure execution time
+ precisely: elapsed time is closer to the real requirements of
+ runtime resources than CPU or GC time, which are both subject to
+ influences from the parallel environment that are outside the scope
+ of the current command transaction.
+
+ The \emph{Timing} panel provides an overview of cumulative command
+ timings for each document node. Commands with elapsed time below
+ the given threshold are ignored in the grand total. Nodes are
+ sorted according to their overall timing. For the document node
+ that corresponds to the current buffer, individual command timings
+ are shown as well. A double-click on a theory node or command moves
+ the editor focus to that particular source position.
+
+ It is also possible to reveal individual timing information via some
+ tooltip for the corresponding command keyword, using the technique
+ of mouse hovering with @{verbatim CONTROL}/@{verbatim COMMAND}
+ modifier key as explained in \secref{sec:tooltips-hyperlinks}.
+ Actual display of timing depends on the global option
+ @{system_option jedit_timing_threshold}, which can be configured in
+ "Plugin Options / Isabelle / General".
+
+ \medskip The \emph{Monitor} panel provides a general impression of
+ recent activity of the farm of worker threads in Isabelle/ML. Its
+ display is continuously updated according to @{system_option
+ editor_chart_delay}. Note that the painting of the chart takes
+ considerable runtime itself --- on the Java Virtual Machine that
+ runs Isabelle/Scala, not Isabelle/ML. Internally, the
+ Isabelle/Scala module @{verbatim isabelle.ML_Statistics} provides
+ further access to statistics of Isabelle/ML. *}
+
+
+section {* Isabelle/Scala console *}
+
+text {* The \emph{Console} plugin of jEdit manages various shells
+ (command interpreters), e.g.\ \emph{BeanShell}, which is the
+ official jEdit scripting language, and the cross-platform
+ \emph{System} shell. Thus the console provides similar
+ functionality than the special buffers @{verbatim "*scratch*"} and
+ @{verbatim "*shell*"} in Emacs.
+
+ Isabelle/jEdit extends the repertoire of the console by
+ \emph{Scala}, which is the regular Scala toplevel loop running
+ inside the \emph{same} JVM process as Isabelle/jEdit itself. This
+ means the Scala command interpreter has access to the JVM name space
+ and state of the running Prover IDE application: the main entry
+ points are @{verbatim view} (the current editor view of jEdit) and
+ @{verbatim PIDE} (the Isabelle/jEdit plugin object).
+
+ For example, the subsequent Scala snippet gets the PIDE document
+ model of the current buffer within the current editor view:
+
+ \begin{center}
+ @{verbatim "PIDE.document_model(view.getBuffer).get"}
+ \end{center}
+
+ This helps to explore Isabelle/Scala functionality interactively.
+ Some care is required to avoid interference with the internals of
+ the running application, especially in production use. *}
+
+
+section {* Low-level output *}
+
+text {* Prover output is normally shown directly in the main text area
+ or secondary \emph{Output} panels, as explained in
+ \secref{sec:prover-output}.
+
+ Beyond this, it is occasionally useful to inspect low-level output
+ channels via some of the following additional panels:
+
+ \begin{itemize}
+
+ \item \emph{Protocol} shows internal messages between the
+ Isabelle/Scala and Isabelle/ML side of the PIDE editing protocol.
+ Recording of messages starts with the first activation of the
+ corresponding dockable window; earlier messages are lost.
+
+ Actual display of protocol messages causes considerable slowdown, so
+ it is important to undock all \emph{Protocol} panels for production
+ work.
+
+ \item \emph{Raw Output} shows chunks of text from the @{verbatim
+ stdout} and @{verbatim stderr} channels of the prover process.
+ Recording of output starts with the first activation of the
+ corresponding dockable window; earlier output is lost.
+
+ The implicit stateful nature of physical I/O channels makes it
+ difficult to relate raw output to the actual command from where it
+ was originating. Parallel execution may add to the confusion.
+ Peeking at physical process I/O is only the last resort to diagnose
+ problems with tools that are not fully PIDE compliant.
+
+ Under normal circumstances, prover output always works via managed
+ message channels (corresponding to @{ML writeln}, @{ML warning},
+ @{ML error} etc.\ in Isabelle/ML), which are displayed by regular
+ means within the document model (\secref{sec:prover-output}).
+
+ \item \emph{Syslog} shows system messages that might be relevant to
+ diagnose problems with the startup or shutdown phase of the prover
+ process; this also includes raw output on @{verbatim stderr}.
+
+ A limited amount of syslog messages are buffered, independently of
+ the docking state of the \emph{Syslog} panel. This allows to
+ diagnose serious problems with Isabelle/PIDE process management,
+ outside of the actual protocol layer.
+
+ Under normal situations, such low-level system output can be
+ ignored.
+
+ \end{itemize}
+*}
+
+
+chapter {* Known problems and workarounds \label{sec:problems} *}
text {*
\begin{itemize}
+ \item \textbf{Problem:} Lack of dependency management for auxiliary files
+ that contribute to a theory (e.g.\ @{command ML_file}).
+
+ \textbf{Workaround:} Re-load files manually within the prover, by
+ editing corresponding command in the text.
+
+ \item \textbf{Problem:} Odd behavior of some diagnostic commands with
+ global side-effects, like writing a physical file.
+
+ \textbf{Workaround:} Copy / paste complete command text from
+ elsewhere, or discontinue continuous checking temporarily.
+
+ \item \textbf{Problem:} No way to delete document nodes from the overall
+ collection of theories.
+
+ \textbf{Workaround:} Ignore unused files. Restart whole
+ Isabelle/jEdit session in worst-case situation.
+
\item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
@{verbatim "C+MINUS"} for adjusting the editor font size depend on
platform details and national keyboards.
- \textbf{Workaround:} Use numeric keypad or rebind keys in the
- jEdit Shortcuts options dialog.
-
- \item \textbf{Problem:} Lack of dependency management for auxiliary files
- that contribute to a theory (e.g.\ @{command ML_file}).
+ \textbf{Workaround:} Rebind keys via \emph{Global Options /
+ Shortcuts}.
- \textbf{Workaround:} Re-load files manually within the prover.
-
- \item \textbf{Problem:} Odd behavior of some diagnostic commands with
- global side-effects, like writing a physical file.
-
- \textbf{Workaround:} Avoid such commands.
+ \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
+ "COMMAND+COMMA"} for application \emph{Preferences} is in conflict
+ with the jEdit default shortcut for \emph{Incremental Search Bar}
+ (action @{verbatim "quick-search"}).
- \item \textbf{Problem:} No way to delete document nodes from the overall
- collection of theories.
-
- \textbf{Workaround:} Restart whole Isabelle/jEdit session in worst-case
- situation.
+ \textbf{Workaround:} Rebind key via \emph{Global Options /
+ Shortcuts} according to national keyboard, e.g.\ @{verbatim
+ "COMMAND+SLASH"} on English ones.
- \item \textbf{Problem:} Linux: some desktop environments with extreme
- animation effects may disrupt Java 7 window placement and/or keyboard
- focus.
+ \item \textbf{Problem:} Mac OS X system fonts sometimes lead to
+ character drop-outs in the main text area.
- \textbf{Workaround:} Disable such effects.
+ \textbf{Workaround:} Use the default @{verbatim IsabelleText} font.
+ (Do not install that font on the system.)
- \item \textbf{Problem:} Linux: some X11 input methods such as IBus tend
- to disrupt key event handling of Java/Swing.
+ \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
+ tend to disrupt key event handling of Java/AWT/Swing.
\textbf{Workaround:} Do not use input methods, reset the environment
variable @{verbatim XMODIFIERS} within Isabelle settings (default in
Isabelle2013-1).
- \item \textbf{Problem:} Linux: some X11 window managers that are not
- ``re-parenting'' cause problems with additional windows opened by the Java
- VM. This affects either historic or neo-minimalistic window managers like
- ``@{verbatim awesome}'' or ``@{verbatim xmonad}''.
+ \item \textbf{Problem:} Some Linux / X11 window managers that are
+ not ``re-parenting'' cause problems with additional windows opened
+ by Java. This affects either historic or neo-minimalistic window
+ managers like @{verbatim awesome} or @{verbatim xmonad}.
\textbf{Workaround:} Use regular re-parenting window manager.
- \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
- "COMMAND+COMMA"} for Preferences is in conflict with the jEdit default
- binding for @{verbatim "quick-search"}.
+ \item \textbf{Problem:} Recent forks of Linux / X11 window managers
+ and desktop environments (variants of Gnome) disrupt the handling of
+ menu popups and mouse positions of Java/AWT/Swing.
+
+ \textbf{Workaround:} Use mainstream versions of Linux desktops.
- \textbf{Workaround:} Remap in jEdit manually according to national
- keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
+ \item \textbf{Problem:} Full-screen mode via jEdit action @{verbatim
+ "toggle-full-screen"} (default shortcut @{verbatim F11}) works on
+ Windows, but not on Mac OS X or various Linux / X11 window managers.
- \item \textbf{Problem:} Mac OS X: Java 7 is officially supported on Lion
- and Mountain Lion, but not Snow Leopard. It usually works on the latter,
- although with a small risk of instabilities.
+ \textbf{Workaround:} Use native full-screen control of the window
+ manager (notably on Mac OS X).
- \textbf{Workaround:} Update to OS X Mountain Lion, or later.
+ \item \textbf{Problem:} Full-screen mode and dockable windows in
+ \emph{floating} state may lead to confusion about window placement
+ (depending on platform characteristics).
+
+ \textbf{Workaround:} Avoid this combination.
\end{itemize}
*}
Binary file src/Doc/JEdit/document/auto-tools.png has changed
Binary file src/Doc/JEdit/document/find.png has changed
Binary file src/Doc/JEdit/document/output.png has changed
Binary file src/Doc/JEdit/document/popup1.png has changed
Binary file src/Doc/JEdit/document/popup2.png has changed
--- a/src/Doc/JEdit/document/root.tex Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/JEdit/document/root.tex Mon Nov 11 18:37:56 2013 +0100
@@ -57,7 +57,7 @@
Research and implementation of concepts around PIDE and Isabelle/jEdit has
started around 2008 and was kindly supported by:
\begin{itemize}
-\item TU M\"unchen \url{http://in.tum.de}
+\item TU M\"unchen \url{http://www.in.tum.de}
\item BMBF \url{http://www.bmbf.de}
\item Universit\'e Paris-Sud \url{http://www.u-psud.fr}
\item Digiteo \url{http://www.digiteo.fr}
@@ -65,7 +65,10 @@
\end{itemize}
-\pagenumbering{roman} \tableofcontents \clearfirst
+\pagenumbering{roman}
+\tableofcontents
+\listoffigures
+\clearfirst
\input{JEdit.tex}
Binary file src/Doc/JEdit/document/sledgehammer.png has changed
--- a/src/Doc/ROOT Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/ROOT Mon Nov 11 18:37:56 2013 +0100
@@ -143,21 +143,24 @@
"document/showsymbols"
"document/style.sty"
-session JEdit (doc) in "JEdit" = Pure +
+session JEdit (doc) in "JEdit" = HOL +
options [document_variants = "jedit", thy_output_source]
theories
JEdit
files
- "../prepare_document"
"../IsarRef/document/style.sty"
+ "../extra.sty"
+ "../iman.sty"
+ "../isar.sty"
+ "../manual.bib"
"../pdfsetup.sty"
- "../iman.sty"
- "../extra.sty"
- "../isar.sty"
+ "../prepare_document"
"../ttbox.sty"
"../underscore.sty"
- "../manual.bib"
"document/build"
+ "document/isabelle-jedit.png"
+ "document/popup1.png"
+ "document/popup2.png"
"document/root.tex"
session LaTeXsugar (doc) in "LaTeXsugar" = HOL +
--- a/src/Doc/System/Sessions.thy Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/System/Sessions.thy Mon Nov 11 18:37:56 2013 +0100
@@ -249,6 +249,8 @@
\secref{sec:tool-build}.
Option @{verbatim "-g"} prints the value of the given option.
+ Option @{verbatim "-l"} lists all options with their declaration and
+ current value.
Option @{verbatim "-x"} specifies a file to export the result in
YXML format, instead of printing it in human-readable form.
--- a/src/Doc/antiquote_setup.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/antiquote_setup.ML Mon Nov 11 18:37:56 2013 +0100
@@ -47,6 +47,22 @@
(K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
+(* unchecked file *)
+
+val file_unchecked_setup =
+ Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
+ (fn {context = ctxt, ...} => fn (name, pos) =>
+ let
+ val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt);
+ val path = Path.append dir (Path.explode name);
+ val _ = Position.report pos (Markup.path name);
+ in
+ space_explode "/" name
+ |> map Thy_Output.verb_text
+ |> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}")
+ end);
+
+
(* ML text *)
local
@@ -233,6 +249,7 @@
val setup =
verbatim_setup #>
+ file_unchecked_setup #>
index_ml_setup #>
named_thms_setup #>
thy_file_setup #>
--- a/src/Doc/manual.bib Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Doc/manual.bib Mon Nov 11 18:37:56 2013 +0100
@@ -794,6 +794,16 @@
pages = {205-216},
publisher = {Elsevier}}
+@inproceedings{Huffman-Kuncar:2013:lifting_transfer,
+ author = {Brian Huffman and Ond\v{r}ej Kun\v{c}ar},
+ title = {{Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL}},
+ booktitle = {Certified Programs and Proofs (CPP 2013)},
+ year = 2013,
+ publisher = Springer,
+ series = {Lecture Notes in Computer Science},
+ volume = {8307},
+}
+
@Book{Huth-Ryan-book,
author = {Michael Huth and Mark Ryan},
title = {Logic in Computer Science. Modelling and reasoning about systems},
@@ -1683,13 +1693,15 @@
year = 2007,
publisher = Springer}
-@unpublished{traytel-berghofer-nipkow-2011,
- author = {D. Traytel and S. Berghofer and T. Nipkow},
- title = {Extending Hindley-Milner Type Inference with Coercive
- Subtyping (long version)},
+@inproceedings{traytel-berghofer-nipkow-2011,
+ author = {Dmitriy Traytel and Stefan Berghofer and Tobias Nipkow},
+ title = {{Extending Hindley-Milner Type Inference with Coercive Structural Subtyping}},
year = 2011,
- note = {Submitted,
- \url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+ editor = {Hongseok Yang},
+ booktitle = "APLAS 2011",
+ series = LNCS,
+ volume = {7078},
+ pages = "89--104"}
@inproceedings{traytel-et-al-2012,
author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette",
--- a/src/HOL/BNF/Tools/coinduction.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/HOL/BNF/Tools/coinduction.ML Mon Nov 11 18:37:56 2013 +0100
@@ -75,7 +75,7 @@
map3 (fn name => fn T => fn (_, rhs) =>
HOLogic.mk_eq (Free (name, T), rhs))
names Ts raw_eqs;
- val phi = map (HOLogic.dest_Trueprop o prop_of) prems @ eqs
+ val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
|> try (Library.foldr1 HOLogic.mk_conj)
|> the_default @{term True}
|> list_exists_free vars
@@ -89,8 +89,8 @@
HEADGOAL (EVERY' [rtac thm,
EVERY' (map (fn var =>
rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
- EVERY' (map (fn prem => rtac conjI THEN' rtac prem) prems),
- CONJ_WRAP' (K (rtac refl)) eqs,
+ if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
+ else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
K (ALLGOALS_SKIP skip
(REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
@@ -100,11 +100,11 @@
let
val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
val inv_thms = init @ [last];
- val eqs = drop p inv_thms;
+ val eqs = take e inv_thms;
fun is_local_var t =
member (fn (t, (_, t')) => t aconv (term_of t')) params t;
val (eqs, assms') = filter_in_out (is_local_var o lhs_of_eq o prop_of) eqs;
- val assms = assms' @ take p inv_thms
+ val assms = assms' @ drop e inv_thms
in
HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
unfold_thms_tac ctxt eqs
--- a/src/HOL/Quotient_Examples/FSet.thy Mon Nov 11 18:25:13 2013 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Mon Nov 11 18:37:56 2013 +0100
@@ -5,6 +5,13 @@
Type of finite sets.
*)
+(********************************************************************
+ WARNING: There is a formalization of 'a fset as a subtype of sets in
+ HOL/Library/FSet.thy using Lifting/Transfer. The user should use
+ that file rather than this file unless there are some very specific
+ reasons.
+*********************************************************************)
+
theory FSet
imports "~~/src/HOL/Library/Multiset" "~~/src/HOL/Library/Quotient_List"
begin
--- a/src/HOL/String.thy Mon Nov 11 18:25:13 2013 +0100
+++ b/src/HOL/String.thy Mon Nov 11 18:37:56 2013 +0100
@@ -425,8 +425,13 @@
definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
where [simp, code del]: "abort _ f = f ()"
+lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
+by simp
+
setup {* Sign.map_naming Name_Space.parent_path *}
+setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *}
+
code_printing constant Code.abort \<rightharpoonup>
(SML) "!(raise/ Fail/ _)"
and (OCaml) "failwith"
--- a/src/HOL/Tools/Lifting/lifting_def.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Mon Nov 11 18:37:56 2013 +0100
@@ -50,7 +50,15 @@
SOME (Goal.prove ctxt [] [] prop (fn {context, ...} => refl_tac context 1))
handle ERROR _ => NONE
-(* Generation of a transfer rule *)
+(*
+ Generates a parametrized transfer rule.
+ transfer_rule - of the form T t f
+ parametric_transfer_rule - of the form par_R t' t
+
+ Result: par_T t' f, after substituing op= for relations in par_T that relate
+ a type constructor to the same type constructor, it is a merge of (par_R' OO T) t' f
+ using Lifting_Term.merge_transfer_relations
+*)
fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
let
@@ -400,6 +408,7 @@
rhs - a term representing the new constant on the raw level
rsp_thm - a respectfulness theorem in the internal tagged form (like '(R ===> R ===> R) f f'),
i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
+ par_thms - a parametricity theorem for rhs
*)
fun add_lift_def var qty rhs rsp_thm par_thms lthy =
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 11 18:37:56 2013 +0100
@@ -477,6 +477,7 @@
quot_thm - a quotient theorem (Quotient R Abs Rep T)
opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
(in the form "reflp R")
+ opt_par_thm - a parametricity theorem for R
*)
fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
@@ -758,7 +759,11 @@
fun setup_typedef () =
case opt_reflp_xthm of
SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used."
- | NONE => setup_by_typedef_thm gen_code input_thm lthy
+ | NONE => (
+ case opt_par_xthm of
+ SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used."
+ | NONE => setup_by_typedef_thm gen_code input_thm lthy
+ )
in
case input_term of
(Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient ()
@@ -848,6 +853,10 @@
@ (map (Pretty.string_of o Pretty.item o single) errs)))
end
+(*
+ Registers the data in qinfo in the Lifting infrastructure.
+*)
+
fun lifting_restore qinfo ctxt =
let
val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo
--- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Nov 11 18:37:56 2013 +0100
@@ -289,9 +289,17 @@
quot_thm
end
+(*
+ Computes the composed abstraction function for rty and qty.
+*)
+
fun abs_fun ctxt (rty, qty) =
quot_thm_abs (prove_quot_thm ctxt (rty, qty))
+(*
+ Computes the composed equivalence relation for rty and qty.
+*)
+
fun equiv_relation ctxt (rty, qty) =
quot_thm_rel (prove_quot_thm ctxt (rty, qty))
@@ -324,6 +332,16 @@
end
end
+(*
+ For the given type, it proves a composed Quotient map theorem, where for each type variable
+ extra Quotient assumption is generated. E.g., for 'a list it generates exactly
+ the Quotient map theorem for the list type. The function generalizes this for the whole
+ type universe. New fresh variables in the assumptions are fixed in the returned context.
+
+ Returns: the composed Quotient map theorem and list mapping each type variable in ty
+ to the corresponding assumption in the returned theorem.
+*)
+
fun prove_param_quot_thm ctxt ty =
let
fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) =
@@ -360,6 +378,13 @@
end
handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg)
+(*
+ It computes a parametrized relator for the given type ty. E.g., for 'a dlist:
+ list_all2 ?R OO cr_dlist with parameters [?R].
+
+ Returns: the definitional term and list of parameters (relations).
+*)
+
fun generate_parametrized_relator ctxt ty =
let
val orig_ctxt = ctxt
@@ -412,6 +437,15 @@
map_interrupt' f l []
end
in
+
+ (*
+ ctm - of the form (par_R OO T) t f, where par_R is a parametricity transfer relation for t
+ and T is a transfer relation between t and f.
+
+ The function merges par_R OO T using definitions of parametrized correspondence relations
+ (e.g., rel_T R OO cr_T == pcr_T R).
+ *)
+
fun merge_transfer_relations ctxt ctm =
let
val ctm = Thm.dest_arg ctm
@@ -488,6 +522,14 @@
handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
end
+(*
+ It replaces cr_T by pcr_T op= in the transfer relation. For composed
+ abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized
+ correspondce relation does not exist, the original relation is kept.
+
+ thm - a transfer rule
+*)
+
fun parametrize_transfer_rule ctxt thm =
let
fun parametrize_relation_conv ctm =
--- a/src/Pure/Concurrent/future.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Mon Nov 11 18:37:56 2013 +0100
@@ -68,6 +68,7 @@
val join_result: 'a future -> 'a Exn.result
val joins: 'a future list -> 'a list
val join: 'a future -> 'a
+ val join_tasks: task list -> unit
val value_result: 'a Exn.result -> 'a future
val value: 'a -> 'a future
val cond_forks: params -> (unit -> 'a) list -> 'a future list
@@ -76,6 +77,7 @@
val promise: (unit -> unit) -> 'a future
val fulfill_result: 'a future -> 'a Exn.result -> unit
val fulfill: 'a future -> 'a -> unit
+ val group_snapshot: group -> task list
val terminate: group -> unit
val shutdown: unit -> unit
end;
@@ -575,6 +577,14 @@
fun joins xs = Par_Exn.release_all (join_results xs);
fun join x = Exn.release (join_result x);
+fun join_tasks tasks =
+ if null tasks then ()
+ else
+ (singleton o forks)
+ {name = "join_tasks", group = SOME (new_group NONE),
+ deps = tasks, pri = 0, interrupts = false} I
+ |> join;
+
(* fast-path operations -- bypass task queue if possible *)
@@ -663,22 +673,20 @@
fun fulfill x res = fulfill_result x (Exn.Res res);
+(* group snapshot *)
+
+fun group_snapshot group =
+ SYNCHRONIZED "group_snapshot" (fn () =>
+ Task_Queue.group_tasks (! queue) group);
+
+
(* terminate *)
fun terminate group =
- let
- val tasks =
- SYNCHRONIZED "terminate" (fn () =>
- let val _ = cancel_group_unsynchronized group;
- in Task_Queue.group_tasks (! queue) group end);
- in
- if null tasks then ()
- else
- (singleton o forks)
- {name = "terminate", group = SOME (new_group NONE),
- deps = tasks, pri = 0, interrupts = false} I
- |> join
- end;
+ SYNCHRONIZED "terminate" (fn () =>
+ let val _ = cancel_group_unsynchronized group;
+ in Task_Queue.group_tasks (! queue) group end)
+ |> join_tasks;
(* shutdown *)
--- a/src/Pure/GUI/gui.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/GUI/gui.scala Mon Nov 11 18:37:56 2013 +0100
@@ -168,10 +168,11 @@
def font_metrics(font: Font): LineMetrics =
font.getLineMetrics("", new FontRenderContext(null, false, false))
- def imitate_font(family: String, font: Font): Font =
+ def imitate_font(family: String, font: Font, scale: Double = 1.0): Font =
{
val font1 = new Font(family, font.getStyle, font.getSize)
- font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
+ val size = scale * (font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
+ font1.deriveFont(size.round.toInt)
}
def transform_font(font: Font, transform: AffineTransform): Font =
--- a/src/Pure/GUI/system_dialog.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/GUI/system_dialog.scala Mon Nov 11 18:37:56 2013 +0100
@@ -1,5 +1,4 @@
/* Title: Pure/GUI/system_dialog.scala
- Module: PIDE-GUI
Author: Makarius
Dialog for system processes, with optional output window.
--- a/src/Pure/General/socket_io.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/General/socket_io.ML Mon Nov 11 18:37:56 2013 +0100
@@ -25,7 +25,7 @@
val rd =
BinPrimIO.RD {
name = name,
- chunkSize = Socket.Ctl.getRCVBUF socket,
+ chunkSize = io_buffer_size,
readVec = SOME (fn n => Socket.recvVec (socket, n)),
readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
readVecNB = NONE,
@@ -44,7 +44,7 @@
val wr =
BinPrimIO.WR {
name = name,
- chunkSize = Socket.Ctl.getSNDBUF socket,
+ chunkSize = io_buffer_size,
writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
writeVecNB = NONE,
@@ -81,6 +81,7 @@
| _ => err ());
val socket: Socket.active INetSock.stream_sock = INetSock.TCP.socket ();
val _ = Socket.connect (socket, INetSock.toAddr (NetHostDB.addr host, port));
+ val _ = INetSock.TCP.setNODELAY (socket, true);
in make_streams socket end;
end;
--- a/src/Pure/ML-Systems/polyml.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Mon Nov 11 18:37:56 2013 +0100
@@ -51,6 +51,8 @@
val raw_explode = SML90.explode;
val implode = SML90.implode;
+val io_buffer_size = 4096;
+
fun quit () = exit 0;
--- a/src/Pure/ML-Systems/smlnj.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Mon Nov 11 18:37:56 2013 +0100
@@ -3,6 +3,7 @@
Compatibility file for Standard ML of New Jersey.
*)
+val io_buffer_size = 4096;
use "ML-Systems/proper_int.ML";
exception Interrupt;
--- a/src/Pure/PIDE/document.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/PIDE/document.scala Mon Nov 11 18:37:56 2013 +0100
@@ -416,7 +416,7 @@
case Some(st) =>
val command = st.command
val node = version.nodes(command.node_name)
- Some((node, command))
+ if (node.commands.contains(command)) Some((node, command)) else None
}
def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
--- a/src/Pure/PIDE/query_operation.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/PIDE/query_operation.scala Mon Nov 11 18:37:56 2013 +0100
@@ -53,8 +53,12 @@
private def remove_overlay()
{
- current_location.foreach(command =>
- editor.remove_overlay(command, operation_name, instance :: current_query))
+ current_location match {
+ case None =>
+ case Some(command) =>
+ editor.remove_overlay(command, operation_name, instance :: current_query)
+ editor.flush()
+ }
}
@@ -129,10 +133,8 @@
if (current_status != new_status) {
current_status = new_status
consume_status(new_status)
- if (new_status == Query_Operation.Status.REMOVED) {
+ if (new_status == Query_Operation.Status.REMOVED)
remove_overlay()
- editor.flush()
- }
}
}
}
@@ -153,13 +155,15 @@
remove_overlay()
reset_state()
consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
- editor.current_command(editor_context, snapshot) match {
- case Some(command) =>
- current_location = Some(command)
- current_query = query
- current_status = Query_Operation.Status.WAITING
- editor.insert_overlay(command, operation_name, instance :: query)
- case None =>
+ if (!snapshot.is_outdated) {
+ editor.current_command(editor_context, snapshot) match {
+ case Some(command) =>
+ current_location = Some(command)
+ current_query = query
+ current_status = Query_Operation.Status.WAITING
+ editor.insert_overlay(command, operation_name, instance :: query)
+ case None =>
+ }
}
consume_status(current_status)
editor.flush()
@@ -206,5 +210,8 @@
def deactivate() {
editor.session.commands_changed -= main_actor
remove_overlay()
+ reset_state()
+ consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
+ consume_status(current_status)
}
}
--- a/src/Pure/System/options.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/System/options.scala Mon Nov 11 18:37:56 2013 +0100
@@ -162,7 +162,10 @@
{
override def toString: String = options.iterator.mkString("Options (", ",", ")")
- def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
+ private def print_opt(opt: Options.Opt): String =
+ if (opt.public) "public " + opt.print else opt.print
+
+ def print: String = cat_lines(options.toList.sortBy(_._1).map(p => print_opt(p._2)))
def description(name: String): String = check_name(name).description
--- a/src/Pure/System/system_channel.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/System/system_channel.ML Mon Nov 11 18:37:56 2013 +0100
@@ -68,7 +68,9 @@
in
System_Channel
{input_line = fn () => read_line in_stream,
- inputN = fn n => Byte.bytesToString (BinIO.inputN (in_stream, n)),
+ inputN = fn n =>
+ if n = 0 then "" (*workaround for polyml-5.5.1 or earlier*)
+ else Byte.bytesToString (BinIO.inputN (in_stream, n)),
output = fn s => BinIO.output (out_stream, Byte.stringToBytes s),
flush = fn () => BinIO.flushOut out_stream}
end;
--- a/src/Pure/System/system_channel.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/System/system_channel.scala Mon Nov 11 18:37:56 2013 +0100
@@ -15,7 +15,7 @@
object System_Channel
{
- def apply(use_socket: Boolean = false): System_Channel =
+ def apply(): System_Channel =
if (Platform.is_windows) new Socket_Channel else new Fifo_Channel
}
@@ -86,6 +86,7 @@
def rendezvous(): (OutputStream, InputStream) =
{
val socket = server.accept
+ socket.setTcpNoDelay(true)
(socket.getOutputStream, socket.getInputStream)
}
--- a/src/Pure/Thy/html.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/Thy/html.scala Mon Nov 11 18:37:56 2013 +0100
@@ -1,4 +1,5 @@
/* Title: Pure/Thy/html.scala
+ Module: PIDE-GUI
Author: Makarius
HTML presentation elements.
--- a/src/Pure/Thy/thy_info.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Nov 11 18:37:56 2013 +0100
@@ -177,9 +177,12 @@
fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i);
fun join_theory (Result {theory, exec_id, ...}) =
- Exn.capture Thm.join_theory_proofs theory ::
- map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id));
-
+ let
+ (*toplevel proofs and diags*)
+ val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id));
+ (*fully nested proofs*)
+ val res = Exn.capture Thm.join_theory_proofs theory;
+ in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end;
datatype task =
Task of string list * (theory list -> result) |
@@ -236,7 +239,7 @@
val results3 = futures
|> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ());
- (* FIXME avoid global reset_futures (!??) *)
+ (* FIXME avoid global Execution.reset (!??) *)
val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ()));
val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4);
--- a/src/Pure/Tools/main.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Pure/Tools/main.scala Mon Nov 11 18:37:56 2013 +0100
@@ -225,11 +225,17 @@
val update =
{
val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
+ val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
val upd =
if (Platform.is_windows)
- List("ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home), "INI_DIR" -> "")
+ List(
+ "ISABELLE_HOME" -> Isabelle_System.jvm_path(isabelle_home),
+ "ISABELLE_HOME_USER" -> Isabelle_System.jvm_path(isabelle_home_user),
+ "INI_DIR" -> "")
else
- List("ISABELLE_HOME" -> isabelle_home)
+ List(
+ "ISABELLE_HOME" -> isabelle_home,
+ "ISABELLE_HOME_USER" -> isabelle_home_user)
(env0: Any) => {
val env = env0.asInstanceOf[java.util.Map[String, String]]
--- a/src/Tools/Code/code_target.ML Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/Code/code_target.ML Mon Nov 11 18:37:56 2013 +0100
@@ -639,12 +639,13 @@
val set_identifiers = gen_set_identifiers cert_name_decls;
val set_identifiers_cmd = gen_set_identifiers read_name_decls;
-fun add_module_alias_cmd target aliasses =
+fun add_module_alias_cmd target aliasses thy =
let
val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\"";
in
fold (fn (sym, name) => set_identifier
- (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))) aliasses
+ (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name))))
+ aliasses thy
end;
--- a/src/Tools/jEdit/etc/options Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/etc/options Mon Nov 11 18:37:56 2013 +0100
@@ -42,6 +42,9 @@
public option jedit_completion_delay : real = 0.0
-- "delay for completion popup (seconds)"
+public option jedit_completion_dismiss_delay : real = 0.0
+ -- "delay for dismissing obsolete completion popup (seconds)"
+
public option jedit_completion_immediate : bool = false
-- "insert unique completion immediately into buffer (if delay = 0)"
--- a/src/Tools/jEdit/etc/settings Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/etc/settings Mon Nov 11 18:37:56 2013 +0100
@@ -7,7 +7,7 @@
#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
-JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dscala.repl.no-threads=true"
+JEDIT_SYSTEM_OPTIONS="-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dscala.repl.no-threads=true"
ISABELLE_JEDIT_OPTIONS=""
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Nov 11 18:37:56 2013 +0100
@@ -488,11 +488,18 @@
list_view.requestFocus
}
+ private val hide_popup_delay =
+ Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
+ popup.hide
+ }
+
private def hide_popup()
{
- val had_focus = list_view.peer.isFocusOwner
- popup.hide
- if (had_focus) refocus()
+ if (list_view.peer.isFocusOwner) refocus()
+
+ if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero)
+ popup.hide
+ else hide_popup_delay.invoke()
}
}
--- a/src/Tools/jEdit/src/document_model.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Nov 11 18:37:56 2013 +0100
@@ -100,10 +100,11 @@
Swing_Thread.require()
if (Isabelle.continuous_checking) {
+ val snapshot = this.snapshot()
Document.Node.Perspective(node_required, Text.Perspective(
for {
doc_view <- PIDE.document_views(buffer)
- range <- doc_view.perspective().ranges
+ range <- doc_view.perspective(snapshot).ranges
} yield range), PIDE.editor.node_overlays(node_name))
}
else empty_perspective
--- a/src/Tools/jEdit/src/document_view.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Mon Nov 11 18:37:56 2013 +0100
@@ -77,14 +77,25 @@
/* perspective */
- def perspective(): Text.Perspective =
+ def perspective(snapshot: Document.Snapshot): Text.Perspective =
{
Swing_Thread.require()
- val active_caret =
- if (text_area.getView != null && text_area.getView.getTextArea == text_area)
- List(JEdit_Lib.point_range(model.buffer, text_area.getCaretPosition))
+ val active_command =
+ {
+ val view = text_area.getView
+ if (view != null && view.getTextArea == text_area) {
+ PIDE.editor.current_command(view, snapshot) match {
+ case Some(command) =>
+ snapshot.node.command_start(command) match {
+ case Some(start) => List(command.proper_range + start)
+ case None => Nil
+ }
+ case None => Nil
+ }
+ }
else Nil
+ }
val buffer_range = JEdit_Lib.buffer_range(model.buffer)
val visible_lines =
@@ -98,7 +109,7 @@
}
yield range).toList
- Text.Perspective(active_caret ::: visible_lines)
+ Text.Perspective(active_command ::: visible_lines)
}
private def update_perspective = new TextAreaExtension
--- a/src/Tools/jEdit/src/find_dockable.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala Mon Nov 11 18:37:56 2013 +0100
@@ -105,7 +105,11 @@
}
private val query_label = new Label("Search criteria:") {
- tooltip = "Search criteria for find operation"
+ tooltip =
+ GUI.tooltip_lines(List(
+ "Search criteria for find operation, e.g.",
+ "",
+ " \"_ = _\" \"op +\" name: Group -name: monoid"))
}
private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
@@ -117,7 +121,7 @@
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
setToolTipText(query_label.tooltip)
- setFont(GUI.imitate_font(Rendering.font_family(), getFont))
+ setFont(GUI.imitate_font(Rendering.font_family(), getFont, 1.2))
}
private case class Context_Entry(val name: String, val description: String)
--- a/src/Tools/jEdit/src/jEdit.props Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Mon Nov 11 18:37:56 2013 +0100
@@ -9,6 +9,7 @@
buffer.sidekick.keystroke-parse=false
buffer.tabSize=2
close-docking-area.shortcut2=C+e C+CIRCUMFLEX
+complete-word.shortcut=
console.dock-position=floating
console.encoding=UTF-8
console.font=IsabelleText
@@ -190,8 +191,8 @@
isabelle-sledgehammer.dock-position=bottom
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
-isabelle.complete.label=Complete text
-isabelle.complete.shortcut=C+b
+isabelle.complete.label=Complete Isabelle text
+isabelle.complete.shortcut2=C+b
isabelle.control-bold.label=Control bold
isabelle.control-bold.shortcut=C+e RIGHT
isabelle.control-reset.label=Control reset
@@ -211,7 +212,6 @@
isabelle.increase-font-size2.shortcut=C+EQUALS
isabelle.reset-continuous-checking.label=Reset continuous checking
isabelle.reset-font-size.label=Reset font size
-isabelle.reset-font-size.shortcut=C+0
isabelle.reset-node-required.label=Reset node required
isabelle.set-continuous-checking.label=Set continuous checking
isabelle.set-node-required.label=Set node required
--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Nov 11 18:37:56 2013 +0100
@@ -66,24 +66,21 @@
{
Swing_Thread.require()
- if (snapshot.is_outdated) None
- else {
- val text_area = view.getTextArea
- PIDE.document_view(text_area) match {
- case Some(doc_view) =>
- val node = snapshot.version.nodes(doc_view.model.node_name)
- val caret = text_area.getCaretPosition
- if (caret < text_area.getBuffer.getLength) {
- val caret_commands = node.command_range(caret)
- if (caret_commands.hasNext) {
- val (cmd0, _) = caret_commands.next
- node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
- }
- else None
+ val text_area = view.getTextArea
+ PIDE.document_view(text_area) match {
+ case Some(doc_view) =>
+ val node = snapshot.version.nodes(doc_view.model.node_name)
+ val caret = snapshot.revert(text_area.getCaretPosition)
+ if (caret < text_area.getBuffer.getLength) {
+ val caret_commands = node.command_range(caret)
+ if (caret_commands.hasNext) {
+ val (cmd0, _) = caret_commands.next
+ node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
}
- else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
- case None => None
- }
+ else None
+ }
+ else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
+ case None => None
}
}
--- a/src/Tools/jEdit/src/plugin.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Mon Nov 11 18:37:56 2013 +0100
@@ -228,26 +228,6 @@
}
- /* Mac OS X application hooks */
-
- def handleQuit(): Boolean =
- {
- jEdit.exit(jEdit.getActiveView(), true)
- false
- }
-
- def handlePreferences()
- {
- CombinedOptions.combinedOptions(jEdit.getActiveView())
- }
-
- def handleAbout(): Boolean =
- {
- new AboutDialog(jEdit.getActiveView())
- true
- }
-
-
/* main plugin plumbing */
override def handleMessage(message: EBMessage)
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Nov 11 18:37:56 2013 +0100
@@ -115,13 +115,13 @@
deactivate()
hierarchy(tip) match {
case Some((old, _ :: rest)) =>
- old.foreach(_.hide_popup)
- tip.hide_popup
- stack = rest
rest match {
case top :: _ => top.request_focus
case Nil => JEdit_Lib.request_focus_view
}
+ old.foreach(_.hide_popup)
+ tip.hide_popup
+ stack = rest
case _ =>
}
}
@@ -131,9 +131,9 @@
deactivate()
if (stack.isEmpty) false
else {
+ JEdit_Lib.request_focus_view
stack.foreach(_.hide_popup)
stack = Nil
- JEdit_Lib.request_focus_view
true
}
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Nov 11 18:25:13 2013 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Nov 11 18:37:56 2013 +0100
@@ -136,7 +136,11 @@
}
private val provers_label = new Label("Provers:") {
- tooltip = "Automatic provers as space-separated list (e.g. \"e spass remote_vampire\")"
+ tooltip =
+ GUI.tooltip_lines(List(
+ "Automatic provers as space-separated list, e.g.",
+ "",
+ " e spass remote_vampire"))
}
private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {