# HG changeset patch # User wenzelm # Date 1384191476 -3600 # Node ID 27246f8b2dac6bd513c14d1007646eb6f8cdaa99 # Parent 4f55054d197c3d81e4fb012cdf5c9281655bbfc8# Parent 50199af40c27cb525417e5fa637931d0ab0063b0 merged diff -r 4f55054d197c -r 27246f8b2dac .hgtags --- 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 diff -r 4f55054d197c -r 27246f8b2dac Admin/Linux/Isabelle --- 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 "$@" - diff -r 4f55054d197c -r 27246f8b2dac Admin/Linux/Isabelle.c --- /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 +#include +#include +#include +#include + + +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"); +} + diff -r 4f55054d197c -r 27246f8b2dac Admin/Linux/Isabelle.run --- /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 "$@" + diff -r 4f55054d197c -r 27246f8b2dac Admin/Linux/build --- /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 + diff -r 4f55054d197c -r 27246f8b2dac Admin/components/bundled-linux --- /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 diff -r 4f55054d197c -r 27246f8b2dac Admin/components/components.sha1 --- 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 diff -r 4f55054d197c -r 27246f8b2dac Admin/components/main --- 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 diff -r 4f55054d197c -r 27246f8b2dac Admin/lib/Tools/makedist_bundle --- 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"' diff -r 4f55054d197c -r 27246f8b2dac CONTRIBUTORS --- 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. diff -r 4f55054d197c -r 27246f8b2dac NEWS --- 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 diff -r 4f55054d197c -r 27246f8b2dac etc/settings --- 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" diff -r 4f55054d197c -r 27246f8b2dac src/Doc/IsarRef/Document_Preparation.thy --- 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} diff -r 4f55054d197c -r 27246f8b2dac src/Doc/IsarRef/HOL_Specific.thy --- 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 \}. 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_\}, its inverse @{text abs_\} 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 \ (x = int n)"}, corresponding transfer rules and the theorem + @{text "\x::int \ {0..}. x < x + 1"}, the attribute would prove + @{text "\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 \ (list_all2 A ===> op =) distinct distinct"}\\ @{text "\bi_unique A; bi_unique B\ \ 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 \ (x = int n)"}, + one can register the following transfer domain rule: + @{text "Domainp ZN = (\x. x \ 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 \ + 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 \ local_theory"}\\ @{command_def (HOL) "lift_definition"} & : & @{text "local_theory \ proof(prove)"}\\ + @{command_def (HOL) "lifting_forget"} & : & @{text "local_theory \ local_theory"}\\ + @{command_def (HOL) "lifting_update"} & : & @{text "local_theory \ local_theory"}\\ @{command_def (HOL) "print_quot_maps"} & : & @{text "context \"}\\ @{command_def (HOL) "print_quotients"} & : & @{text "context \"}\\ @{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 :: \ 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 :: \"} @{keyword (HOL) "is"} @{text t} Defines a new function @{text f} with an abstract type @{text \} 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 :: \"}, then + the command builds a term @{text "F"} as a corresponding combination of abstraction + and representation functions such that @{text "F :: \ \ \" } and + defines @{text f} is as @{text "f \ 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 "\"} by + @{command_def (HOL) "lift_definition"}, the package defines a new bundle + that is called @{text "\.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 "\.lifting"}. + + The command @{command (HOL) "lifting_forget"} @{text "\.lifting"} deletes set-up of the Lifting + package + for @{text \} and deletes all the transfer rules that were introduced + by @{command (HOL) "lift_definition"} using @{text \} 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 \ + 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 \ B \ list_all2 A \ 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 \\ list_all2 S = list_all2 (R \\ 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 \} (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 \}. E.g., for @{text "'a dlist"}, @{text pcr_def} is + @{text "pcr_dlist A \ list_all2 A \\ 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 \.lifting} + together with the commands @{command (HOL) lifting_forget} and @{command (HOL) lifting_update} is + preferred for normal usage. + \end{description} *} diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/Base.thy --- 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" diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/JEdit.thy --- 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 "\"} that both produce the + Isabelle symbol @{text "\"} 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 "\"}, @{text "\"}, @{text "\"}, @{text "\"} \\ - @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} \\ - @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} \\ - @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} \\ - @{verbatim "\"}, @{verbatim "\"}, @{verbatim "\"}, @{text "\"} \\ + \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 "\"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\ - @{text "\"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\ - @{text "\"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\ + \item Completion of syntax keywords requires at least 3 relevant + characters in the text. - @{text "\"} & @{verbatim "!!"} & @{verbatim "\\And"} \\ - @{text "\"} & @{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 "\"} & @{verbatim "!"} & @{verbatim "\\forall"} \\ - @{text "\"} & @{verbatim "?"} & @{verbatim "\\exists"} \\ - @{text "\"} & @{verbatim "-->"} & @{verbatim "\\longrightarrow"} \\ - @{text "\"} & @{verbatim "&"} & @{verbatim "\\and"} \\ - @{text "\"} & @{verbatim "|"} & @{verbatim "\\or"} \\ - @{text "\"} & @{verbatim "~"} & @{verbatim "\\not"} \\ - @{text "\"} & @{verbatim "~="} & @{verbatim "\\noteq"} \\ - @{text "\"} & @{verbatim ":"} & @{verbatim "\\in"} \\ - @{text "\"} & @{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 "\"}''. + + For the editor front-end, a certain subset of symbols is rendered + physically via Unicode glyphs, in order to show ``@{verbatim "\"}'' + as ``@{text "\"}'', 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 "\"}''. 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 "\"}'' will be shown in the text buffer + instead of its Unicode rendering ``@{text "\"}''. 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 "\"}, 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 "\"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\ + @{text "\"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\ + @{text "\"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex] + @{text "\"} & @{verbatim "\\And"} & @{verbatim "!!"} \\ + @{text "\"} & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex] + @{text "\"} & @{verbatim "\\forall"} & @{verbatim "!"} \\ + @{text "\"} & @{verbatim "\\exists"} & @{verbatim "?"} \\ + @{text "\"} & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\ + @{text "\"} & @{verbatim "\\and"} & @{verbatim "&"} \\ + @{text "\"} & @{verbatim "\\or"} & @{verbatim "|"} \\ + @{text "\"} & @{verbatim "\\not"} & @{verbatim "~"} \\ + @{text "\"} & @{verbatim "\\noteq"} & @{verbatim "~="} \\ + @{text "\"} & @{verbatim "\\in"} & @{verbatim ":"} \\ + @{text "\"} & @{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 "\"} & superscript & @{verbatim "C+e UP"} \\ - @{verbatim "\"} & subscript & @{verbatim "C+e DOWN"} \\ - @{verbatim "\"} & 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 "\"} that both produce the Isabelle - symbol @{text "\"} 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} *} diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/document/auto-tools.png Binary file src/Doc/JEdit/document/auto-tools.png has changed diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/document/find.png Binary file src/Doc/JEdit/document/find.png has changed diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/document/output.png Binary file src/Doc/JEdit/document/output.png has changed diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/document/popup1.png Binary file src/Doc/JEdit/document/popup1.png has changed diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/document/popup2.png Binary file src/Doc/JEdit/document/popup2.png has changed diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/document/root.tex --- 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} diff -r 4f55054d197c -r 27246f8b2dac src/Doc/JEdit/document/sledgehammer.png Binary file src/Doc/JEdit/document/sledgehammer.png has changed diff -r 4f55054d197c -r 27246f8b2dac src/Doc/ROOT --- 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 + diff -r 4f55054d197c -r 27246f8b2dac src/Doc/System/Sessions.thy --- 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. diff -r 4f55054d197c -r 27246f8b2dac src/Doc/antiquote_setup.ML --- 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 #> diff -r 4f55054d197c -r 27246f8b2dac src/Doc/manual.bib --- 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", diff -r 4f55054d197c -r 27246f8b2dac src/HOL/BNF/Tools/coinduction.ML --- 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 diff -r 4f55054d197c -r 27246f8b2dac src/HOL/Quotient_Examples/FSet.thy --- 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 diff -r 4f55054d197c -r 27246f8b2dac src/HOL/String.thy --- 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 \ (unit \ 'a) \ '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 \ (SML) "!(raise/ Fail/ _)" and (OCaml) "failwith" diff -r 4f55054d197c -r 27246f8b2dac src/HOL/Tools/Lifting/lifting_def.ML --- 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 = diff -r 4f55054d197c -r 27246f8b2dac src/HOL/Tools/Lifting/lifting_setup.ML --- 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 diff -r 4f55054d197c -r 27246f8b2dac src/HOL/Tools/Lifting/lifting_term.ML --- 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 = diff -r 4f55054d197c -r 27246f8b2dac src/Pure/Concurrent/future.ML --- 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 *) diff -r 4f55054d197c -r 27246f8b2dac src/Pure/GUI/gui.scala --- 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 = diff -r 4f55054d197c -r 27246f8b2dac src/Pure/GUI/system_dialog.scala --- 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. diff -r 4f55054d197c -r 27246f8b2dac src/Pure/General/socket_io.ML --- 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; diff -r 4f55054d197c -r 27246f8b2dac src/Pure/ML-Systems/polyml.ML --- 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; diff -r 4f55054d197c -r 27246f8b2dac src/Pure/ML-Systems/smlnj.ML --- 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; diff -r 4f55054d197c -r 27246f8b2dac src/Pure/PIDE/document.scala --- 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) diff -r 4f55054d197c -r 27246f8b2dac src/Pure/PIDE/query_operation.scala --- 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) } } diff -r 4f55054d197c -r 27246f8b2dac src/Pure/System/options.scala --- 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 diff -r 4f55054d197c -r 27246f8b2dac src/Pure/System/system_channel.ML --- 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; diff -r 4f55054d197c -r 27246f8b2dac src/Pure/System/system_channel.scala --- 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) } diff -r 4f55054d197c -r 27246f8b2dac src/Pure/Thy/html.scala --- 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. diff -r 4f55054d197c -r 27246f8b2dac src/Pure/Thy/thy_info.ML --- 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); diff -r 4f55054d197c -r 27246f8b2dac src/Pure/Tools/main.scala --- 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]] diff -r 4f55054d197c -r 27246f8b2dac src/Tools/Code/code_target.ML --- 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; diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/etc/options --- 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)" diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/etc/settings --- 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="" diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/completion_popup.scala --- 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() } } diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/document_model.scala --- 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 diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/document_view.scala --- 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 diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/find_dockable.scala --- 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) diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/jEdit.props --- 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 diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/jedit_editor.scala --- 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 } } diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/plugin.scala --- 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) diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/pretty_tooltip.scala --- 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 } } diff -r 4f55054d197c -r 27246f8b2dac src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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") {