# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1312066858 -3600
# Node ID 1bbe4268664d328ed119dec7ebac1cede7f3857a
# Parent  f65b9f14d5dead2e486a7aae18df7b3541d7b8bd
updated to new Isabelle

diff -r f65b9f14d5de -r 1bbe4268664d ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Tue Jun 28 09:22:00 2011 +0100
+++ b/ProgTutorial/Parsing.thy	Sun Jul 31 00:00:58 2011 +0100
@@ -222,18 +222,19 @@
   aborts the whole process of parsing in case of a failure and prints an error
   message. For example if you invoke the parser
 
-  
-  @{ML [display,gray] "!! (fn _ => \"foo\") ($$ \"h\")"}
 
+  @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"}
+*}
+text {*
   on @{text [quotes] "hello"}, the parsing succeeds
 
   @{ML_response [display,gray] 
-  "(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" 
+  "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" 
   "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
 
   but if you invoke it on @{text [quotes] "world"}
-  
-  @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
+
+  @{ML_response_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
                                "Exception ABORT raised"}
 
   then the parsing aborts and the error message @{text "foo"} is printed. In order to
@@ -241,7 +242,7 @@
   @{ML_ind error in Scan}. For example:
 
   @{ML_response_fake [display,gray] 
-  "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
+  "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\"))"
   "Exception Error \"foo\" raised"}
 
   This ``prefixing'' is usually done by wrappers such as @{ML_ind local_theory in Outer_Syntax} 
@@ -256,7 +257,7 @@
 let 
   val err_msg = fn _ => p ^ " is not followed by " ^ q
 in
-  ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
+  ($$ p -- (!! (fn _ => err_msg) ($$ q))) || ($$ r -- $$ r)
 end *}
 
 
diff -r f65b9f14d5de -r 1bbe4268664d ProgTutorial/Recipes/ExternalSolver.thy
--- a/ProgTutorial/Recipes/ExternalSolver.thy	Tue Jun 28 09:22:00 2011 +0100
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Sun Jul 31 00:00:58 2011 +0100
@@ -10,7 +10,7 @@
   You want to use an external application.
   \smallskip
 
-  {\bf Solution:} The function @{ML bash_output} might be the right thing for
+  {\bf Solution:} The function @{ML bash_output in Isabelle_System} might be the right thing for
   you.
   \smallskip
 
@@ -20,7 +20,7 @@
   For example, consider running an ordinary shell commands:
 
   @{ML_response [display,gray] 
-    "bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
+    "Isabelle_System.bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
 
   Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
   on Page~\pageref{rec:timeout}), i.e. external applications are killed
@@ -28,10 +28,10 @@
   one second:
 
   @{ML_response_fake [display,gray] 
-    "TimeLimit.timeLimit (Time.fromSeconds 1) bash_output \"sleep 30\"
+    "TimeLimit.timeLimit (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
      handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
 
-  The function @{ML bash_output} can also be used for more reasonable
+  The function @{ML bash_output in Isabelle_System} can also be used for more reasonable
   applications, e.g. coupling external solvers with Isabelle. In that case,
   one has to make sure that Isabelle can find the particular executable.
   One way to ensure this is by adding a Bash-like variable binding into
@@ -46,7 +46,7 @@
 
   In Isabelle, this application may now be executed by
 
-  @{ML_response_fake [display,gray] "bash_output \"$FOO\"" "\<dots>"}
+  @{ML_response_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"}
 *}
 
 
diff -r f65b9f14d5de -r 1bbe4268664d progtutorial.pdf
Binary file progtutorial.pdf has changed