
diff -r cd861a121f60 -r 2a69b119cdee CookBook/Parsing.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Parsing.thy	Sat Sep 06 04:32:18 2008 +0200
@@ -0,0 +1,660 @@
+theory Parsing
+imports Main
+
+begin
+
+chapter {* Parsing *}
+
+text {*
+
+  Lots of Standard ML code is given in this document, for various reasons,
+  including:
+  \begin{itemize}
+  \item direct quotation of code found in the Isabelle source files,
+  or simplified versions of such code
+  \item identifiers found in the Isabelle source code, with their types 
+  (or specialisations of their types)
+  \item code examples, which can be run by the reader, to help illustrate the
+  behaviour of functions found in the Isabelle source code
+  \item ancillary functions, not from the Isabelle source code, 
+  which enable the reader to run relevant code examples
+  \item type abbreviations, which help explain the uses of certain functions
+  \end{itemize}
+
+*}
+
+section {* Parsing Isar input *}
+
+text {*
+
+  The typical parsing function has the type
+  \texttt{'src -> 'res * 'src}, with input  
+  of type \texttt{'src}, returning a result 
+  of type \texttt{'res}, which is (or is derived from) the first part of the
+  input, and also returning the remainder of the input.
+  (In the common case, when it is clear what the ``remainder of the input''
+  means, we will just say that the functions ``returns'' the
+  value of type \texttt{'res}). 
+  An exception is raised if an appropriate value 
+  cannot be produced from the input.
+  A range of exceptions can be used to identify different reasons 
+  for the failure of a parse.
+  
+  This contrasts the standard parsing function in Standard ML,
+  which is of type 
+  \texttt{type ('res, 'src) reader = 'src -> ('res * 'src) option};
+  (for example, \texttt{List.getItem} and \texttt{Substring.getc}).
+  However, much of the discussion at 
+  FIX file:/home/jeremy/html/ml/SMLBasis/string-cvt.html
+  is relevant.
+
+  Naturally one may convert between the two different sorts of parsing functions
+  as follows:
+  \begin{verbatim}
+  open StringCvt ;
+  type ('res, 'src) ex_reader = 'src -> 'res * 'src
+  (* ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader *)
+  fun ex_reader rdr src = Option.valOf (rdr src) ;
+  (* reader : ('res, 'src) ex_reader -> ('res, 'src) reader *)
+  fun reader exrdr src = SOME (exrdr src) handle _ => NONE ;
+  \end{verbatim}
+  
+*}
+
+section{* The \texttt{Scan} structure *}
+
+text {* 
+  The source file is \texttt{src/General/scan.ML}.
+  This structure provides functions for using and combining parsing functions
+  of the type \texttt{'src -> 'res * 'src}.
+  Three exceptions are used:
+  \begin{verbatim}
+  exception MORE of string option;  (*need more input (prompt)*)
+  exception FAIL of string option;  (*try alternatives (reason of failure)*)
+  exception ABORT of string;        (*dead end*)
+  \end{verbatim}
+  Many functions in this structure (generally those with names composed of
+  symbols) are declared as infix.
+
+  Some functions from that structure are
+  \begin{verbatim}
+  |-- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
+  'src -> 'res2 * 'src''
+  --| : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
+  'src -> 'res1 * 'src''
+  -- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
+  'src -> ('res1 * 'res2) * 'src''
+  ^^ : ('src -> string * 'src') * ('src' -> string * 'src'') ->
+  'src -> string * 'src''
+  \end{verbatim}
+  These functions parse a result off the input source twice.
+
+  \texttt{|--} and \texttt{--|} 
+  return the first result and the second result, respectively.
+
+  \texttt{--} returns both.
+
+  \verb|^^| returns the result of concatenating the two results
+  (which must be strings).
+
+  Note how, although the types 
+  \texttt{'src}, \texttt{'src'} and \texttt{'src''} will normally be the same,
+  the types as shown help suggest the behaviour of the functions.
+  \begin{verbatim}
+  :-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->
+  'src -> ('res1 * 'res2) * 'src''
+  :|-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->
+  'src -> 'res2 * 'src''
+  \end{verbatim}
+  These are similar to \texttt{|--} and \texttt{--|},
+  except that the second parsing function can depend on the result of the first.
+  \begin{verbatim}
+  >> : ('src -> 'res1 * 'src') * ('res1 -> 'res2) -> 'src -> 'res2 * 'src'
+  || : ('src -> 'res_src) * ('src -> 'res_src) -> 'src -> 'res_src
+  \end{verbatim}
+  \texttt{p >> f} applies a function \texttt{f} to the result of a parse.
+  
+  \texttt{||} tries a second parsing function if the first one
+  fails by raising an exception of the form \texttt{FAIL \_}.
+  
+  \begin{verbatim}
+  succeed : 'res -> ('src -> 'res * 'src) ;
+  fail : ('src -> 'res_src) ;
+  !! : ('src * string option -> string) -> 
+  ('src -> 'res_src) -> ('src -> 'res_src) ;
+  \end{verbatim}
+  \texttt{succeed r} returns \texttt{r}, with the input unchanged.
+  \texttt{fail} always fails, raising exception \texttt{FAIL NONE}.
+  \texttt{!! f} only affects the failure mode, turning a failure that
+  raises \texttt{FAIL \_} into a failure that raises \texttt{ABORT ...}.
+  This is used to prevent recovery from the failure ---
+  thus, in \texttt{!! parse1 || parse2}, if \texttt{parse1} fails, 
+  it won't recover by trying \texttt{parse2}.
+
+  \begin{verbatim}
+  one : ('si -> bool) -> ('si list -> 'si * 'si list) ;
+  some : ('si -> 'res option) -> ('si list -> 'res * 'si list) ;
+  \end{verbatim}
+  These require the input to be a list of items:
+  they fail, raising \texttt{MORE NONE} if the list is empty.
+  On other failures they raise \texttt{FAIL NONE} 
+
+  \texttt{one p} takes the first
+  item from the list if it satisfies \texttt{p}, otherwise fails.
+
+  \texttt{some f} takes the first
+  item from the list and applies \texttt{f} to it, failing if this returns
+  \texttt{NONE}.  
+
+  \begin{verbatim}
+  many : ('si -> bool) -> 'si list -> 'si list * 'si list ; 
+  \end{verbatim}
+  \texttt{many p} takes items from the input until it encounters one 
+  which does not satisfy \texttt{p}.  If it reaches the end of the input
+  it fails, raising \texttt{MORE NONE}.
+
+  \texttt{many1} (with the same type) fails if the first item 
+  does not satisfy \texttt{p}.  
+
+  \begin{verbatim}
+  option : ('src -> 'res * 'src) -> ('src -> 'res option * 'src)
+  optional : ('src -> 'res * 'src) -> 'res -> ('src -> 'res * 'src)
+  \end{verbatim}
+  \texttt{option}: 
+  where the parser \texttt{f} succeeds with result \texttt{r} 
+  or raises \texttt{FAIL \_},
+  \texttt{option f} gives the result \texttt{SOME r} or \texttt{NONE}.
+  
+  \texttt{optional}: if parser \texttt{f} fails by raising \texttt{FAIL \_},
+  \texttt{optional f default} provides the result \texttt{default}.
+
+  \begin{verbatim}
+  repeat : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
+  repeat1 : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
+  bulk : ('src -> 'res * 'src) -> 'src -> 'res list * 'src 
+  \end{verbatim}
+  \texttt{repeat f} repeatedly parses an item off the remaining input until 
+  \texttt{f} fails with \texttt{FAIL \_}
+
+  \texttt{repeat1} is as for \texttt{repeat}, but requires at least one
+  successful parse.
+
+  \begin{verbatim}
+  lift : ('src -> 'res * 'src) -> ('ex * 'src -> 'res * ('ex * 'src))
+  \end{verbatim}
+  \texttt{lift} changes the source type of a parser by putting in an extra
+  component \texttt{'ex}, which is ignored in the parsing.
+
+  The \texttt{Scan} structure also provides the type \texttt{lexicon}, 
+  HOW DO THEY WORK ?? TO BE COMPLETED
+  \begin{verbatim}
+  dest_lexicon: lexicon -> string list ;
+  make_lexicon: string list list -> lexicon ;
+  empty_lexicon: lexicon ;
+  extend_lexicon: string list list -> lexicon -> lexicon ;
+  merge_lexicons: lexicon -> lexicon -> lexicon ;
+  is_literal: lexicon -> string list -> bool ;
+  literal: lexicon -> string list -> string list * string list ;
+  \end{verbatim}
+  Two lexicons, for the commands and keywords, are stored and can be retrieved
+  by:
+  \begin{verbatim}
+  val (command_lexicon, keyword_lexicon) = OuterSyntax.get_lexicons () ;
+  val commands = Scan.dest_lexicon command_lexicon ;
+  val keywords = Scan.dest_lexicon keyword_lexicon ;
+  \end{verbatim}
+*}
+
+section{* The \texttt{OuterLex} structure *}
+
+text {*
+  The source file is @{text "src/Pure/Isar/outer_lex.ML"}.
+  In some other source files its name is abbreviated:
+  \begin{verbatim}
+  structure T = OuterLex;
+  \end{verbatim}
+  This structure defines the type \texttt{token}.
+  (The types
+  \texttt{OuterLex.token},
+  \texttt{OuterParse.token} and
+  \texttt{SpecParse.token} are all the same).
+  
+  Input text is split up into tokens, and the input source type for many parsing
+  functions is \texttt{token list}.
+
+  The datatype definition (which is not published in the signature) is
+  \begin{verbatim}
+  datatype token = Token of Position.T * (token_kind * string);
+  \end{verbatim}
+  but here are some runnable examples for viewing tokens: 
+
+*}
+
+text {*
+  FIXME
+
+  @{text "
+  begin{verbatim}
+  type token = T.token ;
+  val toks : token list = OuterSyntax.scan ``theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }'' ;
+  print_depth 20 ;
+  List.map T.text_of toks ;
+  val proper_toks = List.filter T.is_proper toks ;
+  List.map T.kind_of proper_toks ;
+  List.map T.unparse proper_toks ;
+  List.map T.val_of proper_toks ;
+  end{verbatim}"}
+
+*}
+
+text {*
+
+  The function \texttt{is\_proper : token -> bool} identifies tokens which are
+  not white space or comments: many parsing functions assume require spaces or
+  comments to have been filtered out.
+  
+  There is a special end-of-file token:
+  \begin{verbatim}
+  val (tok_eof : token, is_eof : token -> bool) = T.stopper ; 
+  (* end of file token *)
+  \end{verbatim}
+
+*}
+
+section {* The \texttt{OuterParse} structure *}
+
+text {*
+  The source file is \texttt{src/Pure/Isar/outer\_parse.ML}.
+  In some other source files its name is abbreviated:
+  \begin{verbatim}
+  structure P = OuterParse;
+  \end{verbatim}
+  Here the parsers use \texttt{token list} as the input source type. 
+  
+  Some of the parsers simply select the first token, provided that it is of the
+  right kind (as returned by \texttt{T.kind\_of}): these are 
+  \texttt{ command, keyword, short\_ident, long\_ident, sym\_ident, term\_var,
+  type\_ident, type\_var, number, string, alt\_string, verbatim, sync, eof}
+  Others select the first token, provided that it is one of several kinds,
+  (eg, \texttt{name, xname, text, typ}).
+
+  \begin{verbatim}
+  type 'a tlp = token list -> 'a * token list ; (* token list parser *)
+  $$$ : string -> string tlp
+  nat : int tlp ;
+  maybe : 'a tlp -> 'a option tlp ;
+  \end{verbatim}
+
+  \texttt{\$\$\$ s} returns the first token,
+  if it equals \texttt{s} \emph{and} \texttt{s} is a keyword.
+
+  \texttt{nat} returns the first token, if it is a number, and evaluates it.
+
+  \texttt{maybe}: if \texttt{p} returns \texttt{r}, 
+  then \texttt{maybe p} returns \texttt{SOME r} ;
+  if the first token is an underscore, it returns \texttt{NONE}.
+
+  A few examples:
+  \begin{verbatim}
+  P.list : 'a tlp -> 'a list tlp ; (* likewise P.list1 *)
+  P.and_list : 'a tlp -> 'a list tlp ; (* likewise P.and_list1 *)
+  val toks : token list = OuterSyntax.scan "44 ,_, 66,77" ;
+  val proper_toks = List.filter T.is_proper toks ;
+  P.list P.nat toks ; (* OK, doesn't recognize white space *)
+  P.list P.nat proper_toks ; (* fails, doesn't recognize what follows ',' *)
+  P.list (P.maybe P.nat) proper_toks ; (* fails, end of input *)
+  P.list (P.maybe P.nat) (proper_toks @ [tok_eof]) ; (* OK *)
+  val toks : token list = OuterSyntax.scan "44 and 55 and 66 and 77" ;
+  P.and_list P.nat (List.filter T.is_proper toks @ [tok_eof]) ; (* ??? *)
+  \end{verbatim}
+
+  The following code helps run examples:
+  \begin{verbatim}
+  fun parse_str tlp str = 
+  let val toks : token list = OuterSyntax.scan str ;
+  val proper_toks = List.filter T.is_proper toks @ [tok_eof] ;
+  val (res, rem_toks) = tlp proper_toks ;
+  val rem_str = String.concat
+  (Library.separate " " (List.map T.unparse rem_toks)) ;
+  in (res, rem_str) end ;
+  \end{verbatim}
+
+  Some examples from \texttt{src/Pure/Isar/outer\_parse.ML}
+  \begin{verbatim}
+  val type_args =
+  type_ident >> Library.single ||
+  $$$ "(" |-- !!! (list1 type_ident --| $$$ ")") ||
+  Scan.succeed [];
+  \end{verbatim}
+  There are three ways parsing a list of type arguments can succeed.
+  The first line reads a single type argument, and turns it into a singleton
+  list.
+  The second line reads "(", and then the remainder, ignoring the "(" ;
+  the remainder consists of a list of type identifiers (at least one),
+  and then a ")" which is also ignored.
+  The \texttt{!!!} ensures that if the parsing proceeds this far and then fails,
+  it won't try the third line (see the description of \texttt{Scan.!!}).
+  The third line consumes no input and returns the empty list.
+
+  \begin{verbatim}
+  fun triple2 (x, (y, z)) = (x, y, z);
+  val arity = xname -- ($$$ "::" |-- !!! (
+  Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) []
+  -- sort)) >> triple2;
+  \end{verbatim}
+  The parser \texttt{arity} reads a typename $t$, then ``\texttt{::}'' (which is
+  ignored), then optionally a list $ss$ of sorts and then another sort $s$.
+  The result $(t, (ss, s))$ is transformed by \texttt{triple2} to $(t, ss, s)$.
+  The second line reads the optional list of sorts:
+  it reads first ``\texttt{(}'' and last ``\texttt{)}'', which are both ignored,
+  and between them a comma-separated list of sorts.
+  If this list is absent, the default \texttt{[]} provides the list of sorts.
+
+  \begin{verbatim}
+  parse_str P.type_args "('a, 'b) ntyp" ;
+  parse_str P.type_args "'a ntyp" ;
+  parse_str P.type_args "ntyp" ;
+  parse_str P.arity "ty :: tycl" ;
+  parse_str P.arity "ty :: (tycl1, tycl2) tycl" ;
+  \end{verbatim}
+
+*}
+
+section {* The \texttt{SpecParse} structure *}
+
+text {*
+  The source file is \texttt{src/Pure/Isar/spec\_parse.ML}.
+  This structure contains token list parsers for more complicated values.
+  For example, 
+  \begin{verbatim}
+  open SpecParse ;
+  attrib : Attrib.src tok_rdr ; 
+  attribs : Attrib.src list tok_rdr ;
+  opt_attribs : Attrib.src list tok_rdr ;
+  xthm : (thmref * Attrib.src list) tok_rdr ;
+  xthms1 : (thmref * Attrib.src list) list tok_rdr ;
+  
+  parse_str attrib "simp" ;
+  parse_str opt_attribs "hello" ;
+  val (ass, "") = parse_str attribs "[standard, xxxx, simp, intro, OF sym]" ;
+  map Args.dest_src ass ;
+  val (asrc, "") = parse_str attrib "THEN trans [THEN sym]" ;
+  
+  parse_str xthm "mythm [attr]" ;
+  parse_str xthms1 "thm1 [attr] thms2" ;
+  \end{verbatim}
+  
+  As you can see, attributes are described using types of the \texttt{Args}
+  structure, described below.
+*}
+
+section{* The \texttt{Args} structure *}
+
+text {*
+  The source file is \texttt{src/Pure/Isar/args.ML}.
+  The primary type of this structure is the \texttt{src} datatype;
+  the single constructors not published in the signature, but 
+  \texttt{Args.src} and \texttt{Args.dest\_src}
+  are in fact the constructor and destructor functions.
+  Note that the types \texttt{Attrib.src} and \texttt{Method.src}
+  are in fact \texttt{Args.src}.
+
+  \begin{verbatim}
+  src : (string * Args.T list) * Position.T -> Args.src ;
+  dest_src : Args.src -> (string * Args.T list) * Position.T ;
+  Args.pretty_src : Proof.context -> Args.src -> Pretty.T ;
+  fun pr_src ctxt src = Pretty.string_of (Args.pretty_src ctxt src) ;
+
+  val thy = ML_Context.the_context () ;
+  val ctxt = ProofContext.init thy ;
+  map (pr_src ctxt) ass ;
+  \end{verbatim}
+
+  So an \texttt{Args.src} consists of the first word, then a list of further 
+  ``arguments'', of type \texttt{Args.T}, with information about position in the
+  input.
+  \begin{verbatim}
+  (* how an Args.src is parsed *)
+  P.position : 'a tlp -> ('a * Position.T) tlp ;
+  P.arguments : Args.T list tlp ;
+
+  val parse_src : Args.src tlp =
+  P.position (P.xname -- P.arguments) >> Args.src ;
+  \end{verbatim}
+
+  \begin{verbatim}
+  val ((first_word, args), pos) = Args.dest_src asrc ;
+  map Args.string_of args ;
+  \end{verbatim}
+
+  The \texttt{Args} structure contains more parsers and parser transformers 
+  for which the input source type is \texttt{Args.T list}.  For example,
+  \begin{verbatim}
+  type 'a atlp = Args.T list -> 'a * Args.T list ;
+  open Args ;
+  nat : int atlp ; (* also Args.int *)
+  thm_sel : PureThy.interval list atlp ;
+  list : 'a atlp -> 'a list atlp ;
+  attribs : (string -> string) -> Args.src list atlp ;
+  opt_attribs : (string -> string) -> Args.src list atlp ;
+  
+  (* parse_atl_str : 'a atlp -> (string -> 'a * string) ;
+  given an Args.T list parser, to get a string parser *)
+  fun parse_atl_str atlp str = 
+  let val (ats, rem_str) = parse_str P.arguments str ;
+  val (res, rem_ats) = atlp ats ;
+  in (res, String.concat (Library.separate " "
+  (List.map Args.string_of rem_ats @ [rem_str]))) end ;
+
+  parse_atl_str Args.int "-1-," ;
+  parse_atl_str (Scan.option Args.int) "x1-," ;
+  parse_atl_str Args.thm_sel "(1-,4,13-22)" ;
+
+  val (ats as atsrc :: _, "") = parse_atl_str (Args.attribs I)
+  "[THEN trans [THEN sym], simp, OF sym]" ;
+  \end{verbatim}
+
+  From here, an attribute is interpreted using \texttt{Attrib.attribute}.
+
+  \texttt{Args} has a large number of functions which parse an \texttt{Args.src}
+  and also refer to a generic context.  
+  Note the use of \texttt{Scan.lift} for this.
+  (as does \texttt{Attrib} - RETHINK THIS)
+  
+  (\texttt{Args.syntax} shown below has type specialised)
+
+  \begin{verbatim}
+  type ('res, 'src) parse_fn = 'src -> 'res * 'src ;
+  type 'a cgatlp = ('a, Context.generic * Args.T list) parse_fn ;
+  Scan.lift : 'a atlp -> 'a cgatlp ;
+  term : term cgatlp ;
+  typ : typ cgatlp ;
+  
+  Args.syntax : string -> 'res cgatlp -> src -> ('res, Context.generic) parse_fn ;
+  Attrib.thm : thm cgatlp ;
+  Attrib.thms : thm list cgatlp ;
+  Attrib.multi_thm : thm list cgatlp ;
+  
+  (* parse_cgatl_str : 'a cgatlp -> (string -> 'a * string) ;
+  given a (Context.generic * Args.T list) parser, to get a string parser *)
+  fun parse_cgatl_str cgatlp str = 
+  let 
+    (* use the current generic context *)
+    val generic = Context.Theory thy ;
+    val (ats, rem_str) = parse_str P.arguments str ;
+    (* ignore any change to the generic context *)
+    val (res, (_, rem_ats)) = cgatlp (generic, ats) ;
+  in (res, String.concat (Library.separate " "
+      (List.map Args.string_of rem_ats @ [rem_str]))) end ;
+  \end{verbatim}
+*}
+
+section{* Attributes, and the \texttt{Attrib} structure *}
+
+text {*
+  The type \texttt{attribute} is declared in \texttt{src/Pure/thm.ML}.
+  The source file for the \texttt{Attrib} structure is
+  \texttt{src/Pure/Isar/attrib.ML}.
+  Most attributes use a theorem to change a generic context (for example, 
+  by declaring that the theorem should be used, by default, in simplification),
+  or change a theorem (which most often involves referring to the current
+  theory). 
+  The functions \texttt{Thm.rule\_attribute} and
+  \texttt{Thm.declaration\_attribute} create attributes of these kinds.
+
+  \begin{verbatim}
+  type attribute = Context.generic * thm -> Context.generic * thm;
+  type 'a trf = 'a -> 'a ; (* transformer of a given type *)
+  Thm.rule_attribute  : (Context.generic -> thm -> thm) -> attribute ;
+  Thm.declaration_attribute : (thm -> Context.generic trf) -> attribute ;
+
+  Attrib.print_attributes : theory -> unit ;
+  Attrib.pretty_attribs : Proof.context -> src list -> Pretty.T list ;
+
+  List.app Pretty.writeln (Attrib.pretty_attribs ctxt ass) ;
+  \end{verbatim}
+
+  An attribute is stored in a theory as indicated by:
+  \begin{verbatim}
+  Attrib.add_attributes : 
+  (bstring * (src -> attribute) * string) list -> theory trf ; 
+  (*
+  Attrib.add_attributes [("THEN", THEN_att, "resolution with rule")] ;
+  *)
+  \end{verbatim}
+  where the first and third arguments are name and description of the attribute,
+  and the second is a function which parses the attribute input text 
+  (including the attribute name, which has necessarily already been parsed).
+  Here, \texttt{THEN\_att} is a function declared in the code for the
+  structure \texttt{Attrib}, but not published in its signature.
+  The source file \texttt{src/Pure/Isar/attrib.ML} shows the use of 
+  \texttt{Attrib.add\_attributes} to add a number of attributes.
+
+  \begin{verbatim}
+  FullAttrib.THEN_att : src -> attribute ;
+  FullAttrib.THEN_att atsrc (generic, ML_Context.thm "sym") ;
+  FullAttrib.THEN_att atsrc (generic, ML_Context.thm "all_comm") ;
+  \end{verbatim}
+
+  \begin{verbatim}
+  Attrib.syntax : attribute cgatlp -> src -> attribute ;
+  Attrib.no_args : attribute -> src -> attribute ;
+  \end{verbatim}
+  When this is called as \texttt{syntax scan src (gc, th)}
+  the generic context \texttt{gc} is used 
+  (and potentially changed to \texttt{gc'})
+  by \texttt{scan} in parsing to obtain an attribute \texttt{attr} which would
+  then be applied to \texttt{(gc', th)}.
+  The source for parsing the attribute is the arguments part of \texttt{src},
+  which must all be consumed by the parse.
+
+  For example, for \texttt{Attrib.no\_args attr src}, the attribute parser 
+  simply returns \texttt{attr}, requiring that the arguments part of
+  \texttt{src} must be empty.
+
+  Some examples from \texttt{src/Pure/Isar/attrib.ML}, modified:
+  \begin{verbatim}
+  fun rot_att_n n (gc, th) = (gc, rotate_prems n th) ;
+  rot_att_n : int -> attribute ;
+  val rot_arg = Scan.lift (Scan.optional Args.int 1 : int atlp) : int cgatlp ;
+  val rotated_att : src -> attribute =
+  Attrib.syntax (rot_arg >> rot_att_n : attribute cgatlp) ;
+  
+  val THEN_arg : int cgatlp = Scan.lift 
+  (Scan.optional (Args.bracks Args.nat : int atlp) 1 : int atlp) ;
+
+  Attrib.thm : thm cgatlp ;
+
+  THEN_arg -- Attrib.thm : (int * thm) cgatlp ;
+
+  fun THEN_att_n (n, tht) (gc, th) = (gc, th RSN (n, tht)) ;
+  THEN_att_n : int * thm -> attribute ;
+
+  val THEN_att : src -> attribute = Attrib.syntax
+  (THEN_arg -- Attrib.thm >> THEN_att_n : attribute cgatlp);
+  \end{verbatim}
+  The functions I've called \texttt{rot\_arg} and \texttt{THEN\_arg}
+  read an optional argument, which for \texttt{rotated} is an integer, 
+  and for \texttt{THEN} is a natural enclosed in square brackets;
+  the default, if the argument is absent, is 1 in each case.
+  Functions \texttt{rot\_att\_n} and \texttt{THEN\_att\_n} turn these into
+  attributes, where \texttt{THEN\_att\_n} also requires a theorem, which is
+  parsed by \texttt{Attrib.thm}.  
+  Infix operators \texttt{--} and \texttt{>>} are in the structure \texttt{Scan}.
+
+*}
+
+section{* Methods, and the \texttt{Method} structure *}
+
+text {*
+  The source file is \texttt{src/Pure/Isar/method.ML}.
+  The type \texttt{method} is defined by the datatype declaration
+  \begin{verbatim}
+  (* datatype method = Meth of thm list -> cases_tactic; *)
+  RuleCases.NO_CASES : tactic -> cases_tactic ;
+  \end{verbatim}
+  In fact \texttt{RAW\_METHOD\_CASES} (below) is exactly the constructor
+  \texttt{Meth}.
+  A \texttt{cases\_tactic} is an elaborated version of a tactic.
+  \texttt{NO\_CASES tac} is a \texttt{cases\_tactic} which consists of a
+  \texttt{cases\_tactic} without any further case information.
+  For further details see the description of structure \texttt{RuleCases} below.
+  The list of theorems to be passed to a method consists of the current
+  \emph{facts} in the proof.
+  
+  \begin{verbatim}
+  RAW_METHOD : (thm list -> tactic) -> method ;
+  METHOD : (thm list -> tactic) -> method ;
+  
+  SIMPLE_METHOD : tactic -> method ;
+  SIMPLE_METHOD' : (int -> tactic) -> method ;
+  SIMPLE_METHOD'' : ((int -> tactic) -> tactic) -> (int -> tactic) -> method ;
+
+  RAW_METHOD_CASES : (thm list -> cases_tactic) -> method ;
+  METHOD_CASES : (thm list -> cases_tactic) -> method ;
+  \end{verbatim}
+  A method is, in its simplest form, a tactic; applying the method is to apply
+  the tactic to the current goal state.
+
+  Applying \texttt{RAW\_METHOD tacf} creates a tactic by applying 
+  \texttt{tacf} to the current {facts}, and applying that tactic to the
+  goal state.
+
+  \texttt{METHOD} is similar but also first applies
+  \texttt{Goal.conjunction\_tac} to all subgoals.
+
+  \texttt{SIMPLE\_METHOD tac} inserts the facts into all subgoals and then
+  applies \texttt{tacf}.
+
+  \texttt{SIMPLE\_METHOD' tacf} inserts the facts and then
+  applies \texttt{tacf} to subgoal 1.
+
+  \texttt{SIMPLE\_METHOD'' quant tacf} does this for subgoal(s) selected by
+  \texttt{quant}, which may be, for example,
+  \texttt{ALLGOALS} (all subgoals),
+  \texttt{TRYALL} (try all subgoals, failure is OK),
+  \texttt{FIRSTGOAL} (try subgoals until it succeeds once), 
+  \texttt{(fn tacf => tacf 4)} (subgoal 4), etc
+  (see the \texttt{Tactical} structure, \cite[Chapter 4]{ref}).
+
+  A method is stored in a theory as indicated by:
+  \begin{verbatim}
+  Method.add_method : 
+  (bstring * (src -> Proof.context -> method) * string) -> theory trf ; 
+  ( *
+  * )
+  \end{verbatim}
+  where the first and third arguments are name and description of the method,
+  and the second is a function which parses the method input text 
+  (including the method name, which has necessarily already been parsed).
+
+  Here, \texttt{xxx} is a function declared in the code for the
+  structure \texttt{Method}, but not published in its signature.
+  The source file \texttt{src/Pure/Isar/method.ML} shows the use of 
+  \texttt{Method.add\_method} to add a number of methods.
+
+
+*}
+
+
+end 
\ No newline at end of file




