1.1 --- a/doc-src/antiquote_setup.ML Thu Mar 27 21:49:10 2008 +0100
1.2 +++ b/doc-src/antiquote_setup.ML Fri Mar 28 00:02:54 2008 +0100
1.3 @@ -36,7 +36,7 @@
1.4 else txt1 ^ ": " ^ txt2;
1.5 val txt' = if kind = "" then txt else kind ^ " " ^ txt;
1.6 val _ = writeln (ml (txt1, txt2));
1.7 - val _ = ML_Context.use_mltext false Position.none (ml (txt1, txt2)) (SOME (Context.Proof ctxt));
1.8 + val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
1.9 in
1.10 "\\indexml" ^ kind ^ enclose "{" "}"
1.11 (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^
2.1 --- a/src/Pure/Isar/isar_cmd.ML Thu Mar 27 21:49:10 2008 +0100
2.2 +++ b/src/Pure/Isar/isar_cmd.ML Fri Mar 28 00:02:54 2008 +0100
2.3 @@ -135,7 +135,7 @@
2.4 (* generic_setup *)
2.5
2.6 fun generic_setup (txt, pos) =
2.7 - ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt
2.8 + ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup" txt
2.9 |> Context.theory_map;
2.10
2.11
2.12 @@ -152,37 +152,42 @@
2.13 in
2.14
2.15 fun parse_ast_translation (a, (txt, pos)) =
2.16 - txt |> ML_Context.use_let pos ("val parse_ast_translation: (string * (" ^ advancedT a ^
2.17 + txt |> ML_Context.expression pos
2.18 + ("val parse_ast_translation: (string * (" ^ advancedT a ^
2.19 "Syntax.ast list -> Syntax.ast)) list")
2.20 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
2.21 |> Context.theory_map;
2.22
2.23 fun parse_translation (a, (txt, pos)) =
2.24 - txt |> ML_Context.use_let pos ("val parse_translation: (string * (" ^ advancedT a ^
2.25 + txt |> ML_Context.expression pos
2.26 + ("val parse_translation: (string * (" ^ advancedT a ^
2.27 "term list -> term)) list")
2.28 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
2.29 |> Context.theory_map;
2.30
2.31 fun print_translation (a, (txt, pos)) =
2.32 - txt |> ML_Context.use_let pos ("val print_translation: (string * (" ^ advancedT a ^
2.33 + txt |> ML_Context.expression pos
2.34 + ("val print_translation: (string * (" ^ advancedT a ^
2.35 "term list -> term)) list")
2.36 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
2.37 |> Context.theory_map;
2.38
2.39 fun print_ast_translation (a, (txt, pos)) =
2.40 - txt |> ML_Context.use_let pos ("val print_ast_translation: (string * (" ^ advancedT a ^
2.41 + txt |> ML_Context.expression pos
2.42 + ("val print_ast_translation: (string * (" ^ advancedT a ^
2.43 "Syntax.ast list -> Syntax.ast)) list")
2.44 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
2.45 |> Context.theory_map;
2.46
2.47 fun typed_print_translation (a, (txt, pos)) =
2.48 - txt |> ML_Context.use_let pos ("val typed_print_translation: (string * (" ^ advancedT a ^
2.49 + txt |> ML_Context.expression pos
2.50 + ("val typed_print_translation: (string * (" ^ advancedT a ^
2.51 "bool -> typ -> term list -> term)) list")
2.52 ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
2.53 |> Context.theory_map;
2.54
2.55 fun token_translation (txt, pos) =
2.56 - txt |> ML_Context.use_let pos
2.57 + txt |> ML_Context.expression pos
2.58 "val token_translation: (string * string * (string -> output * int)) list"
2.59 "Context.map_theory (Sign.add_tokentrfuns token_translation)"
2.60 |> Context.theory_map;
2.61 @@ -205,8 +210,7 @@
2.62 \in\n\
2.63 \ fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
2.64 \end;\n";
2.65 - in ML_Context.use_mltext_update false pos txt end
2.66 - |> Context.theory_map;
2.67 + in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false pos txt)) end;
2.68
2.69
2.70 (* axioms *)
2.71 @@ -233,7 +237,8 @@
2.72 (* declarations *)
2.73
2.74 fun declaration (txt, pos) =
2.75 - txt |> ML_Context.use_let pos "val declaration: Morphism.declaration"
2.76 + txt |> ML_Context.expression pos
2.77 + "val declaration: Morphism.declaration"
2.78 "Context.map_proof (LocalTheory.declaration declaration)"
2.79 |> Context.proof_map;
2.80
2.81 @@ -241,7 +246,7 @@
2.82 (* simprocs *)
2.83
2.84 fun simproc_setup name lhss (proc, pos) identifier =
2.85 - ML_Context.use_let pos
2.86 + ML_Context.expression pos
2.87 "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
2.88 ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
2.89 \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
2.90 @@ -382,12 +387,12 @@
2.91 Context.setmp_thread_data (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
2.92
2.93 (*passes changes of theory context*)
2.94 -fun use_mltext_theory (txt, pos) =
2.95 - Toplevel.theory' (fn int => Context.theory_map (ML_Context.use_mltext_update int pos txt));
2.96 +fun use_mltext_theory (txt, pos) = Toplevel.theory' (fn int =>
2.97 + Context.theory_map (ML_Context.exec (fn () => ML_Context.eval int pos txt)));
2.98
2.99 (*ignore result theory context*)
2.100 fun use_mltext verbose (txt, pos) = Toplevel.keep' (fn int => fn state =>
2.101 - (ML_Context.use_mltext (verbose andalso int) pos txt (try Toplevel.generic_theory_of state)));
2.102 + (ML_Context.eval_in (try Toplevel.generic_theory_of state) (verbose andalso int) pos txt));
2.103
2.104 val use_commit = Toplevel.imperative Secure.commit;
2.105
3.1 --- a/src/Pure/Isar/method.ML Thu Mar 27 21:49:10 2008 +0100
3.2 +++ b/src/Pure/Isar/method.ML Fri Mar 28 00:02:54 2008 +0100
3.3 @@ -354,9 +354,9 @@
3.4 fun set_tactic f = tactic_ref := f;
3.5
3.6 fun ml_tactic (txt, pos) ctxt = NAMED_CRITICAL "ML" (fn () =>
3.7 - (ML_Context.use_mltext false pos
3.8 + (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos
3.9 ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
3.10 - ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt));
3.11 + ^ txt ^ "\nin Method.set_tactic tactic end");
3.12 Context.setmp_thread_data (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
3.13
3.14 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
3.15 @@ -447,7 +447,7 @@
3.16 (* method_setup *)
3.17
3.18 fun method_setup name (txt, pos) cmt =
3.19 - ML_Context.use_let pos
3.20 + ML_Context.expression pos
3.21 "val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
3.22 "Context.map_theory (Method.add_method method)"
3.23 ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")
4.1 --- a/src/Pure/ML/ml_context.ML Thu Mar 27 21:49:10 2008 +0100
4.2 +++ b/src/Pure/ML/ml_context.ML Fri Mar 28 00:02:54 2008 +0100
4.3 @@ -21,7 +21,7 @@
4.4 val the_generic_context: unit -> Context.generic
4.5 val the_global_context: unit -> theory
4.6 val the_local_context: unit -> Proof.context
4.7 - val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic
4.8 + val exec: (unit -> unit) -> Context.generic -> Context.generic
4.9 val stored_thms: thm list ref
4.10 val ml_store_thm: string * thm -> unit
4.11 val ml_store_thms: string * thm list -> unit
4.12 @@ -34,12 +34,12 @@
4.13 (string * string * string) * (Context.generic * Args.T list)) -> unit
4.14 val eval_antiquotes_fn: (string * Position.T -> string * string) ref (* FIXME tmp *)
4.15 val trace: bool ref
4.16 - val use_mltext: bool -> Position.T -> string -> Context.generic option -> unit
4.17 - val use_mltext_update: bool -> Position.T -> string -> Context.generic -> Context.generic
4.18 - val use_let: Position.T -> string -> string -> string -> Context.generic -> Context.generic
4.19 - val use: Path.T -> unit
4.20 + val eval: bool -> Position.T -> string -> unit
4.21 + val eval_file: Path.T -> unit
4.22 + val eval_in: Context.generic option -> bool -> Position.T -> string -> unit
4.23 val evaluate: (string -> unit) * (string -> 'b) -> bool ->
4.24 string * (unit -> 'a) option ref -> string -> 'a
4.25 + val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
4.26 end
4.27
4.28 structure ML_Context: ML_CONTEXT =
4.29 @@ -51,10 +51,10 @@
4.30 val the_global_context = Context.theory_of o the_generic_context;
4.31 val the_local_context = Context.proof_of o the_generic_context;
4.32
4.33 -fun pass_context context f x =
4.34 - (case Context.setmp_thread_data (SOME context) (fn () => (f x, Context.thread_data ())) () of
4.35 - (y, SOME context') => (y, context')
4.36 - | (_, NONE) => error "Lost context after evaluation");
4.37 +fun exec (e: unit -> unit) context =
4.38 + (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
4.39 + SOME context' => context'
4.40 + | NONE => error "Missing context after execution");
4.41
4.42
4.43 (* theorem bindings *)
4.44 @@ -200,18 +200,11 @@
4.45
4.46 (* ML evaluation *)
4.47
4.48 -fun use_mltext verbose pos txt opt_context =
4.49 - Context.setmp_thread_data opt_context (fn () => eval_wrapper Output.ml_output verbose pos txt) ();
4.50 +val eval = eval_wrapper Output.ml_output;
4.51 +fun eval_file path = eval true (Position.path path) (File.read path);
4.52
4.53 -fun use_mltext_update verbose pos txt context =
4.54 - #2 (pass_context context (fn () => eval_wrapper Output.ml_output verbose pos txt) ());
4.55 -
4.56 -fun use_let pos bind body txt =
4.57 - use_mltext_update false pos
4.58 - ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
4.59 - " end (ML_Context.the_generic_context ())));");
4.60 -
4.61 -fun use path = eval_wrapper Output.ml_output true (Position.path path) (File.read path);
4.62 +fun eval_in context verbose pos txt =
4.63 + Context.setmp_thread_data context (fn () => eval verbose pos txt) ();
4.64
4.65 fun evaluate pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
4.66 let
4.67 @@ -220,6 +213,11 @@
4.68 ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
4.69 in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
4.70
4.71 +fun expression pos bind body txt =
4.72 + exec (fn () => eval false pos
4.73 + ("Context.set_thread_data (SOME (let " ^ bind ^ " = " ^ txt ^ " in " ^ body ^
4.74 + " end (ML_Context.the_generic_context ())));"));
4.75 +
4.76
4.77 (* basic antiquotations *)
4.78
5.1 --- a/src/Pure/Thy/thy_info.ML Thu Mar 27 21:49:10 2008 +0100
5.2 +++ b/src/Pure/Thy/thy_info.ML Fri Mar 28 00:02:54 2008 +0100
5.3 @@ -546,9 +546,8 @@
5.4 |> Present.begin_theory update_time dir uses;
5.5
5.6 val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
5.7 - val ((), theory'') =
5.8 - ML_Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
5.9 - ||> Context.the_theory;
5.10 + val theory'' =
5.11 + Context.theory_map (ML_Context.exec (fn () => List.app (load_file false) uses_now)) theory';
5.12 in theory'' end;
5.13
5.14 fun end_theory theory =
6.1 --- a/src/Pure/Thy/thy_load.ML Thu Mar 27 21:49:10 2008 +0100
6.2 +++ b/src/Pure/Thy/thy_load.ML Fri Mar 28 00:02:54 2008 +0100
6.3 @@ -119,7 +119,7 @@
6.4 fun load_ml dir raw_path =
6.5 (case check_ml dir raw_path of
6.6 NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
6.7 - | SOME (path, id) => (ML_Context.use path; (path, id)));
6.8 + | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
6.9
6.10 (*dependent on outer syntax*)
6.11 val load_thy_fn =
7.1 --- a/src/Pure/Thy/thy_output.ML Thu Mar 27 21:49:10 2008 +0100
7.2 +++ b/src/Pure/Thy/thy_output.ML Fri Mar 28 00:02:54 2008 +0100
7.3 @@ -502,7 +502,7 @@
7.4 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
7.5
7.6 fun output_ml ml src ctxt (txt, pos) =
7.7 - (ML_Context.use_mltext false pos (ml txt) (SOME (Context.Proof ctxt));
7.8 + (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
7.9 (if ! source then str_of_source src else txt)
7.10 |> (if ! quotes then quote else I)
7.11 |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
8.1 --- a/src/Pure/codegen.ML Thu Mar 27 21:49:10 2008 +0100
8.2 +++ b/src/Pure/codegen.ML Fri Mar 28 00:02:54 2008 +0100
8.3 @@ -963,7 +963,7 @@
8.4 [Pretty.str "]"])]]),
8.5 Pretty.str ");"]) ^
8.6 "\n\nend;\n") ();
8.7 - val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
8.8 + val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
8.9 fun iter f k = if k > i then NONE
8.10 else (case (f () handle Match =>
8.11 (if quiet then ()
8.12 @@ -1053,7 +1053,7 @@
8.13 [Pretty.str "(result ())"],
8.14 Pretty.str ");"]) ^
8.15 "\n\nend;\n";
8.16 - val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
8.17 + val _ = ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none s;
8.18 in !eval_result end) ();
8.19 in e () end;
8.20
8.21 @@ -1148,8 +1148,9 @@
8.22 val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
8.23 val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
8.24 in ((case opt_fname of
8.25 - NONE => ML_Context.use_mltext false Position.none (space_implode "\n" (map snd code))
8.26 - (SOME (Context.Theory thy))
8.27 + NONE =>
8.28 + ML_Context.eval_in (SOME (Context.Theory thy)) false Position.none
8.29 + (space_implode "\n" (map snd code))
8.30 | SOME fname =>
8.31 if lib then
8.32 app (fn (name, s) => File.write