diff -r 84aef87b348a -r ffa5c4ec9611 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Wed Aug 20 14:42:14 2014 +0100
+++ b/ProgTutorial/Parsing.thy	Wed Oct 15 23:12:54 2014 +0100
@@ -79,11 +79,11 @@
   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}
 
@@ -142,7 +142,7 @@
 
   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:
 
 
@@ -173,7 +173,7 @@
   "((\"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]
@@ -220,7 +220,7 @@
   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
@@ -280,7 +280,7 @@
   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\"])"}
@@ -970,7 +970,7 @@
   ...
   \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).
@@ -1190,7 +1190,7 @@
 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:
 
@@ -1230,6 +1230,7 @@
   \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
@@ -1238,7 +1239,7 @@
   
   @{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] 
@@ -1251,26 +1252,24 @@
 
   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.ML
+"./FoobarCommand/ROOT
 ./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 
@@ -1469,7 +1468,7 @@
 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: