reorganized signature of ML_Context;
authorwenzelm
Fri Mar 28 00:02:54 2008 +0100 (2008-03-28)
changeset 264551757a6e049f4
parent 26454 57923fdab83b
child 26456 a63501938ce1
reorganized signature of ML_Context;
doc-src/antiquote_setup.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/codegen.ML
     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 -
    4.51 -fun use_mltext_update verbose pos txt context =
    4.52 -  #2 (pass_context context (fn () => eval_wrapper Output.ml_output verbose pos txt) ());
    4.53 +val eval = eval_wrapper Output.ml_output;
    4.54 +fun eval_file path = eval true (Position.path path) (File.read path);
    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