--- a/ProgTutorial/antiquote_setup.ML Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML Thu Aug 20 22:30:20 2009 +0200
@@ -6,84 +6,84 @@
open OutputTutorial
(* functions for generating appropriate expressions *)
-fun ml_val_open ys istruct txt =
-let
- fun ml_val_open_aux ys txt =
- implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"];
-in
- (case istruct of
- NONE => ml_val_open_aux ys txt
- | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end"))
-end
+fun translate_string f str =
+ implode (map f (Symbol.explode str))
+
+fun prefix_lines prfx txt =
+ map (fn s => prfx ^ s) (split_lines txt)
-fun ml_val txt = ml_val_open [] NONE txt;
-fun ml_val_ind istruct txt = ml_val_open [] istruct txt;
+fun ml_with_vars ys txt =
+ implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]
+
+fun ml_with_struct (NONE) txt = txt
+ | ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"]
+
+fun ml_val vs stru txt =
+ txt |> ml_with_struct stru
+ |> ml_with_vars vs
fun ml_pat (lhs, pat) =
- let
- val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
- in "val " ^ pat' ^ " = " ^ lhs end;
+ implode ["val ", translate_string (fn "\<dots>" => "_" | s => s) pat, " = ", lhs]
-fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
-fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
+fun ml_struct txt =
+ implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"]
+
+fun ml_type txt =
+ implode ["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 prefix_str txt =
- map (fn s => prefix_str ^ s) (split_lines txt)
-
-val transform_cmts_str =
- Source.of_string
- #> ML_Lex.source
- #> Source.exhaust
- #> Chunks.transform_cmts
- #> implode
- #> string_explode ""
-
(* checks and prints a possibly open expressions, no index *)
-fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) =
- (eval_fn ctxt (ml_val_open ovars istruc txt); output (string_explode "" txt))
+fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
+ (eval_fn ctxt (ml_val vs stru txt);
+ output (split_lines txt))
val parser_ml = Scan.lift (Args.name --
(Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name)))
-(* checks and prinds a single entity, with index *)
-fun output_ml_ind {context = ctxt, ...} (txt, istruc) =
- (eval_fn ctxt (ml_val_ind istruc txt);
- case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt) of
- (NONE, bn, "") => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString}
- | (NONE, bn, qn) => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruct qn}
- | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruct st})
+(* checks and prints a single ML-item and produces an index entry *)
+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))
val parser_ml_ind = Scan.lift (Args.name --
Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name))
-(* checks and prints types and structures *)
-fun output_struct {context = ctxt, ...} txt =
- (eval_fn ctxt (ml_struct txt);
- output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "structure"})
+(* checks and prints structures *)
+fun gen_output_struct outfn {context = 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_type {context = ctxt, ...} txt =
- (eval_fn ctxt (ml_type txt);
- output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "type"})
+(* checks and prints types *)
+fun gen_output_type outfn {context = 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
(* checks and expression agains a result pattern *)
fun output_response {context = ctxt, ...} (lhs, pat) =
(eval_fn ctxt (ml_pat (lhs, pat));
- output ((string_explode "" lhs) @ (string_explode "> " pat)))
+ output ((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 lhs);
- output ((string_explode "" lhs) @ (string_explode "> " pat)))
+ (eval_fn ctxt (ml_val [] NONE lhs);
+ output ((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 ((string_explode "" lhs) @ (string_explode "> " pat))
+ output ((split_lines lhs) @ (prefix_lines "> " pat))
val single_arg = Scan.lift (Args.name)
val two_args = Scan.lift (Args.name -- Args.name)
@@ -91,7 +91,9 @@
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_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
@@ -101,14 +103,15 @@
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 "}")
+ implode [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 [href_link txt]
- else error ("Source file " ^ (quote txt) ^ " does not exist."))
+ else error (implode ["Source file ", quote txt, " does not exist."]))
+
val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
@@ -150,7 +153,6 @@
ThyOutput.output output
end
-
val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state