# HG changeset patch # User wenzelm # Date 1087411020 -7200 # Node ID 08ee855c1d942214bad93ff7e95570dad8655e5b # Parent f1789e22ceec957202d0f6995444fd116c11ecc1 tuned; diff -r f1789e22ceec -r 08ee855c1d94 doc-src/IsarRef/pure.tex --- 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 diff -r f1789e22ceec -r 08ee855c1d94 doc-src/IsarRef/syntax.tex --- 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,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, \\ \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,\,, 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,\,. 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,\,''. Concerning Isabelle itself, any sequence of the form -\verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol. -Greek letters \verb+\+, \verb+\+, etc. (apart from -\verb+\+), 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} diff -r f1789e22ceec -r 08ee855c1d94 doc-src/Ref/defining.tex --- 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,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~| \\ + & & \verb,\, ~|~ \verb,\, ~|~ \verb,\, ~|~ \verb,\, \\ \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 diff -r f1789e22ceec -r 08ee855c1d94 src/Pure/General/output.ML --- 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 *) diff -r f1789e22ceec -r 08ee855c1d94 src/Pure/General/scan.ML --- 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;