--- a/ProgTutorial/Base.thy	Wed Jun 02 10:08:16 2010 +0200
+++ b/ProgTutorial/Base.thy	Tue Jun 08 15:18:30 2010 +0200
@@ -104,20 +104,23 @@
       (fn (txt, pos) =>
         Toplevel.generic_theory
          (ML_Context.exec 
-           (fn () => ML_Context.eval true pos txt) 
+           (fn () => ML_Context.eval_text true pos txt) 
               #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))
-
+*}
+ML {*
 val _ =
   Outer_Syntax.command "ML_prf" "ML text within proof" 
     (Keyword.tag "TutorialML" Keyword.prf_decl)
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))
+        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)))
+*}
 
+ML {*
 val _ =
   Outer_Syntax.command "ML_val" "diagnostic ML text" 
   (Keyword.tag "TutorialML" Keyword.diag)
-    (Parse.ML_source >> IsarCmd.ml_diag true)
+    (Parse.ML_source >> Isar_Cmd.ml_diag true)
 *}
 
 ML {*
@@ -125,7 +128,7 @@
   Outer_Syntax.command "setup" "ML theory setup" 
     (Keyword.tag_ml Keyword.thy_decl)
       (Parse.ML_source >> (fn (txt, pos) => 
-        (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
+        (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
 *}
 
 ML {*
@@ -133,7 +136,7 @@
   Outer_Syntax.local_theory "local_setup" "ML local theory setup" 
     (Keyword.tag_ml Keyword.thy_decl)
       (Parse.ML_source >> (fn (txt, pos) => 
-         IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
+         Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
 *}
 
 ML {*

--- a/ProgTutorial/Recipes/Antiquotes.thy	Wed Jun 02 10:08:16 2010 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Tue Jun 08 15:18:30 2010 +0200
@@ -35,7 +35,7 @@
 
   The code is checked by sending the ML-expression @{text [quotes] "val _ =
   a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML
-  "ML_Context.eval_in"} in Line 4 below). The complete code of the
+  "ML_Context.eval_text_in"} in Line 4 below). The complete code of the
   document antiquotation is as follows:
 
 *}
@@ -43,10 +43,10 @@
 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
 
 fun output_ml {context = ctxt, ...} code_txt =
-  (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
-   ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
+  (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); 
+   Thy_Output.output (map Pretty.str (space_explode "\n" code_txt)))
 
-val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
+val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
 
 text {*
   The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this
@@ -55,13 +55,13 @@
   function @{ML ml_val}, which constructs the appropriate ML-expression, and
   using @{ML "eval_in" in ML_Context}, which calls the compiler.  If the code is
   ``approved'' by the compiler, then the output function @{ML "output" in
-  ThyOutput} in the next line pretty prints the code. This function expects
+  Thy_Output} in the next line pretty prints the code. This function expects
   that the code is a list of (pretty)strings where each string correspond to a
   line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"
   for txt} which produces such a list according to linebreaks.  There are a
   number of options for antiquotations that are observed by the function 
-  @{ML "output" in ThyOutput} when printing the code (including @{text "[display]"} 
-  and @{text "[quotes]"}). The function @{ML "antiquotation" in ThyOutput} in 
+  @{ML "output" in Thy_Output} when printing the code (including @{text "[display]"} 
+  and @{text "[quotes]"}). The function @{ML "antiquotation" in Thy_Output} in 
   Line 7 sets up the new document antiquotation.
 
   \begin{readmore}
@@ -74,10 +74,10 @@
 *}
 
 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =
-  (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
-   ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
+  (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt);
+   Thy_Output.output (map Pretty.str (space_explode "\n" code_txt)))
 
-val _ = ThyOutput.antiquotation "ML_checked"
+val _ = Thy_Output.antiquotation "ML_checked"
          (Scan.lift (Parse.position Args.name)) output_ml *}
 
 text {*
@@ -128,15 +128,15 @@
 *}
 
 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = 
-  (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt, pat));
+  (ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat));
    let 
      val code_output = space_explode "\n" code_txt 
      val resp_output = add_resp (space_explode "\n" pat)
    in 
-     ThyOutput.output (map Pretty.str (code_output @ resp_output)) 
+     Thy_Output.output (map Pretty.str (code_output @ resp_output)) 
    end)
 
-val _ = ThyOutput.antiquotation "ML_resp" 
+val _ = Thy_Output.antiquotation "ML_resp" 
           (Scan.lift (Parse.position (Args.name -- Args.name))) 
              output_ml_resp*}
 

