isabelle-cookbook: comparison ProgTutorial/Parsing.thy

equal deleted inserted replaced

-:84aef87b348a
+:ffa5c4ec9611
 fail if you try to consume more than a single character.
 There are three exceptions that are raised by the parsing combinators:
 \begin{itemize}
-\item @{text "FAIL"} is used to indicate that alternative routes of parsing
+\item @{text "FAIL"} indicates that alternative routes of parsing
 might be explored.
 \item @{text "MORE"} indicates that there is not enough input for the parser. For example
 in @{text "($$ \"h\") []"}.
-\item @{text "ABORT"} is the exception that is raised when a dead end is reached.
+\item @{text "ABORT"} indicates that a dead end is reached.
 It is used for example in the function @{ML "!!"} (see below).
 \end{itemize}
 However, note that these exceptions are private to the parser and cannot be accessed
 by the programmer (for example to handle them).
 "Scan.this_string \"hell\" (Symbol.explode \"hello\")"
 "(\"hell\", [\"o\"])"}
 Parsers that explore alternatives can be constructed using the function
 @{ML_ind  "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the
-result of @{text "p"}, in case it succeeds, otherwise it returns the
+result of @{text "p"}, in case it succeeds; otherwise it returns the
 result of @{text "q"}. For example:
 @{ML_response [display,gray]
 "let
 (just_e input, just_h input)
 end"
 "((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
 The parser @{ML "Scan.optional p x" for p x} returns the result of the parser
-@{text "p"}, if it succeeds; otherwise it returns
+@{text "p"}, in case it succeeds; otherwise it returns
 the default value @{text "x"}. For example:
 @{ML_response [display,gray]
 "let
 val p = Scan.optional ($$ \"h\") \"x\"
 To see this assume that @{text p} is present in the input, but it is not
 followed by @{text q}. That means @{ML "(p -- q)" for p q} will fail and
 hence the alternative parser @{text r} will be tried. However, in many
 circumstances this will be the wrong parser for the input ``@{text "p"}-followed-by-something''
 and therefore will also fail. The error message is then caused by the failure
-of @{text r}, not by the absence of @{text q} in the input. This kind of
+of @{text r}, not by the absence of @{text q} in the input. Such
 situation can be avoided when using the function @{ML "!!"}.  This function
 aborts the whole process of parsing in case of a failure and prints an error
 message. For example if you invoke the parser
 "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
 yields the expected parsing.
 The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as
-often as it succeeds. For example:
+long as it succeeds. For example:
 @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
 "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
 Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
 \isacommand{imports}~@{text Main}\\
 \isacommand{keywords} @{text [quotes] "foobar"} @{text "::"} @{text "thy_decl"}\\
 ...
 \end{graybox}
-whereby @{ML_ind "thy_decl" in Keyword} indicates the kind of the
+where @{ML_ind "thy_decl" in Keyword} indicates the kind of the
 command.  Another possible kind is @{text "thy_goal"}, or you can
 also omit the kind entirely, in which case you declare a keyword
 (something that is part of a command).
 Now you can implement \isacommand{foobar} as follows.
 section {* Proof-General and Keyword Files *}
 text {*
 In order to use a new command in Emacs and Proof-General, you need a keyword
 file that can be loaded by ProofGeneral. To keep things simple we take as
-running example the command \isacommand{foobar} from the previous section.
+a running example the command \isacommand{foobar} from the previous section.
 A keyword file can be generated with the command-line:
 @{text [display] "$ isabelle keywords -k foobar some_log_files"}
 be used to generate a keyword file containing the command \isacommand{foobar}.
 \label{fig:commandtheory}}
 \end{figure}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 For our purposes it is sufficient to use the log files of the theories
 @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
 the log file for the theory @{text "Command.thy"}, which contains the new
 \isacommand{foobar}-command. If you target other logics besides HOL, such
 as Nominal or ZF, then you need to adapt the log files appropriately.
 @{text Pure} and @{text HOL} are usually compiled during the installation of
 Isabelle. So log files for them should be already available. If not, then
-they can be conveniently compiled with the help of the build-script from the Isabelle
+they can be easily compiled with the build-script from the Isabelle
 distribution.
 @{text [display]
 "$ ./build -m \"Pure\"
 $ ./build -m \"HOL\""}
 @{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
 For the theory @{text "Command.thy"}, you first need to create a ``managed'' subdirectory
 with:
-@{text [display] "$ isabelle mkdir FoobarCommand"}
+@{text [display] "$ isabelle mkroot -d FoobarCommand"}
 This generates a directory containing the files:
 @{text [display]
-"./IsaMakefile
+"./FoobarCommand/ROOT
-./FoobarCommand/ROOT.ML
 ./FoobarCommand/document
 ./FoobarCommand/document/root.tex"}
 You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
 and add the line
 @{text [display] "no_document use_thy \"Command\";"}
-to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing:
+to the file @{text "./FoobarCommand/ROOT"}. You can now compile the theory by just typing:
-@{text [display] "$ isabelle make"}
+@{text [display] "$ isabelle build"}
 If the compilation succeeds, you have finally created all the necessary log files.
 They are stored in the directory
 @{text [display]  "~/.isabelle/heaps/Isabelle2012/polyml-5.2.1_x86-linux/log"}
 section {* Methods (TBD) *}
 text {*
 (FIXME: maybe move to after the tactic section)
-Methods are central to Isabelle. They are the ones you use for example
+Methods are central to Isabelle. You use them, for example,
 in \isacommand{apply}. To print out all currently known methods you can use the
 Isabelle command:
 \begin{isabelle}
 \isacommand{print\_methods}\\

changeset 559	ffa5c4ec9611
parent 558	84aef87b348a
child 563	50d3059de9c6