diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Sun Aug 22 22:56:52 2010 +0800
+++ b/ProgTutorial/antiquote_setup.ML	Sat Aug 28 13:27:16 2010 +0800
@@ -38,7 +38,7 @@
 (* checks and prints a possibly open expressions, no index *)
 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
   (eval_fn ctxt (ml_val vs stru txt); 
-   output (split_lines txt))
+   output ctxt (split_lines txt))
 
 val parser_ml = Scan.lift (Args.name --
   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
@@ -48,51 +48,51 @@
 fun output_ml_ind {context = ctxt, ...} (txt, stru) =
   (eval_fn ctxt (ml_val [] stru txt); 
    case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
-     (NONE, bn, "")  => output_indexed {main = Code txt, minor = NoString} (split_lines txt)
-   | (NONE, bn, qn)  => output_indexed {main = Code bn,  minor = Struct qn} (split_lines txt)
-   | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt))
+     (NONE, bn, "")  => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt)
+   | (NONE, bn, qn)  => output_indexed ctxt {main = Code bn,  minor = Struct qn} (split_lines txt)
+   | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt))
 
 val parser_ml_ind = Scan.lift (Args.name --
   Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))
 
 (* checks and prints structures *)
-fun gen_output_struct outfn {context = ctxt, ...} txt = 
+fun gen_output_struct outfn ctxt txt = 
   (eval_fn ctxt (ml_struct txt); 
    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
 
-val output_struct = gen_output_struct (K output)
-val output_struct_ind = gen_output_struct output_indexed
+fun output_struct {context = ctxt, ...} = gen_output_struct (K (output ctxt)) ctxt 
+fun output_struct_ind {context = ctxt, ...} = gen_output_struct (output_indexed ctxt) ctxt 
 
 (* prints functors; no checks *)
-fun gen_output_funct outfn {context = ctxt, ...} txt = 
+fun gen_output_funct outfn txt = 
   (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
 
-val output_funct = gen_output_funct (K output)
-val output_funct_ind = gen_output_funct output_indexed
+fun output_funct {context = ctxt, ...} = gen_output_funct (K (output ctxt)) 
+fun output_funct_ind {context = ctxt, ...} = gen_output_funct (output_indexed ctxt)
 
 (* checks and prints types *)
-fun gen_output_type outfn {context = ctxt, ...} txt = 
+fun gen_output_type outfn ctxt txt = 
   (eval_fn ctxt (ml_type txt); 
    outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
 
-val output_type = gen_output_type (K output)
-val output_type_ind = gen_output_type output_indexed
+fun output_type {context = ctxt, ...} = gen_output_type (K (output ctxt)) ctxt
+fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt 
 
 (* checks and expression agains a result pattern *)
 fun output_response {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_pat (lhs, pat));
      write_file_ml_blk lhs (ProofContext.theory_of ctxt);
-     output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
+     output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE lhs);
      write_file_ml_blk lhs (ProofContext.theory_of ctxt);
-     output ((split_lines lhs) @ (prefix_lines "> " pat)))
+     output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
-fun ouput_response_fake_both _ (lhs, pat) = 
-    output ((split_lines lhs) @ (prefix_lines "> " pat))
+fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = 
+    output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))
 
 val single_arg = Scan.lift (Args.name)
 val two_args   = Scan.lift (Args.name -- Args.name)
@@ -118,7 +118,7 @@
     (case eq of 
        NONE => eval_fn ctxt (ml_pat (lhs, pat))
      | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
-     output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
+     output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
 val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq
 
@@ -131,9 +131,9 @@
  implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
 end 
 
-fun check_file_exists _ txt =
+fun check_file_exists {context = ctxt, ...} txt =
   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
-   then output [href_link txt]
+   then output ctxt [href_link txt]
    else error (implode ["Source file ", quote txt, " does not exist."]))
 
 val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists
@@ -146,7 +146,7 @@
       SOME prf => prf
     | _ => error "No proof state")
 
-fun output_goals  {state = node, ...}  _ = 
+fun output_goals  {state = node, context = ctxt, ...} _ = 
 let
   fun subgoals 0 = ""
     | subgoals 1 = "goal (1 subgoal):"
@@ -161,7 +161,7 @@
                       0 => [goals] 
                     | n => [Pretty.str (subgoals n), goals])  
 in 
-  Thy_Output.output output
+  Thy_Output.output ctxt output
 end
 
 fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
@@ -173,7 +173,7 @@
   val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))
   val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))
 in 
-  Thy_Output.output output
+  Thy_Output.output ctxt output
 end
 
 val _ = Thy_Output.antiquotation "subgoals" (Scan.succeed ()) output_goals