diff -r 8939b8fd8603 -r 069d525f8f1d CookBook/antiquote_setup.ML
--- a/CookBook/antiquote_setup.ML	Wed Mar 18 23:52:51 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-(* Auxiliary antiquotations for the tutorial. *)
-
-structure AntiquoteSetup: sig end =
-struct
-
-(* functions for generating appropriate expressions *)
-fun ml_val_open (ys, xs) txt = 
-  let fun ml_val_open_aux ys txt = 
-          "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
-  in
-    (case xs of
-       [] => ml_val_open_aux ys txt
-     | _  => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
-  end;
-
-fun ml_val txt = ml_val_open ([],[]) txt;
-
-fun ml_pat (lhs, pat) =
-  let 
-     val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
-  in "val " ^ pat' ^ " = " ^ lhs end;
-
-fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
-fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
-
-(* eval function *)
-fun eval_fn ctxt exp =
-  ML_Context.eval_in (SOME ctxt) false Position.none exp
-
-(* string functions *)
-fun string_explode str txt =
-  map (fn s => str ^ s) (space_explode "\n" txt)
-
-val transform_cmts_str =
-     Source.of_string 
-  #> ML_Lex.source 
-  #> Source.exhaust 
-  #> Chunks.transform_cmts 
-  #> implode 
-  #> string_explode "";
-
-(* output function *)
-fun output_fn txt =  Chunks.output (map Pretty.str txt)
-
-(* checks and prints open expressions *)
-fun output_ml {context = ctxt, ...} (txt, ovars) =
-  (eval_fn ctxt (ml_val_open ovars txt);
-   output_fn (transform_cmts_str txt))
-
-val parser_ml = Scan.lift (Args.name --
-  (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-   Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) 
-
-(* checks and prints types and structures *)
-fun output_exp ml {context = ctxt, ...} txt = 
-  (eval_fn ctxt (ml txt);
-   output_fn (string_explode "" txt))
-
-(* checks and expression agains a result pattern *)
-fun output_response {context = ctxt, ...} (lhs, pat) = 
-    (eval_fn ctxt (ml_pat (lhs, pat));
-     output_fn ((string_explode "" lhs) @ (string_explode "> " 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 lhs);
-     output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
-
-(* checks the expressions, but does not check it against a result pattern *)
-fun ouput_response_fake_both _ (lhs, pat) = 
-    output_fn ((string_explode "" lhs) @ (string_explode "> " pat))
-
-val single_arg = Scan.lift (Args.name)
-val two_args   = Scan.lift (Args.name -- Args.name)
-
-val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
-val _ = ThyOutput.antiquotation "ML_type" single_arg (output_exp ml_type)
-val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct)
-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
-
-fun href_link txt =
-let 
-  val raw = Symbol.encode_raw
-  val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    
-in
- (raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}")
-end 
-
-(* checks whether a file exists in the Isabelle distribution *)
-fun check_file_exists _ txt =
-  (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
-   then output_fn [href_link txt]
-   else error ("Source file " ^ (quote txt) ^ " does not exist."))
-
-val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
-
-
-(* replaces the official subgoal antiquotation with one *)
-(* that is closer to the actual output                  *)
-fun output_goals  {state = node, ...}  _ = 
-let
-  fun subgoals 0 = ""
-    | subgoals 1 = "goal (1 subgoal):"
-    | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
-
-  fun proof_state state =
-    (case try Toplevel.proof_of state of
-      SOME prf => prf
-    | _ => error "No proof state")
-
-  val state = proof_state node;
-  val goals = Proof.pretty_goals false state;
-
-  val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
-  val (As, B) = Logic.strip_horn prop;
-  val output  = (case (length As) of
-                      0 => goals 
-                    | n => (Pretty.str (subgoals n))::goals)  
-in 
-  ThyOutput.output output
-end
-
-
-val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
-   
-end;