6185

1 
(* Title: Pure/context.ML


2 
ID: $Id$


3 
Author: Markus Wenzel, TU Muenchen


4 


5 
Global theory context.


6 
*)


7 


8 
signature BASIC_CONTEXT =


9 
sig


10 
val context: theory > unit


11 
val the_context: unit > theory


12 
end;


13 


14 
signature CONTEXT =


15 
sig


16 
include BASIC_CONTEXT


17 
val get_context: unit > theory option


18 
val set_context: theory option > unit


19 
val reset_context: unit > unit


20 
val setmp: theory > ('a > 'b) > 'a > 'b


21 
val >> : (theory > theory) > unit


22 
end;


23 


24 
structure Context: CONTEXT =


25 
struct


26 


27 


28 
(* theory context *)


29 


30 
local


31 
val current_theory = ref (None: theory option);


32 
in


33 
fun get_context () = ! current_theory;


34 
fun set_context opt_thy = current_theory := opt_thy;


35 
fun setmp thy f x = Library.setmp current_theory (Some thy) f x;


36 
end;


37 


38 
fun the_context () =


39 
(case get_context () of


40 
Some thy => thy


41 
 _ => error "Unknown theory context");


42 


43 
fun context thy = set_context (Some thy);


44 
fun reset_context () = set_context None;


45 


46 


47 
(* map context *)


48 


49 
nonfix >>;


50 
fun >> f = set_context (Some (f (the_context ())));


51 


52 


53 
end;


54 


55 
structure BasicContext: BASIC_CONTEXT = Context;


56 
open BasicContext;
