# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1396784754 -3600
# Node ID 2c34c69236cef5fe7587754ba7d71dbcb8e4aaf4
# Parent  638ed040e6f8b59d3b0c30526643aa13788b11a5
updated to new isabelle

diff -r 638ed040e6f8 -r 2c34c69236ce ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Thu Apr 03 12:16:56 2014 +0100
+++ b/ProgTutorial/Essential.thy	Sun Apr 06 12:45:54 2014 +0100
@@ -178,7 +178,7 @@
   can use the following ML-function to set the printing depth to a higher 
   value:
 
-  @{ML [display,gray] "print_depth 50"}
+  @{ML [display,gray] "default_print_depth 50"}
   \end{exercise}
 
   The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 
diff -r 638ed040e6f8 -r 2c34c69236ce ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Thu Apr 03 12:16:56 2014 +0100
+++ b/ProgTutorial/Parsing.thy	Sun Apr 06 12:45:54 2014 +0100
@@ -561,7 +561,7 @@
 end" 
 "([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
 
-  You might have to adjust the @{ML_ind print_depth} in order to
+  You might have to adjust the @{ML_ind default_print_depth} in order to
   see the complete list.
 
   The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
diff -r 638ed040e6f8 -r 2c34c69236ce ProgTutorial/Recipes/Antiquotes.thy
--- a/ProgTutorial/Recipes/Antiquotes.thy	Thu Apr 03 12:16:56 2014 +0100
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Sun Apr 06 12:45:54 2014 +0100
@@ -46,7 +46,7 @@
 let
   val srcpos = {delimited = false, text = (ml_val code_txt), pos = Position.none}
 in
-  (ML_Context.eval_source_in (SOME ctxt) false srcpos; 
+  (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos; 
    Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
 end
 
@@ -83,7 +83,7 @@
 let
   val srcpos = {delimited = false, pos = pos, text = ml_val code_txt}
 in
-  (ML_Context.eval_source_in (SOME ctxt) false srcpos;
+  (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos;
    Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
 end
 
@@ -143,7 +143,7 @@
   (let
      val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos}
    in
-     ML_Context.eval_source_in (SOME ctxt) false srcpos 
+     ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos 
    end;
    let 
      val code_output = space_explode "\n" code_txt 
diff -r 638ed040e6f8 -r 2c34c69236ce ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Thu Apr 03 12:16:56 2014 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Sun Apr 06 12:45:54 2014 +0100
@@ -33,7 +33,7 @@
 
 (* eval function *)
 fun eval_fn ctxt exp =
-  ML_Context.eval_source_in (SOME ctxt) false 
+  ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags 
     {delimited = false, text = exp, pos = Position.none}
 
 (* checks and prints a possibly open expressions, no index *)
diff -r 638ed040e6f8 -r 2c34c69236ce progtutorial.pdf
Binary file progtutorial.pdf has changed