--- a/doc-src/IsarRef/pure.tex Wed Jun 16 20:36:43 2004 +0200
+++ b/doc-src/IsarRef/pure.tex Wed Jun 16 20:37:00 2004 +0200
@@ -1520,8 +1520,28 @@
\isarcmd{print_drafts}^* & : & \isarkeep{\cdot} \\
\end{matharray}
+\railalias{usethy}{use\_thy}
+\railterm{usethy}
+\railalias{usethyonly}{use\_thy\_only}
+\railterm{usethyonly}
+\railalias{updatethy}{update\_thy}
+\railterm{updatethy}
+\railalias{updatethyonly}{update\_thy\_only}
+\railterm{updatethyonly}
+\railalias{displaydrafts}{display\_drafts}
+\railterm{displaydrafts}
+\railalias{printdrafts}{print\_drafts}
+\railterm{printdrafts}
+
+\begin{rail}
+ ('cd' | usethy | usethyonly | updatethy | updatethyonly) name
+ ;
+ (displaydrafts | printdrafts) (name +)
+ ;
+\end{rail}
+
\begin{descr}
-\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
+\item [$\isarkeyword{cd}~path$] changes the current directory of the Isabelle
process.
\item [$\isarkeyword{pwd}~$] prints the current working directory.
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
@@ -1531,10 +1551,10 @@
implicit theory context to that of the theory loaded.} (see also
\cite[\S1,\S6]{isabelle-ref}). Note that both the ML and Isar versions may
load new- and old-style theories alike.
-\item [$\isarkeyword{display_drafts} and \isarkeyword{print_drafts}$] perform
- simple output of a given list of raw source files (specified as repeated
- $name$ arguments). Only those symbols that do not require additional LaTeX
- packages are displayed properly, everything else is left verbatim.
+\item [$\isarkeyword{display_drafts}~paths$ and
+ $\isarkeyword{print_drafts}~paths$] perform simple output of a given list of
+ raw source files. Only those symbols that do not require additional
+ {\LaTeX} packages are displayed properly, everything else is left verbatim.
\end{descr}
These system commands are scarcely used when working with the Proof~General
--- a/doc-src/IsarRef/syntax.tex Wed Jun 16 20:36:43 2004 +0200
+++ b/doc-src/IsarRef/syntax.tex Wed Jun 16 20:37:00 2004 +0200
@@ -63,17 +63,17 @@
\section{Lexical matters}\label{sec:lex-syntax}
-The Isabelle/Isar outer syntax provides token classes as presented below.
-Note that some of these coincide (by full intention) with the inner lexical
-syntax as presented in \cite{isabelle-ref}.
+The Isabelle/Isar outer syntax provides token classes as presented below; most
+of these coincide with the inner lexical syntax as presented in
+\cite{isabelle-ref}.
\indexoutertoken{ident}\indexoutertoken{longident}\indexoutertoken{symident}
\indexoutertoken{nat}\indexoutertoken{var}\indexoutertoken{typefree}
\indexoutertoken{typevar}\indexoutertoken{string}\indexoutertoken{verbatim}
\begin{matharray}{rcl}
- ident & = & letter~quasiletter^* \\
- longident & = & ident\verb,.,ident~\dots~ident \\
- symident & = & sym^+ ~|~ symbol \\
+ ident & = & letter\,quasiletter^* \\
+ longident & = & ident (\verb,.,ident)^+ \\
+ symident & = & sym^+ ~|~ \verb,\<,ident\verb,>, \\
nat & = & digit^+ \\
var & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
typefree & = & \verb,',ident \\
@@ -81,34 +81,42 @@
string & = & \verb,", ~\dots~ \verb,", \\
verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[1ex]
- letter & = & latin ~|~ symletter \\
+ letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek \\
+ quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', ~|~ \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
- quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', ~|~ \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~ %$
\verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\
& & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
\verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
- symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots\\
-symletter & = & \verb,\<, (latin ~|~ latin~latin ~|~ greek) \verb,>, \\
-greek & = & \verb,alpha, ~|~ \verb,beta, ~|~ \verb,gamma, ~|~ \verb,delta, ~|~ \verb,epsilon, ~|~ \verb,zeta, ~|~ \verb,eta, ~| \\
- & & \verb,theta, ~|~ \verb,iota, ~|~ \verb,kappa, ~|~ \verb,mu, ~|~ \verb,nu, ~|~ \verb,xi, ~|~ \verb,pi, ~|~ \verb,rho, ~| \\
- & & \verb,sigma, ~|~ \verb,tau, ~|~ \verb,upsilon, ~|~ \verb,phi, ~|~ \verb,psi, ~|~ \verb,omega, ~|~ \verb,Gamma, ~| \\
- & & \verb,Delta, ~|~ \verb,Theta, ~|~ \verb,Lambda, ~|~ \verb,Xi, ~|~ \verb,Pi, ~|~ \verb,Sigma, ~|~ \verb,Upsilon, ~| \\
- & & \verb,Phi, ~|~ \verb,Psi, ~|~ \verb,Omega,
+greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
+ & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
+ & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
+ & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~| \\
+ & & \verb,\<tau>, ~|~ \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<psi>, ~| \\
+ & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
+ & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
+ & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
\end{matharray}
The syntax of $string$ admits any characters, including newlines; ``\verb|"|''
(double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash.
-Note that ML-style control characters are \emph{not} supported. The body of
-$verbatim$ may consist of any text not containing ``\verb|*}|''; this allows
-convenient inclusion of quotes without further escapes.
+The body of $verbatim$ may consist of any text not containing ``\verb|*}|'';
+this allows convenient inclusion of quotes without further escapes. The greek
+letters do \emph{not} include \verb,\<lambda>,, which is already used
+differently in the meta-logic.
-Comments take the form \texttt{(*~\dots~*)} and may in principle be nested,
-just as in ML. Note that these are \emph{source} comments only, which are
-stripped after lexical analysis of the input. The Isar document syntax also
-provides \emph{formal comments} that are considered as part of the text (see
-\S\ref{sec:comments}).
+Common mathematical symbols such as $\forall$ are represented in Isabelle as
+\verb,\<forall>,. There are infinitely many legal symbols like this, although
+proper presentation is left to front-end tools such as {\LaTeX} or
+Proof~General with the X-Symbol package. A list of standard Isabelle symbols
+that work well with these tools is given in \cite[appendix~A]{isabelle-sys}.
+
+Comments take the form \texttt{(*~\dots~*)} and may be nested, although
+user-interface tools may prevent this. Note that \texttt{(*~\dots~*)}
+indicate source comments only, which are stripped after lexical analysis of
+the input. The Isar document syntax also provides formal comments that are
+considered as part of the text (see \S\ref{sec:comments}).
\begin{warn}
Proof~General does not handle nested comments properly; it is also unable to
@@ -118,20 +126,6 @@
these delimiters.
\end{warn}
-\medskip
-
-Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as
-``\verb,\<forall>,''. Concerning Isabelle itself, any sequence of the form
-\verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol.
-Greek letters \verb+\<alpha>+, \verb+\<beta>+, etc. (apart from
-\verb+\<lambda>+), as well as the \verb+\<^isub>+ and \verb+\<^isup>+ control
-characters may be used in identifiers as well.
-
-Display of appropriate glyphs is a matter of front-end tools, say the
-user-interface of Proof~General plus the X-Symbol package, or the {\LaTeX}
-macro setup of document output. A list of predefined Isabelle symbols is
-given in \cite[appendix~A]{isabelle-sys}.
-
\section{Common syntax entities}
--- a/doc-src/Ref/defining.tex Wed Jun 16 20:36:43 2004 +0200
+++ b/doc-src/Ref/defining.tex Wed Jun 16 20:37:00 2004 +0200
@@ -231,26 +231,28 @@
\ndxbold{xstr}, respectively. Typical examples are {\tt x}, {\tt ?x7}, {\tt
'a}, {\tt ?'a3}, {\tt \#42}, {\tt ''foo bar''}. Here is the precise syntax:
\begin{eqnarray*}
-id & = & letter~quasiletter^* \\
-longid & = & id\mbox{\tt .}id~\dots~id \\
+id & = & letter\,quasiletter^* \\
+longid & = & id (\mbox{\tt .}id)^+ \\
var & = & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
tid & = & \mbox{\tt '}id \\
tvar & = & \mbox{\tt ?}tid ~~|~~
\mbox{\tt ?}tid\mbox{\tt .}nat \\
num & = & nat ~~|~~ \mbox{\tt-}nat \\
xnum & = & \mbox{\tt \#}nat ~~|~~ \mbox{\tt \#-}nat \\
-xstr & = & \mbox{\tt ''\rm text\tt ''} \\[1ex]
-letter & = & latin ~|~ symletter \\
+xstr & = & \mbox{\tt ''~\dots~\tt ''} \\[1ex]
+letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek \\
+quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', ~|~ \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
nat & = & digit^+ \\
-quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', ~|~ \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
-symletter & = & \verb,\<, (latin ~|~ latin~latin ~|~ greek) \verb,>, \\
-greek & = & \verb,alpha, ~|~ \verb,beta, ~|~ \verb,gamma, ~|~ \verb,delta, ~|~ \verb,epsilon, ~|~ \verb,zeta, ~|~ \verb,eta, ~| \\
- & & \verb,theta, ~|~ \verb,iota, ~|~ \verb,kappa, ~|~ \verb,mu, ~|~ \verb,nu, ~|~ \verb,xi, ~|~ \verb,pi, ~|~ \verb,rho, ~| \\
- & & \verb,sigma, ~|~ \verb,tau, ~|~ \verb,upsilon, ~|~ \verb,phi, ~|~ \verb,psi, ~|~ \verb,omega, ~|~ \verb,Gamma, ~| \\
- & & \verb,Delta, ~|~ \verb,Theta, ~|~ \verb,Lambda, ~|~ \verb,Xi, ~|~ \verb,Pi, ~|~ \verb,Sigma, ~|~ \verb,Upsilon, ~| \\
- & & \verb,Phi, ~|~ \verb,Psi, ~|~ \verb,Omega,
+greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
+ & & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
+ & & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
+ & & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~| \\
+ & & \verb,\<tau>, ~|~ \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<psi>, ~| \\
+ & & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
+ & & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
+ & & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
\end{eqnarray*}
The lexer repeatedly takes the longest prefix of the input string that
forms a valid token. A maximal prefix that is both a delimiter and a
--- a/src/Pure/General/output.ML Wed Jun 16 20:36:43 2004 +0200
+++ b/src/Pure/General/output.ML Wed Jun 16 20:37:00 2004 +0200
@@ -66,9 +66,12 @@
fun has_mode s = s mem_string ! print_mode;
-val modes = ref (Symtab.empty:
- ((string -> string * real) * (string * int -> string) * (string -> string))
- Symtab.table);
+type mode_fns =
+ {output_width: string -> string * real,
+ indent: string * int -> string,
+ raw: string -> string};
+
+val modes = ref (Symtab.empty: mode_fns Symtab.table);
exception MISSING_DEFAULT_OUTPUT;
@@ -78,18 +81,18 @@
(case Library.get_first lookup_mode (! print_mode) of Some p => p
| None =>
(case lookup_mode "" of Some p => p
- | None => raise MISSING_DEFAULT_OUTPUT));
+ | None => raise MISSING_DEFAULT_OUTPUT)); (*sys_error would require output again!*)
-fun output_width x = #1 (get_mode ()) x;
+fun output_width x = #output_width (get_mode ()) x;
val output = #1 o output_width;
-fun indent x = #2 (get_mode ()) x;
-fun raw x = #3 (get_mode ()) x;
+fun indent x = #indent (get_mode ()) x;
+fun raw x = #raw (get_mode ()) x;
(** output channels **)
-(*process channels -- normally NOT used directly!*)
+(*primitive process channels -- normally NOT used directly!*)
fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
@@ -113,10 +116,10 @@
(* add_mode *)
-fun add_mode name m =
+fun add_mode name (f, g, h) =
(if is_none (lookup_mode name) then ()
else warning ("Redeclaration of symbol print mode: " ^ quote name);
- modes := Symtab.update ((name, m), ! modes));
+ modes := Symtab.update ((name, {output_width = f, indent = g, raw = h}), ! modes));
(* produce errors *)
--- a/src/Pure/General/scan.ML Wed Jun 16 20:36:43 2004 +0200
+++ b/src/Pure/General/scan.ML Wed Jun 16 20:37:00 2004 +0200
@@ -160,7 +160,7 @@
if y = x then drop_prefix ys xs else raise FAIL None;
in (ys, drop_prefix ys xs) end;
-fun this_string s = this (explode s) >> (K s);
+fun this_string s = this (explode s) >> K s; (*primitive string -- no symbols yet!*)
fun any _ [] = raise MORE None
| any pred (lst as x :: xs) =
@@ -377,9 +377,7 @@
| Some res => res)
end;
-
end;
-
structure BasicScan: BASIC_SCAN = Scan;
open BasicScan;