# 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.