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

6238

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

6310

21 
val pass: theory option > ('a > 'b) > 'a > 'b * theory option


22 
val pass_theory: theory > ('a > 'b) > 'a > 'b * theory

6238

23 
val save: ('a > 'b) > 'a > 'b

6185

24 
val >> : (theory > theory) > unit


25 
end;


26 


27 
structure Context: CONTEXT =


28 
struct


29 


30 


31 
(* theory context *)


32 


33 
local


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


35 
in


36 
fun get_context () = ! current_theory;


37 
fun set_context opt_thy = current_theory := opt_thy;

6238

38 
fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;

6185

39 
end;


40 


41 
fun the_context () =


42 
(case get_context () of


43 
Some thy => thy


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


45 


46 
fun context thy = set_context (Some thy);


47 
fun reset_context () = set_context None;


48 

6310

49 
fun pass opt_thy f x =

6261

50 
setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;


51 

6310

52 
fun pass_theory thy f x =


53 
(case pass (Some thy) f x of

6261

54 
(y, Some thy') => (y, thy')


55 
 (_, None) => error "Missing ML theory context");


56 

6238

57 
fun save f x = setmp (get_context ()) f x;


58 

6185

59 


60 
(* map context *)


61 


62 
nonfix >>;


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


64 


65 


66 
end;


67 


68 
structure BasicContext: BASIC_CONTEXT = Context;


69 
open BasicContext;
