# HG changeset patch
# User wenzelm
# Date 952373295 -3600
# Node ID ebbbfdb35c848eb84f887896a34f5c52a3118125
# Parent  8927067ef10755e926924997916fb8ff00a34c61
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);

diff -r 8927067ef107 -r ebbbfdb35c84 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Mar 06 15:44:51 2000 +0100
+++ b/src/Pure/context.ML	Mon Mar 06 21:08:15 2000 +0100
@@ -22,6 +22,10 @@
   val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
   val save: ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
+  val use_mltext: string -> bool -> theory option -> unit
+  val use_mltext_theory: string -> bool -> theory -> theory
+  val use_let: string -> string -> string -> theory -> theory
+  val use_setup: string -> theory -> theory
 end;
 
 structure Context: CONTEXT =
@@ -63,6 +67,20 @@
 fun >> f = set_context (Some (f (the_context ())));
 
 
+(* use ML text *)
+
+fun use_mltext txt verb opt_thy = setmp opt_thy (use_text writeln verb) txt;
+fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text writeln verb) txt);
+
+fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
+
+fun use_let name body txt =
+  use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
+
+val use_setup =
+  use_let "setup: (theory -> theory) list" "Library.apply setup";
+
+
 end;
 
 structure BasicContext: BASIC_CONTEXT = Context;