--- a/ProgTutorial/antiquote_setup.ML	Wed Jun 02 10:08:16 2010 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue Jun 08 15:18:30 2010 +0200
@@ -33,7 +33,7 @@
 
 (* eval function *)
 fun eval_fn ctxt exp =
-  ML_Context.eval_in (SOME ctxt) false Position.none exp
+  ML_Context.eval_text_in (SOME ctxt) false Position.none exp
 
 (* checks and prints a possibly open expressions, no index *)
 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
@@ -98,17 +98,17 @@
 val two_args   = Scan.lift (Args.name -- Args.name)
 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
-val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
-val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind
-val _ = ThyOutput.antiquotation "ML_type" single_arg output_type
-val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind
-val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
-val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind
-val _ = ThyOutput.antiquotation "ML_funct" single_arg output_funct
-val _ = ThyOutput.antiquotation "ML_funct_ind" single_arg output_funct_ind
-val _ = ThyOutput.antiquotation "ML_response" two_args output_response
-val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
-val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
+val _ = Thy_Output.antiquotation "ML" parser_ml output_ml
+val _ = Thy_Output.antiquotation "ML_ind" parser_ml_ind output_ml_ind
+val _ = Thy_Output.antiquotation "ML_type" single_arg output_type
+val _ = Thy_Output.antiquotation "ML_type_ind" single_arg output_type_ind
+val _ = Thy_Output.antiquotation "ML_struct" single_arg output_struct
+val _ = Thy_Output.antiquotation "ML_struct_ind" single_arg output_struct_ind
+val _ = Thy_Output.antiquotation "ML_funct" single_arg output_funct
+val _ = Thy_Output.antiquotation "ML_funct_ind" single_arg output_funct_ind
+val _ = Thy_Output.antiquotation "ML_response" two_args output_response
+val _ = Thy_Output.antiquotation "ML_response_fake" two_args output_response_fake
+val _ = Thy_Output.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
 
 (* FIXME: experimental *)
 fun ml_eq (lhs, pat, eq) =
@@ -120,7 +120,7 @@
      | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
      output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
-val _ = ThyOutput.antiquotation "ML_response_eq" test output_response_eq
+val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq
 
 (* checks whether a file exists in the Isabelle distribution *)
 fun href_link txt =
@@ -136,7 +136,7 @@
    then output [href_link txt]
    else error (implode ["Source file ", quote txt, " does not exist."]))
 
-val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
+val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists
 
 
 (* replaces the official subgoal antiquotation with one *)
@@ -161,7 +161,7 @@
                       0 => [goals] 
                     | n => [Pretty.str (subgoals n), goals])  
 in 
-  ThyOutput.output output
+  Thy_Output.output output
 end
 
 fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
@@ -173,10 +173,10 @@
   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 
-  ThyOutput.output output
+  Thy_Output.output output
 end
 
-val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
-val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
+val _ = Thy_Output.antiquotation "subgoals" (Scan.succeed ()) output_goals
+val _ = Thy_Output.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
 
 end;

--- a/ProgTutorial/output_tutorial.ML	Wed Jun 02 10:08:16 2010 +0200
+++ b/ProgTutorial/output_tutorial.ML	Tue Jun 08 15:18:30 2010 +0200
@@ -2,7 +2,7 @@
 structure OutputTutorial =
 struct
 
-(* rebuilding the output function from ThyOutput in order to *)
+(* rebuilding the output function from Thy_Output in order to *)
 (* enable the options [gray, linenos]                        *)
 
 val gray = Unsynchronized.ref false
@@ -14,15 +14,15 @@
   val prts = map Pretty.str txt
 in   
   prts
-  |> (if ! ThyOutput.quotes then map Pretty.quote else I)
-  |> (if ! ThyOutput.display then
-    map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
+  |> (if ! Thy_Output.quotes then map Pretty.quote else I)
+  |> (if ! Thy_Output.display then
+    map (Output.output o Pretty.string_of o Pretty.indent (! Thy_Output.indent))
     #> space_implode "\\isasep\\isanewline%\n"
     #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
     #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   else
-    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
+    map (Output.output o (if ! Thy_Output.break then Pretty.string_of else Pretty.str_of))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}")
 end
@@ -84,7 +84,7 @@
   | boolean "false" = false
   | boolean s = error ("Bad boolean value: " ^ quote s);
 
-val _ = ThyOutput.add_options
+val _ = Thy_Output.add_options
  [("gray", Library.setmp_CRITICAL gray o boolean),
   ("linenos", Library.setmp_CRITICAL linenos o boolean)]
 

Binary file progtutorial.pdf has changed