updated command termination issue;
Mon, 14 Aug 2000 18:43:57 +0200
changeset 9601 69d2fb3dc4c6
parent 9600 a585662e6490
child 9602 900df8e67fcf
updated command termination issue;
--- 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 @@
-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
@@ -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
 to appear in the final {\LaTeX} document.