# HG changeset patch # User wenzelm # Date 966271437 -7200 # Node ID 69d2fb3dc4c6fe636a8faffd17ca94f3263b8c6b # Parent a585662e6490cbac228865230fca1a6baca029dd updated command termination issue; diff -r a585662e6490 -r 69d2fb3dc4c6 doc-src/IsarRef/syntax.tex --- a/doc-src/IsarRef/syntax.tex Mon Aug 14 18:43:30 2000 +0200 +++ b/doc-src/IsarRef/syntax.tex Mon Aug 14 18:43:57 2000 +0200 @@ -25,11 +25,17 @@ \medskip -Another notable point is proper input termination. Proof~General demands any -command to be terminated by ``\texttt{;}'' -(semicolon)\index{semicolon}\index{*;}. As far as plain Isabelle/Isar is -concerned, commands may be directly run together, though. In the presentation -of Isabelle/Isar documents, semicolons are omitted in order to gain +Isabelle/Isar input may contain any number of input termination characters +``\texttt{;}'' (semicolon) to separate commands explicitly. This may be +particularly useful in interactive shell sessions to make clear where the +current command is intended to end. Otherwise, the interactive loop will +continue until end-of-command in clearly indicated from the input syntax, +e.g.\ encounter of the next command keyword. + +Advanced interfaces such as Proof~General \cite{proofgeneral} do not require +explicit semicolons, the amount of input text is determined automatically by +inspecting the Emacs text buffer. Also note that in the presentation of +Isabelle/Isar documents, semicolons are omitted in any case to gain readability. @@ -327,9 +333,9 @@ are to be presented in the final output produced by the Isabelle document preparation system (see also \S\ref{sec:document-prep}). -Thus embedding something like -\texttt{{\at}{\ttlbrace}term[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within -some text block would cause +Thus embedding of +\texttt{{\at}{\ttlbrace}term[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a +text block would cause \isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x} to appear in the final {\LaTeX} document.