# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1401277269 -3600
# Node ID 3c214b215f7efa2f90f86ef879d82e9e425f4028
# Parent  2c34c69236cef5fe7587754ba7d71dbcb8e4aaf4
some small updates for Isabelle and corrections in the Parsing chapter

diff -r 2c34c69236ce -r 3c214b215f7e ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Sun Apr 06 12:45:54 2014 +0100
+++ b/ProgTutorial/Parsing.thy	Wed May 28 12:41:09 2014 +0100
@@ -1,5 +1,7 @@
 theory Parsing
-imports Base "Helper/Command/Command" "Package/Simple_Inductive_Package"
+imports Base "Package/Simple_Inductive_Package"
+keywords "foobar" "foobar_trace" :: thy_decl and
+         "foobar_goal" "foobar_prove" :: thy_goal
 begin
 
 chapter {* Parsing\label{chp:parsing} *}
@@ -71,8 +73,10 @@
   "($$ \"x\") (Symbol.explode \"world\")" 
   "Exception FAIL raised"}
   
-  will raise the exception @{text "FAIL"}.  There are three exceptions used in
-  the parsing combinators:
+  will raise the exception @{text "FAIL"}. The function @{ML_ind "$$" in Scan} will also
+  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 
@@ -223,8 +227,7 @@
 
 
   @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"}
-*}
-text {*
+
   on @{text [quotes] "hello"}, the parsing succeeds
 
   @{ML_response [display,gray] 
@@ -241,10 +244,11 @@
   @{ML_ind error in Scan}. For example:
 
   @{ML_response_fake [display,gray] 
-  "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\"))"
+  "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
   "Exception Error \"foo\" raised"}
 
-  This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in Outer_Syntax} 
+  This kind of ``prefixing'' to see the correct error message is usually done by wrappers 
+  such as @{ML_ind local_theory in Outer_Syntax} 
   (see Section~\ref{sec:newcommand} which explains this function in more detail). 
   
   Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
diff -r 2c34c69236ce -r 3c214b215f7e ProgTutorial/Recipes/Sat.thy
--- a/ProgTutorial/Recipes/Sat.thy	Sun Apr 06 12:45:54 2014 +0100
+++ b/ProgTutorial/Recipes/Sat.thy	Wed May 28 12:41:09 2014 +0100
@@ -66,35 +66,30 @@
   to see better which assignment the table contains.
  
   Having produced a propositional formula, you can now call the SAT solvers 
-  with the function @{ML "SatSolver.invoke_solver"}. For example
+  with the function @{ML "SAT_Solver.invoke_solver"}. For example
 
   @{ML_response_fake [display,gray]
-  "SatSolver.invoke_solver \"dpll\" pform"
-  "SatSolver.SATISFIABLE assg"}
+  "SAT_Solver.invoke_solver \"minisat\" pform"
+  "SAT_Solver.SATISFIABLE assg"}
 
   determines that the formula @{ML pform} is satisfiable. If we inspect
   the returned function @{text assg}
 
   @{ML_response [display,gray]
 "let
-  val SatSolver.SATISFIABLE assg = SatSolver.invoke_solver \"dpll\" pform
+  val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform
 in 
   (assg 1, assg 2, assg 3)
 end"
   "(SOME true, SOME true, NONE)"}
 
-  we obtain a possible assignment for the variables @{text "A"} and @{text "B"}
+  we obtain a possible assignment for the variables @{text "A"} an @{text "B"}
   that makes the formula satisfiable. 
 
-  Note that we invoked the SAT solver with the string @{text [quotes] dpll}. 
-  This string specifies which SAT solver is invoked (in this case the internal
-  one). If instead you invoke the SAT solver with the string @{text [quotes] "auto"}
-
-  @{ML [display,gray] "SatSolver.invoke_solver \"auto\" pform"}
-
+  Note that we invoked the SAT solver with the string @{text [quotes] auto}. 
+  This string specifies which specific SAT solver is invoked. If instead 
+  called with @{text [quotes] "auto"}
   several external SAT solvers will be tried (assuming they are installed). 
-  If no external SAT solver is installed, then the default is 
-  @{text [quotes] "dpll"}.
 
   There are also two tactics that make use of SAT solvers. One 
   is the tactic @{ML sat_tac in SAT}. For example 
diff -r 2c34c69236ce -r 3c214b215f7e ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sun Apr 06 12:45:54 2014 +0100
+++ b/ProgTutorial/Tactical.thy	Wed May 28 12:41:09 2014 +0100
@@ -388,7 +388,7 @@
  
 lemma 
   shows "False \<Longrightarrow> True"
-apply(tactic {* print_tac "foo message" *})
+apply(tactic {* print_tac @{context} "foo message" *})
 txt{*gives:
      \begin{isabelle}
      @{text "foo message"}\\[3mm] 
diff -r 2c34c69236ce -r 3c214b215f7e ROOT
--- a/ROOT	Sun Apr 06 12:45:54 2014 +0100
+++ b/ROOT	Wed May 28 12:41:09 2014 +0100
@@ -5,7 +5,6 @@
     "~~/src/HOL/Number_Theory/Primes" 
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Code_Abstract_Nat"
-    "Helper/Command/Command"
   theories [quick_and_dirty, document = false] 
     "Intro"
     "First_Steps"
@@ -37,7 +36,6 @@
     "~~/src/HOL/Number_Theory/Primes" 
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Code_Abstract_Nat"
-    "Helper/Command/Command"
   theories [quick_and_dirty, document = true] 
     "Intro"
     "First_Steps"
@@ -60,9 +58,9 @@
     "Recipes/Sat"
     "Recipes/USTypes"
     "Solutions"
-  files 
-    "document/root.bib" 
-    "document/root.tex" 
-    "document/build"
+  document_files 
+    "root.bib" 
+    "root.tex" 
+    "build"
 
 
diff -r 2c34c69236ce -r 3c214b215f7e progtutorial.pdf
Binary file progtutorial.pdf has changed