# HG changeset patch # User wenzelm # Date 1403962530 -7200 # Node ID 2f4948579905085b12b3d1710a4aa046e2fa0e7b # Parent 2b8b1a8587da30415a325ecab7e41e34d8d8eb14# Parent 94081154306d8b91be5f834a23bb12c20fe3fcce merged diff -r 2b8b1a8587da -r 2f4948579905 src/Doc/Implementation/Integration.thy --- a/src/Doc/Implementation/Integration.thy Sat Jun 28 11:44:22 2014 +0200 +++ b/src/Doc/Implementation/Integration.thy Sat Jun 28 15:35:30 2014 +0200 @@ -96,12 +96,9 @@ subsection {* Toplevel transitions \label{sec:toplevel-transition} *} text {* - An Isar toplevel transition consists of a partial function on the - toplevel state, with additional information for diagnostics and - error reporting: there are fields for command name, source position, - optional source text, as well as flags for interactive-only commands - (which issue a warning in batch-mode), printing of result state, - etc. + An Isar toplevel transition consists of a partial function on the toplevel + state, with additional information for diagnostics and error reporting: + there are fields for command name, source position, and other meta-data. The operational part is represented as the sequential union of a list of partial functions, which are tried in turn until the first @@ -145,8 +142,9 @@ \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global goal function, which turns a theory into a proof state. The theory may be changed before entering the proof; the generic Isar goal - setup includes an argument that specifies how to apply the proven - result to the theory, when the proof is finished. + setup includes an @{verbatim after_qed} argument that specifies how to + apply the proven result to the enclosing context, when the proof + is finished. \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic proof command, with a singleton result. diff -r 2b8b1a8587da -r 2f4948579905 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Sat Jun 28 11:44:22 2014 +0200 +++ b/src/Doc/Implementation/ML.thy Sat Jun 28 15:35:30 2014 +0200 @@ -16,8 +16,8 @@ infrastructure with library modules to address the needs of this difficult task. For example, the raw parallel programming model of Poly/ML is presented as considerably more abstract concept of - \emph{future values}, which is then used to augment the inference - kernel, proof interpreter, and theory loader accordingly. + \emph{futures}, which is then used to augment the inference + kernel, Isar theory and proof interpreter, and PIDE document management. The main aspects of Isabelle/ML are introduced below. These first-hand explanations should help to understand how proper @@ -92,8 +92,8 @@ \end{verbatim} As in regular typography, there is some extra space \emph{before} - section headings that are adjacent to plain text (not other headings - as in the example above). + section headings that are adjacent to plain text, bit not other headings + as in the example above. \medskip The precise wording of the prose text given in these headings is chosen carefully to introduce the main theme of the @@ -141,7 +141,7 @@ structures are not ``opened'', but names are referenced with explicit qualification, as in @{ML Syntax.string_of_term} for example. When devising names for structures and their components it - is important aim at eye-catching compositions of both parts, because + is important to aim at eye-catching compositions of both parts, because this is how they are seen in the sources and documentation. For the same reasons, aliases of well-known library functions should be avoided. @@ -191,15 +191,12 @@ \item A function that maps @{ML_text foo} to @{ML_text bar} is called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never - @{ML_text foo2bar}, @{ML_text bar_from_foo}, @{ML_text - bar_for_foo}, or @{ML_text bar4foo}). + @{ML_text foo2bar}, nor @{ML_text bar_from_foo}, nor @{ML_text + bar_for_foo}, nor @{ML_text bar4foo}). \item The name component @{ML_text legacy} means that the operation is about to be discontinued soon. - \item The name component @{ML_text old} means that this is historic - material that might disappear at some later stage. - \item The name component @{ML_text global} means that this works with the background theory instead of the regular local context (\secref{sec:context}), sometimes for historical reasons, sometimes @@ -221,8 +218,7 @@ \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text context} (never @{ML_text ctx}) - \item generic contexts are called @{ML_text context}, rarely - @{ML_text ctxt} + \item generic contexts are called @{ML_text context} \item local theories are called @{ML_text lthy}, except for local theories that are treated as proof context (which is a semantic @@ -233,8 +229,8 @@ Variations with primed or decimal numbers are always possible, as well as semantic prefixes like @{ML_text foo_thy} or @{ML_text bar_ctxt}, but the base conventions above need to be preserved. - This allows to visualize the their data flow via plain regular - expressions in the editor. + This allows to emphasize their data flow via plain regular + expressions in the text editor. \item The main logical entities (\secref{ch:logic}) have established naming convention as follows: @@ -280,18 +276,23 @@ Note that the goal state @{ML_text st} above is rarely made explicit, if tactic combinators (tacticals) are used as usual. + A tactic that requires a proof context needs to make that explicit as seen + in the @{verbatim ctxt} argument above. Do not refer to the background + theory of @{verbatim st} -- it is not a proper context, but merely a formal + certificate. + \end{itemize} *} subsection {* General source layout *} -text {* The general Isabelle/ML source layout imitates regular - type-setting to some extent, augmented by the requirements for - deeply nested expressions that are commonplace in functional - programming. - - \paragraph{Line length} is 80 characters according to ancient +text {* + The general Isabelle/ML source layout imitates regular type-setting + conventions, augmented by the requirements for deeply nested expressions + that are commonplace in functional programming. + + \paragraph{Line length} is limited to 80 characters according to ancient standards, but we allow as much as 100 characters (not more).\footnote{Readability requires to keep the beginning of a line in view while watching its end. Modern wide-screen displays do not @@ -344,7 +345,7 @@ of a type-writer to certain predefined positions. In software they could be used as a primitive run-length compression of consecutive spaces, but the precise result would depend on non-standardized - editor configuration.} + text editor configuration.} Each level of nesting is indented by 2 spaces, sometimes 1, very rarely 4, never 8 or any other odd number. @@ -389,7 +390,7 @@ syntax of Standard ML is quite ambitious and admits a lot of variance that can distort the meaning of the text. - Clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle}, + Multiple clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle}, @{ML_text case} get extra indentation to indicate the nesting clearly. Example: @@ -445,15 +446,15 @@ Extra parentheses around @{ML_text case} expressions are optional, but help to analyse the nesting based on character matching in the - editor. + text editor. \medskip There are two main exceptions to the overall principle of compositionality in the layout of complex expressions. \begin{enumerate} - \item @{ML_text "if"} expressions are iterated as if there would be - a multi-branch conditional in SML, e.g. + \item @{ML_text "if"} expressions are iterated as if ML had multi-branch + conditionals, e.g. \begin{verbatim} (* RIGHT *) @@ -476,7 +477,7 @@ \end{verbatim} Here the visual appearance is that of three arguments @{ML_text x}, - @{ML_text y}, @{ML_text z}. + @{ML_text y}, @{ML_text z} in a row. \end{enumerate} @@ -504,15 +505,24 @@ let val y = ... in ... end + + + (* WRONG *) + + fun foo x = + let + val y = ... + in + ... end \end{verbatim} \medskip In general the source layout is meant to emphasize the structure of complex language expressions, not to pretend that SML - had a completely different syntax (say that of Haskell or Java). + had a completely different syntax (say that of Haskell, Scala, Java). *} -section {* SML embedded into Isabelle/Isar *} +section {* ML embedded into Isabelle/Isar *} text {* ML and Isar are intertwined via an open-ended bootstrap process that provides more and more programming facilities and @@ -520,36 +530,35 @@ the raw environment of existing implementations of Standard ML (mainly Poly/ML, but also SML/NJ). - Isabelle/Pure marks the point where the original ML toplevel is - superseded by the Isar toplevel that maintains a uniform context for - arbitrary ML values (see also \secref{sec:context}). This formal - environment holds ML compiler bindings, logical entities, and many - other things. Raw SML is never encountered again after the initial - bootstrap of Isabelle/Pure. - - Object-logics like Isabelle/HOL are built within the - Isabelle/ML/Isar environment by introducing suitable theories with - associated ML modules, either inlined or as separate files. Thus - Isabelle/HOL is defined as a regular user-space application within - the Isabelle framework. Further add-on tools can be implemented in - ML within the Isar context in the same manner: ML is part of the - standard repertoire of Isabelle, and there is no distinction between - ``user'' and ``developer'' in this respect. + Isabelle/Pure marks the point where the raw ML toplevel is superseded by + Isabelle/ML within the Isar theory and proof language, with a uniform + context for arbitrary ML values (see also \secref{sec:context}). This formal + environment holds ML compiler bindings, logical entities, and many other + things. + + Object-logics like Isabelle/HOL are built within the Isabelle/ML/Isar + environment by introducing suitable theories with associated ML modules, + either inlined within @{verbatim ".thy"} files, or as separate @{verbatim + ".ML"} files that are loading from some theory. Thus Isabelle/HOL is defined + as a regular user-space application within the Isabelle framework. Further + add-on tools can be implemented in ML within the Isar context in the same + manner: ML is part of the standard repertoire of Isabelle, and there is no + distinction between ``users'' and ``developers'' in this respect. *} subsection {* Isar ML commands *} -text {* The primary Isar source language provides facilities to ``open - a window'' to the underlying ML compiler. Especially see the Isar - commands @{command_ref "ML_file"} and @{command_ref "ML"}: both work the - same way, only the source text is provided via a file vs.\ inlined, - respectively. Apart from embedding ML into the main theory - definition like that, there are many more commands that refer to ML - source, such as @{command_ref setup} or @{command_ref declaration}. - Even more fine-grained embedding of ML into Isar is encountered in - the proof method @{method_ref tactic}, which refines the pending - goal state via a given expression of type @{ML_type tactic}. +text {* + The primary Isar source language provides facilities to ``open a window'' to + the underlying ML compiler. Especially see the Isar commands @{command_ref + "ML_file"} and @{command_ref "ML"}: both work the same way, but the source + text is provided differently, via a file vs.\ inlined, respectively. Apart + from embedding ML into the main theory definition like that, there are many + more commands that refer to ML source, such as @{command_ref setup} or + @{command_ref declaration}. Even more fine-grained embedding of ML into Isar + is encountered in the proof method @{method_ref tactic}, which refines the + pending goal state via a given expression of type @{ML_type tactic}. *} text %mlex {* The following artificial example demonstrates some ML @@ -568,18 +577,18 @@ paragraph, nor in a different theory that is independent from the current one in the import hierarchy. - Removing the above ML declaration from the source text will remove - any trace of this definition as expected. The Isabelle/ML toplevel - environment is managed in a \emph{stateless} way: unlike the raw ML - toplevel there are no global side-effects involved - here.\footnote{Such a stateless compilation environment is also a - prerequisite for robust parallel compilation within independent - nodes of the implicit theory development graph.} + Removing the above ML declaration from the source text will remove any trace + of this definition, as expected. The Isabelle/ML toplevel environment is + managed in a \emph{stateless} way: in contrast to the raw ML toplevel, there + are no global side-effects involved here.\footnote{Such a stateless + compilation environment is also a prerequisite for robust parallel + compilation within independent nodes of the implicit theory development + graph.} \medskip The next example shows how to embed ML into Isar proofs, using - @{command_ref "ML_prf"} instead of Instead of @{command_ref "ML"}. + @{command_ref "ML_prf"} instead of Instead of @{command_ref "ML"}. As illustrated below, the effect on the ML environment is local to - the whole proof body, ignoring the block structure. + the whole proof body, but ignoring the block structure. *} notepad @@ -597,13 +606,13 @@ context. \medskip Two further ML commands are useful in certain situations: - @{command_ref ML_val} and @{command_ref ML_command} are - \emph{diagnostic} in the sense that there is no effect on the - underlying environment, and can thus used anywhere (even outside a - theory). The examples below produce long strings of digits by - invoking @{ML factorial}: @{command ML_val} already takes care of - printing the ML toplevel result, but @{command ML_command} is silent - so we produce an explicit output message. *} + @{command_ref ML_val} and @{command_ref ML_command} are \emph{diagnostic} in + the sense that there is no effect on the underlying environment, and can + thus be used anywhere. The examples below produce long strings of digits by + invoking @{ML factorial}: @{command ML_val} takes care of printing the ML + toplevel result, but @{command ML_command} is silent so we produce an + explicit output message. +*} ML_val {* factorial 100 *} ML_command {* writeln (string_of_int (factorial 100)) *} @@ -646,11 +655,10 @@ \item @{ML ML_Thms.bind_thms}~@{text "(name, thms)"} stores a list of theorems produced in ML both in the (global) theory context and the - ML toplevel, associating it with the provided name. Theorems are - put into a global ``standard'' format before being stored. - - \item @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but refers to a - singleton fact. + ML toplevel, associating it with the provided name. + + \item @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but + refers to a singleton fact. \end{description} @@ -664,7 +672,7 @@ subsection {* Antiquotations \label{sec:ML-antiq} *} -text {* A very important consequence of embedding SML into Isar is the +text {* A very important consequence of embedding ML into Isar is the concept of \emph{ML antiquotation}. The standard token language of ML is augmented by special syntactic entities of the following form: @@ -672,14 +680,13 @@ @{syntax_def antiquote}: '@{' nameref args '}' \} - Here @{syntax nameref} and @{syntax args} are regular outer syntax - categories \cite{isabelle-isar-ref}. Attributes and proof methods - use similar syntax. + Here @{syntax nameref} and @{syntax args} are outer syntax categories, as + defined in \cite{isabelle-isar-ref}. \medskip A regular antiquotation @{text "@{name args}"} processes its arguments by the usual means of the Isar source language, and produces corresponding ML source text, either as literal - \emph{inline} text (e.g. @{text "@{term t}"}) or abstract + \emph{inline} text (e.g.\ @{text "@{term t}"}) or abstract \emph{value} (e.g. @{text "@{thm th}"}). This pre-compilation scheme allows to refer to formal entities in a robust manner, with proper static scoping and with some degree of logical checking of @@ -690,8 +697,8 @@ subsection {* Printing ML values *} text {* The ML compiler knows about the structure of values according - to their static type, and can print them in the manner of the - toplevel loop, although the details are non-portable. The + to their static type, and can print them in the manner of its + toplevel, although the details are non-portable. The antiquotations @{ML_antiquotation_def "make_string"} and @{ML_antiquotation_def "print"} provide a quasi-portable way to refer to this potential capability of the underlying ML system in @@ -699,7 +706,7 @@ This is occasionally useful for diagnostic or demonstration purposes. Note that production-quality tools require proper - user-level error messages. *} + user-level error messages, avoiding raw ML values in the output. *} text %mlantiq {* \begin{matharray}{rcl} @@ -756,9 +763,8 @@ @{text "\\<^sub>1 \ \ \ \\<^sub>n \ \"}. This is isomorphic to the well-known encoding via tuples @{text "\\<^sub>1 \ \ \ \\<^sub>n \ \"}, but the curried version fits more smoothly into the basic calculus.\footnote{The - difference is even more significant in higher-order logic, because - the redundant tuple structure needs to be accommodated by formal - reasoning.} + difference is even more significant in HOL, because the redundant + tuple structure needs to be accommodated extraneous proof steps.} Currying gives some flexibility due to \emph{partial application}. A function @{text "f: \\<^sub>1 \ \\<^sub>2 \ \"} can be applied to @{text "x: \\<^sub>1"} @@ -773,10 +779,10 @@ observes certain standard patterns and minimizes adhoc permutations in their application. In Isabelle/ML, large portions of text can be written without auxiliary operations like @{text "swap: \ \ \ \ \ \ - \"} or @{text "C: (\ \ \ \ \) \ (\ \ \ \ \)"} (the latter not + \"} or @{text "C: (\ \ \ \ \) \ (\ \ \ \ \)"} (the latter is not present in the Isabelle/ML library). - \medskip The basic idea is that arguments that vary less are moved + \medskip The main idea is that arguments that vary less are moved further to the left than those that vary more. Two particularly important categories of functions are \emph{selectors} and \emph{updates}. @@ -862,7 +868,7 @@ text {* As explained above, a function @{text "f: \ \ \ \ \"} can be understood as update on a configuration of type @{text "\"}, - parametrized by arguments of type @{text "\"}. Given @{text "a: \"} + parameterized by an argument of type @{text "\"}. Given @{text "a: \"} the partial application @{text "(f a): \ \ \"} operates homogeneously on @{text "\"}. This can be iterated naturally over a list of parameters @{text "[a\<^sub>1, \, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \ #> f a\<^sub>n"}. @@ -899,7 +905,7 @@ @{text "f"} to a list of parameters. \item @{ML fold_rev}~@{text "f"} is similar to @{ML fold}~@{text - "f"}, but works inside-out. + "f"}, but works inside-out, as if the list would be reversed. \item @{ML fold_map}~@{text "f"} lifts the parametrized update function @{text "f"} (with side-result) to a list of parameters and @@ -908,14 +914,13 @@ \end{description} \begin{warn} - The literature on functional programming provides a multitude of - combinators called @{text "foldl"}, @{text "foldr"} etc. SML97 - provides its own variations as @{ML List.foldl} and @{ML - List.foldr}, while the classic Isabelle library also has the - historic @{ML Library.foldl} and @{ML Library.foldr}. To avoid - unnecessary complication and confusion, all these historical - versions should be ignored, and @{ML fold} (or @{ML fold_rev}) used - exclusively. + The literature on functional programming provides a confusing multitude of + combinators called @{text "foldl"}, @{text "foldr"} etc. SML97 provides its + own variations as @{ML List.foldl} and @{ML List.foldr}, while the classic + Isabelle library also has the historic @{ML Library.foldl} and @{ML + Library.foldr}. To avoid unnecessary complication, all these historical + versions should be ignored, and the canonical @{ML fold} (or @{ML fold_rev}) + used exclusively. \end{warn} *} @@ -964,9 +969,9 @@ Buffer.empty |> add_content tree |> Buffer.content; *} -text {* The slow part of @{ML slow_content} is the @{ML implode} of +text {* The slowness of @{ML slow_content} is due to the @{ML implode} of the recursive results, because it copies previously produced strings - again. + again and again. The incremental @{ML add_content} avoids this by operating on a buffer that is passed through in a linear fashion. Using @{ML_text @@ -974,7 +979,7 @@ additional boiler-plate. Of course, the two @{ML "Buffer.add"} invocations with concatenated strings could have been split into smaller parts, but this would have obfuscated the source without - making a big difference in allocations. Here we have done some + making a big difference in performance. Here we have done some peephole-optimization for the sake of readability. Another benefit of @{ML add_content} is its ``open'' form as a @@ -987,7 +992,7 @@ Note that @{ML fast_content} above is only defined as example. In many practical situations, it is customary to provide the incremental @{ML add_content} only and leave the initialization and - termination to the concrete application by the user. + termination to the concrete application to the user. *} @@ -999,9 +1004,10 @@ Depending on the user interface involved, these messages may appear in different text styles or colours. The standard output for - terminal sessions prefixes each line of warnings by @{verbatim + batch sessions prefixes each line of warnings by @{verbatim "###"} and errors by @{verbatim "***"}, but leaves anything else - unchanged. + unchanged. The message body may contain further markup and formatting, + which is routinely used in the Prover IDE \cite{isabelle-jedit}. Messages are associated with the transaction context of the running Isar command. This enables the front-end to manage commands and @@ -1015,7 +1021,7 @@ @{index_ML writeln: "string -> unit"} \\ @{index_ML tracing: "string -> unit"} \\ @{index_ML warning: "string -> unit"} \\ - @{index_ML error: "string -> 'a"} \\ + @{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\ \end{mldecls} \begin{description} @@ -1072,7 +1078,7 @@ \begin{warn} The message channels should be used in a message-oriented manner. This means that multi-line output that logically belongs together is - issued by a \emph{single} invocation of @{ML writeln} etc.\ with the + issued by a single invocation of @{ML writeln} etc.\ with the functional concatenation of all message constituents. \end{warn} *} @@ -1102,23 +1108,23 @@ \paragraph{Regular user errors.} These are meant to provide informative feedback about malformed input etc. - The \emph{error} function raises the corresponding \emph{ERROR} - exception, with a plain text message as argument. \emph{ERROR} + The \emph{error} function raises the corresponding @{ML ERROR} + exception, with a plain text message as argument. @{ML ERROR} exceptions can be handled internally, in order to be ignored, turned into other exceptions, or cascaded by appending messages. If the - corresponding Isabelle/Isar command terminates with an \emph{ERROR} - exception state, the toplevel will print the result on the error + corresponding Isabelle/Isar command terminates with an @{ML ERROR} + exception state, the system will print the result on the error channel (see \secref{sec:message-channels}). It is considered bad style to refer to internal function names or - values in ML source notation in user error messages. + values in ML source notation in user error messages. Do not use + @{text "@{make_string}"} here! Grammatical correctness of error messages can be improved by \emph{omitting} final punctuation: messages are often concatenated or put into a larger context (e.g.\ augmented with source position). - By not insisting in the final word at the origin of the error, the - system can perform its administrative tasks more easily and - robustly. + Note that punctuation after formal entities (types, terms, theorems) is + particularly prone to user confusion. \paragraph{Program failures.} There is a handful of standard exceptions that indicate general failure situations, or failures of @@ -1129,7 +1135,7 @@ main purpose is to determine quickly what has happened where. Traditionally, the (short) exception message would include the name of an ML function, although this is no longer necessary, because the - ML runtime system prints a detailed source position of the + ML runtime system attaches detailed source position stemming from the corresponding @{ML_text raise} keyword. \medskip User modules can always introduce their own custom @@ -1142,17 +1148,16 @@ \paragraph{Interrupts.} These indicate arbitrary system events: both the ML runtime system and the Isabelle/ML infrastructure signal various exceptional situations by raising the special - \emph{Interrupt} exception in user code. - - This is the one and only way that physical events can intrude an - Isabelle/ML program. Such an interrupt can mean out-of-memory, - stack overflow, timeout, internal signaling of threads, or the user - producing a console interrupt manually etc. An Isabelle/ML program - that intercepts interrupts becomes dependent on physical effects of - the environment. Even worse, exception handling patterns that are - too general by accident, e.g.\ by misspelled exception constructors, - will cover interrupts unintentionally and thus render the program - semantics ill-defined. + @{ML Exn.Interrupt} exception in user code. + + This is the one and only way that physical events can intrude an Isabelle/ML + program. Such an interrupt can mean out-of-memory, stack overflow, timeout, + internal signaling of threads, or a POSIX process signal. An Isabelle/ML + program that intercepts interrupts becomes dependent on physical effects of + the environment. Even worse, exception handling patterns that are too + general by accident, e.g.\ by misspelled exception constructors, will cover + interrupts unintentionally and thus render the program semantics + ill-defined. Note that the Interrupt exception dates back to the original SML90 language definition. It was excluded from the SML97 version to @@ -1189,7 +1194,7 @@ \emph{not} handled here, i.e.\ this form serves as safe replacement for the \emph{unsafe} version @{ML_text "(SOME"}~@{text "f x"}~@{ML_text "handle _ => NONE)"} that is occasionally seen in - books about SML97, not Isabelle/ML. + books about SML97, but not in Isabelle/ML. \item @{ML can} is similar to @{ML try} with more abstract result. @@ -1238,7 +1243,7 @@ text {* A \emph{symbol} constitutes the smallest textual unit in Isabelle/ML --- raw ML characters are normally not encountered at - all! Isabelle strings consist of a sequence of symbols, represented + all. Isabelle strings consist of a sequence of symbols, represented as a packed string or an exploded list of strings. Each symbol is in itself a small string, which has either one of the following forms: @@ -1275,25 +1280,19 @@ classified as a letter, which means it may occur within regular Isabelle identifiers. - The character set underlying Isabelle symbols is 7-bit ASCII, but - 8-bit character sequences are passed-through unchanged. Unicode/UCS - data in UTF-8 encoding is processed in a non-strict fashion, such - that well-formed code sequences are recognized - accordingly.\footnote{Note that ISO-Latin-1 differs from UTF-8 only - in some special punctuation characters that even have replacements - within the standard collection of Isabelle symbols. Text consisting - of ASCII plus accented letters can be processed in either encoding.} - Unicode provides its own collection of mathematical symbols, but - within the core Isabelle/ML world there is no link to the standard - collection of Isabelle regular symbols. - - \medskip Output of Isabelle symbols depends on the print mode - \cite{isabelle-isar-ref}. For example, the standard {\LaTeX} - setup of the Isabelle document preparation system would present - ``\verb,\,\verb,,'' as @{text "\"}, and - ``\verb,\,\verb,<^bold>,\verb,\,\verb,,'' as @{text "\<^bold>\"}. - On-screen rendering usually works by mapping a finite subset of - Isabelle symbols to suitable Unicode characters. + The character set underlying Isabelle symbols is 7-bit ASCII, but 8-bit + character sequences are passed-through unchanged. Unicode/UCS data in UTF-8 + encoding is processed in a non-strict fashion, such that well-formed code + sequences are recognized accordingly. Unicode provides its own collection of + mathematical symbols, but within the core Isabelle/ML world there is no link + to the standard collection of Isabelle regular symbols. + + \medskip Output of Isabelle symbols depends on the print mode. For example, + the standard {\LaTeX} setup of the Isabelle document preparation system + would present ``\verb,\,\verb,,'' as @{text "\"}, and + ``\verb,\,\verb,<^bold>,\verb,\,\verb,,'' as @{text "\<^bold>\"}. On-screen + rendering usually works by mapping a finite subset of Isabelle symbols to + suitable Unicode characters. *} text %mlref {* @@ -1329,8 +1328,9 @@ \item Type @{ML_type "Symbol.sym"} is a concrete datatype that represents the different kinds of symbols explicitly, with - constructors @{ML "Symbol.Char"}, @{ML "Symbol.Sym"}, @{ML - "Symbol.UTF8"}, @{ML "Symbol.Ctrl"}, @{ML "Symbol.Raw"}. + constructors @{ML "Symbol.Char"}, @{ML "Symbol.UTF8"}, + @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, @{ML "Symbol.Raw"}, + @{ML "Symbol.Malformed"}. \item @{ML "Symbol.decode"} converts the string representation of a symbol into the datatype version. @@ -1430,7 +1430,7 @@ text {* Note that in Unicode renderings of the symbol @{text "\"}, variations of encodings like UTF-8 or UTF-16 pose delicate questions - about the multi-byte representations its codepoint, which is outside + about the multi-byte representations of its codepoint, which is outside of the 16-bit address space of the original Unicode standard from the 1990-ies. In Isabelle/ML it is just ``\verb,\,\verb,,'' literally, using plain ASCII characters beyond any doubts. *} @@ -1445,12 +1445,11 @@ \begin{description} - \item Type @{ML_type int} represents regular mathematical integers, - which are \emph{unbounded}. Overflow never happens in - practice.\footnote{The size limit for integer bit patterns in memory - is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.} - This works uniformly for all supported ML platforms (Poly/ML and - SML/NJ). + \item Type @{ML_type int} represents regular mathematical integers, which + are \emph{unbounded}. Overflow is treated properly, but should never happen + in practice.\footnote{The size limit for integer bit patterns in memory is + 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.} This works + uniformly for all supported ML platforms (Poly/ML and SML/NJ). Literal integers in ML text are forced to be of this one true integer type --- adhoc overloading of SML97 is disabled. @@ -1481,7 +1480,7 @@ \item @{ML seconds}~@{text "s"} turns the concrete scalar @{text "s"} (measured in seconds) into an abstract time value. Floating point numbers are easy to use as configuration options in the - context (see \secref{sec:config-options}) or system preferences that + context (see \secref{sec:config-options}) or system options that are maintained externally. \end{description} @@ -1503,7 +1502,7 @@ *} text {* Apart from @{ML Option.map} most other operations defined in - structure @{ML_structure Option} are alien to Isabelle/ML an never + structure @{ML_structure Option} are alien to Isabelle/ML and never used. The operations shown above are defined in @{file "~~/src/Pure/General/basics.ML"}. *} @@ -1607,22 +1606,21 @@ Isabelle/ML, following standard conventions for their names and types. - Note that a function called @{text lookup} is obliged to express its + Note that a function called @{verbatim lookup} is obliged to express its partiality via an explicit option element. There is no choice to raise an exception, without changing the name to something like @{text "the_element"} or @{text "get"}. The @{text "defined"} operation is essentially a contraction of @{ML - is_some} and @{text "lookup"}, but this is sufficiently frequent to + is_some} and @{verbatim "lookup"}, but this is sufficiently frequent to justify its independent existence. This also gives the implementation some opportunity for peep-hole optimization. \end{description} - Association lists are adequate as simple and light-weight - implementation of finite mappings in many practical situations. A - more heavy-duty table structure is defined in @{file - "~~/src/Pure/General/table.ML"}; that version scales easily to + Association lists are adequate as simple implementation of finite mappings + in many practical situations. A more advanced table structure is defined in + @{file "~~/src/Pure/General/table.ML"}; that version scales easily to thousands or millions of elements. *} @@ -1689,13 +1687,13 @@ avoid a perceived loss of performance. See also \cite{Sutter:2005}.} - Isabelle/Isar exploits the inherent structure of theories and proofs - to support \emph{implicit parallelism} to a large extent. LCF-style - theorem provides almost ideal conditions for that, see also - \cite{Wenzel:2009}. This means, significant parts of theory and - proof checking is parallelized by default. In Isabelle2013, a - maximum speedup-factor of 3.5 on 4 cores and 6.5 on 8 cores can be - expected. + Isabelle/Isar exploits the inherent structure of theories and proofs to + support \emph{implicit parallelism} to a large extent. LCF-style theorem + proving provides almost ideal conditions for that, see also + \cite{Wenzel:2009}. This means, significant parts of theory and proof + checking is parallelized by default. In Isabelle2013, a maximum + speedup-factor of 3.5 on 4 cores and 6.5 on 8 cores can be expected + \cite{Wenzel:2013:ITP}. \medskip ML threads lack the memory protection of separate processes, and operate concurrently on shared heap memory. This has @@ -1717,15 +1715,14 @@ performance of the whole system. \end{warn} - Apart from observing the principles of thread-safeness passively, - advanced tools may also exploit parallelism actively, e.g.\ by using - ``future values'' (\secref{sec:futures}) or the more basic library + Apart from observing the principles of thread-safeness passively, advanced + tools may also exploit parallelism actively, e.g.\ by using library functions for parallel list operations (\secref{sec:parlist}). \begin{warn} Parallel computing resources are managed centrally by the Isabelle/ML infrastructure. User programs must not fork their own - ML threads to perform computations. + ML threads to perform heavy computations. \end{warn} *} @@ -1772,7 +1769,8 @@ new state record can be created on each invocation, and passed through any auxiliary functions of the component. The state record may well contain mutable references, without requiring any special - synchronizations, as long as each invocation gets its own copy. + synchronizations, as long as each invocation gets its own copy, and the + tool itself is single-threaded. \item Avoid raw output on @{text "stdout"} or @{text "stderr"}. The Poly/ML library is thread-safe for each individual output operation, @@ -1781,7 +1779,7 @@ interleaving of atomic chunks. Note that this does not affect regular message output channels - (\secref{sec:message-channels}). An official message is associated + (\secref{sec:message-channels}). An official message id is associated with the command transaction from where it originates, independently of other transactions. This means each running Isar command has effectively its own set of message channels, and interleaving can @@ -1789,7 +1787,7 @@ message boundaries). \item Treat environment variables and the current working directory - of the running process as strictly read-only. + of the running process as read-only. \item Restrict writing to the file-system to unique temporary files. Isabelle already provides a temporary directory that is unique for @@ -2021,13 +2019,13 @@ all results are regular values, that list is returned. Otherwise, the collection of all exceptions is raised, wrapped-up as collective parallel exception. Note that the latter prevents access to - individual exceptions by conventional @{verbatim "handle"} of SML. + individual exceptions by conventional @{verbatim "handle"} of ML. \item @{ML Par_Exn.release_first} is similar to @{ML Par_Exn.release_all}, but only the first exception that has occurred in the original evaluation process is raised again, the others are ignored. That single exception may get handled by conventional - means in SML. + means in ML. \end{description} *} @@ -2310,7 +2308,7 @@ @{text a} without any further evaluation. There is very low overhead for this proforma wrapping of strict values as - future values. + futures. \item @{ML Future.map}~@{text "f x"} is a fast-path implementation of @{ML Future.fork}~@{text "(fn () => f ("}@{ML Future.join}~@{text "x))"}, which diff -r 2b8b1a8587da -r 2f4948579905 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Sat Jun 28 11:44:22 2014 +0200 +++ b/src/Doc/Implementation/Prelim.thy Sat Jun 28 15:35:30 2014 +0200 @@ -310,7 +310,7 @@ of the three kinds of contexts: theory, proof, generic. \paragraph{Theory data} declarations need to implement the following - SML signature: + ML signature: \medskip \begin{tabular}{ll} @@ -336,7 +336,7 @@ chain of diamonds would cause an exponential blowup! \paragraph{Proof context data} declarations need to implement the - following SML signature: + following ML signature: \medskip \begin{tabular}{ll} diff -r 2b8b1a8587da -r 2f4948579905 src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Sat Jun 28 11:44:22 2014 +0200 +++ b/src/Doc/Implementation/Tactic.thy Sat Jun 28 15:35:30 2014 +0200 @@ -97,7 +97,7 @@ successor states. The underlying sequence implementation is lazy both in head and tail, and is purely functional in \emph{not} supporting memoing.\footnote{The lack of memoing and the strict - nature of SML requires some care when working with low-level + nature of ML requires some care when working with low-level sequence operations, to avoid duplicate or premature evaluation of results. It also means that modified runtime behavior, such as timeout, is very hard to achieve for general tactics.} diff -r 2b8b1a8587da -r 2f4948579905 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sat Jun 28 11:44:22 2014 +0200 +++ b/src/Doc/JEdit/JEdit.thy Sat Jun 28 15:35:30 2014 +0200 @@ -8,14 +8,14 @@ section {* Concepts and terminology *} -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. +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,Wenzel:2014:ITP-PIDE}, + 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. \begin{description} @@ -74,7 +74,7 @@ Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for the jEdit text editor, while preserving its general look-and-feel as far as possible. The main plugin is called ``Isabelle'' and has its own menu - \emph{Plugins~/ Isabelle} with several panels (see also + \emph{Plugins~/ Isabelle} with access to several panels (see also \secref{sec:dockables}), as well as \emph{Plugins~/ Plugin Options~/ Isabelle} (see also \secref{sec:options}). @@ -84,7 +84,7 @@ automatically by the Isabelle build tool \cite{isabelle-sys}: if it is absent or outdated wrt.\ its sources, the build process updates it before entering the Prover IDE. Changing the logic session within Isabelle/jEdit - requires a restart of the application. + requires a restart of the whole application. \medskip The main job of the Prover IDE is to manage sources and their changes, taking the logical structure as a formal document into account (see @@ -92,18 +92,17 @@ asynchronously in a lock-free manner. The prover is free to organize the checking of the formal text in parallel on multiple cores, and provides feedback via markup, which is rendered in the editor via colors, boxes, - squiggly underline, hyperlinks, popup windows, icons, clickable output etc. + squiggly underlines, hyperlinks, popup windows, icons, clickable output etc. 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 (see also \secref{sec:tooltips-hyperlinks}). - Formal output (in popups etc.) may be explored recursively, using the same + Output (in popups etc.) may be explored recursively, using the same techniques as in the editor source buffer. Thus the Prover IDE gives an impression of direct access to formal content of the prover within the editor, but in reality only certain aspects are - exposed, according to the possibilities of the prover and its many add-on - tools. + exposed, according to the possibilities of the prover and its many tools. *} @@ -129,18 +128,18 @@ 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. +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. + 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 @@ -152,7 +151,8 @@ formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \emph{ErrorList}, \emph{Code2HTML}) are included to saturate the dependencies of bundled plugins, but have no particular use in - Isabelle/jEdit. *} + Isabelle/jEdit. +*} subsection {* Options \label{sec:options} *} @@ -204,11 +204,12 @@ properties, and additional keyboard shortcuts for Isabelle-specific functionality. Users may change their keymap later, but need to copy some keyboard shortcuts manually (see also @{file_unchecked - "$ISABELLE_HOME_USER/jedit/keymaps"}). + "$ISABELLE_HOME_USER/jedit/keymaps"} versus @{verbatim shortcut} properties + in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}). *} -section {* Command-line invocation *} +section {* Command-line invocation \label{sec:command-line} *} text {* Isabelle/jEdit is normally invoked as standalone application, with @@ -244,22 +245,22 @@ of @{tool build}. The @{verbatim "-n"} option bypasses the implicit build process for the selected session image. - The @{verbatim "-m"} option specifies additional print modes for the - prover process. Note that the system option @{system_option_ref - jedit_print_mode} allows to do the same persistently (e.g.\ via the - Plugin Options dialog of Isabelle/jEdit), without requiring - command-line invocation. + The @{verbatim "-m"} option specifies additional print modes for the prover + process. Note that the system option @{system_option_ref jedit_print_mode} + allows to do the same persistently (e.g.\ via the \emph{Plugin Options} + dialog of Isabelle/jEdit), without requiring command-line invocation. - The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass - additional low-level options to the JVM or jEdit, respectively. The - defaults are provided by the Isabelle settings environment - \cite{isabelle-sys}. + The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass additional + low-level options to the JVM or jEdit, respectively. The defaults are + provided by the Isabelle settings environment \cite{isabelle-sys}, but note + that these only work for the command-line tool described here, and not the + regular application. The @{verbatim "-b"} and @{verbatim "-f"} options control the self-build mechanism of Isabelle/jEdit. This is only relevant for building from sources, which also requires an auxiliary @{verbatim jedit_build} component - from @{url "http://isabelle.in.tum.de/components"}. Note that official - Isabelle releases already include a pre-built version of Isabelle/jEdit. + from @{url "http://isabelle.in.tum.de/components"}. The official + Isabelle release already includes a pre-built version of Isabelle/jEdit. *} @@ -273,11 +274,11 @@ distributors allow (see also \secref{sec:problems}). Isabelle/jEdit enables platform-specific look-and-feel by default as - follows: + follows. \begin{description} - \item[Linux] The platform-independent \emph{Nimbus} is used by + \item[Linux:] The platform-independent \emph{Nimbus} is used by default. \emph{GTK+} works under the side-condition that the overall GTK theme is @@ -286,16 +287,16 @@ is lagging behind further development of Swing and GTK. The graphics rendering performance can be worse than for other Swing look-and-feels.} - \item[Windows] Regular \emph{Windows} is used by default, but + \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. + \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, + 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. It is advisable to have the - \emph{MacOSX} enabled all the time on that platform. + \emph{MacOSX} plugin enabled all the time on that platform. \end{description} @@ -328,8 +329,8 @@ \emph{HyperSearch Results} or the \emph{File System Browser}. Plugins often provide a central dockable to access their key functionality, which may be opened by the user on demand. The Isabelle/jEdit plugin takes this approach - to the extreme: its main plugin menu merely provides entry-points to panels - that are managed as dockable windows. Some important panels are docked by + to the extreme: its plugin menu merely provides entry-points to panels that + are managed as dockable windows. Some important panels are docked by default, e.g.\ \emph{Documentation}, \emph{Output}, \emph{Query}, but the user can change this arrangement easily. @@ -365,23 +366,21 @@ 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.} +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.\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.} See also \cite{Wenzel:2011:CICM}. - 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 + 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"}. @@ -390,22 +389,20 @@ 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 + 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{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 (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 @@ -414,16 +411,15 @@ 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 prevent Isabelle/jEdit to use - 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 is occasionally tempting to use - the same font in other applications). + Note that a Java/AWT/Swing application can load additional fonts only if + they are not installed on the operating system already! Some outdated + version of @{verbatim IsabelleText} that happens to be provided by the + operating system would prevent Isabelle/jEdit to use 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 is 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 @@ -434,8 +430,8 @@ 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: + This is a summary for practically relevant input methods for Isabelle + symbols. \begin{enumerate} @@ -487,12 +483,11 @@ \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. + Note that the above abbreviations refer to the input method. The logical + notation provides ASCII alternatives that often coincide, but sometimes + deviate. 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 @@ -562,13 +557,13 @@ @{verbatim "*shell*"}. 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 Scala expression @{verbatim "PIDE.snapshot(view)"} makes a PIDE - document snapshot of the current buffer within the current editor view. + is the regular Scala toplevel loop running inside the 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 + Scala expression @{verbatim "PIDE.snapshot(view)"} makes a PIDE document + snapshot of the current buffer within the current editor view. This helps to explore Isabelle/Scala functionality interactively. Some care is required to avoid interference with the internals of the running @@ -578,21 +573,21 @@ 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 - physical files. +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 model of jEdit as far as possible. In particular, theory + sources are passed directly from the editor to the prover, without + indirection via physical 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 forward slashes of Unix/POSIX, too. - Further differences arise due to drive letters and network shares. + 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 forward slashes + like Unix/POSIX. Further differences arise due to Windows 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} @@ -603,14 +598,14 @@ 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). + \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 (\secref{sec:command-line}). Isabelle/jEdit imitates @{verbatim "$ISABELLE_HOME"} and @{verbatim "$ISABELLE_HOME_USER"} within the Java process environment, in order to @@ -624,7 +619,7 @@ file in the text editor, independently of the path notation. Formally checked paths in prover input are subject to completion - (\secref{sec:completion}): partial specifications are resolved via actual + (\secref{sec:completion}): partial specifications are resolved via directory content and possible completions are offered in a popup. *} @@ -710,8 +705,8 @@ resolve dependencies of theory imports. The system requests to load additional files into editor buffers, in order to be included in the document model for further checking. It is also possible to let the system - resolve dependencies automatically, according to \emph{Plugin Options~/ - Isabelle~/ General~/ Auto Load}. + resolve dependencies automatically, according to the system option + @{system_option jedit_auto_load}. \medskip The visible \emph{perspective} of Isabelle/jEdit is defined by the collective view on theory buffers via open text areas. The perspective is @@ -732,7 +727,7 @@ \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, + languages: colors, icons, highlighting, squiggly underlines, 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 @@ -759,10 +754,10 @@ \medskip As a concession to the massive amount of ML files in Isabelle/HOL itself, the content of auxiliary files is only added to the PIDE document-model on demand, the first time when opened explicitly in the - editor. There are further special tricks to manage markup of ML files, such - that Isabelle/HOL may be edited conveniently in the Prover IDE on small - machines with only 4--8\,GB of main memory. Using @{verbatim Pure} as logic - session image, the exploration may start at the top @{file + editor. There are further tricks to manage markup of ML files, such that + Isabelle/HOL may be edited conveniently in the Prover IDE on small machines + with only 4--8\,GB of main memory. Using @{verbatim Pure} as logic session + image, the exploration may start at the top @{file "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file "$ISABELLE_HOME/src/HOL/HOL.thy"}, for example. @@ -774,8 +769,8 @@ The change of responsibility from prover to editor counts as an update of the document content, so subsequent theory sources need to be re-checked. - When the buffer is closed, the responsibility remains to the editor, though: - the file may be opened again without causing another document update. + When the buffer is closed, the responsibility remains to the editor: the + file may be opened again without causing another document update. A file that is opened in the editor, but its theory with the load command is not, is presently inactive in the document model. A file that is loaded via @@ -798,15 +793,15 @@ section {* Output \label{sec: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. +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 underlines 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, without the text itself. \begin{figure}[htb] \begin{center} @@ -829,8 +824,8 @@ 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 according to \emph{Plugin Options~/ Isabelle~/ General~/ - Text Overview Limit} (in characters). + it is restricted according to the system option @{system_option + jedit_text_overview_limit} (in characters). Another course-grained overview is provided by the \emph{Theories} panel, but without direct correspondence to text positions. A @@ -853,8 +848,8 @@ 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, while using secondary output - windows only rarely. + possible to do meaningful proof editing within the primary text area and its + markup, while 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 @@ -874,7 +869,7 @@ text {* The \emph{Query} panel provides various GUI forms to request extra - information from the prover In old times the user would have issued some + information from the prover. In old times the user would have issued some diagnostic command like @{command find_theorems} and inspected its output, but this is now integrated into the Prover IDE. @@ -905,7 +900,9 @@ \item The \emph{Search} field allows to highlight query output according to some regular expression, in the notation that is commonly used on the Java - platform. This may serve as an additional visual filter of the result. + platform.\footnote{@{url + "http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html"}} + This may serve as an additional visual filter of the result. \item The \emph{Zoom} box controls the font size of the output area. @@ -961,7 +958,7 @@ the theory or proof context, or proof state. See also the Isar commands @{command_ref print_context}, @{command_ref print_cases}, @{command_ref print_term_bindings}, @{command_ref print_theorems}, - @{command_ref print_state} in \cite{isabelle-isar-ref}. + @{command_ref print_state} described in \cite{isabelle-isar-ref}. *} @@ -1103,7 +1100,7 @@ *} -subsubsection {* Symbols *} +subsubsection {* Isabelle symbols *} text {* The completion tables for Isabelle symbols (\secref{sec:symbols}) are @@ -1288,10 +1285,11 @@ text {* A \emph{completion popup} is a minimally invasive GUI component over the text area that offers a selection of completion items to be inserted into - the text, e.g.\ by mouse clicks. The popup 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 + the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to + the frequency of selection, with persistent history. The popup 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. Thus the popup serves as a mechanism of confirmation of proposed items, but the default is to continue without completion. @@ -1322,18 +1320,18 @@ Completion may first propose replacements to be selected (via a popup), or replace text immediately in certain situations and depending on certain options like @{system_option jedit_completion_immediate}. In any case, - insertion works uniformly, by imitating normal text insertion to some - extent. The precise behaviour depends on the state of the \emph{text - selection} of jEdit. Isabelle/jEdit tries to accommodate the most common - forms of advanced selections in jEdit, but not all combinations make sense. - At least the following important cases are well-defined. + insertion works uniformly, by imitating normal jEdit text insertion, + depending on the state of the \emph{text selection}. Isabelle/jEdit tries to + accommodate the most common forms of advanced selections in jEdit, but not + all combinations make sense. At least the following important cases are + well-defined: \begin{description} \item[No selection.] The original is removed and the replacement inserted, depending on the caret position. - \item[Rectangular selection zero width.] This special case is treated by + \item[Rectangular selection of zero width.] This special case is treated by jEdit as ``tall caret'' and insertion of completion imitates its normal behaviour: separate copies of the replacement are inserted for each line of the selection. @@ -1348,7 +1346,7 @@ \emph{HyperSearch}: clicking on one of the items in the \emph{HyperSearch Results} window makes jEdit select all its occurrences in the corresponding line of text. Then explicit completion can be invoked via @{verbatim "C+b"}, - for example to replace occurrences of @{verbatim "-->"} by @{text "\"}. + e.g.\ to replace occurrences of @{verbatim "-->"} by @{text "\"}. \medskip Insertion works by removing and inserting pieces of text from the buffer. This counts as one atomic operation on the jEdit history. Thus @@ -1453,7 +1451,7 @@ \item @{system_option_ref 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_ref "try0"}. + @{command_ref "try0"} \cite{isabelle-isar-ref}. The tool is disabled by default, since unparameterized invocation of standard proof methods often consumes substantial CPU resources @@ -1577,7 +1575,7 @@ modifier key as explained in \secref{sec:tooltips-hyperlinks}. Actual display of timing depends on the global option @{system_option_ref jedit_timing_threshold}, which can be configured in - "Plugin Options~/ Isabelle~/ General". + \emph{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 @@ -1622,8 +1620,8 @@ Under normal circumstances, prover output always works via managed message channels (corresponding to @{ML writeln}, @{ML warning}, @{ML - Output.error_message} etc.\ in Isabelle/ML), which are displayed by regular - means within the document model (\secref{sec:output}). + Output.error_message} in Isabelle/ML), which are displayed by regular means + within the document model (\secref{sec:output}). \item \emph{Syslog} shows system messages that might be relevant to diagnose problems with the startup or shutdown phase of the prover @@ -1683,16 +1681,16 @@ \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-2). + \textbf{Workaround:} Do not use X11 input methods. Note that environment + variable @{verbatim XMODIFIERS} is reset by default within Isabelle + settings. \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 a regular re-parenting window manager. + \textbf{Workaround:} Use a regular re-parenting X11 window manager. \item \textbf{Problem:} Recent forks of Linux/X11 window managers and desktop environments (variants of Gnome) disrupt the handling of diff -r 2b8b1a8587da -r 2f4948579905 src/Doc/manual.bib --- a/src/Doc/manual.bib Sat Jun 28 11:44:22 2014 +0200 +++ b/src/Doc/manual.bib Sat Jun 28 15:35:30 2014 +0200 @@ -1921,6 +1921,18 @@ volume = {7998}, } +@inproceedings{Wenzel:2014:ITP-PIDE, + author = {Makarius Wenzel}, + title = {Asynchronous User Interaction and Tool Integration in {Isabelle/PIDE}}, + booktitle = {Interactive Theorem Proving --- 5th International Conference, + ITP 2014, Vienna, Austria}, + editor = {Gerwin Klein and Ruben Gamboa}, + year = {2014}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {8558}, +} + @book{principia, author = {A. N. Whitehead and B. Russell}, title = {Principia Mathematica},