author  wenzelm 
Tue, 16 Jan 2001 00:35:50 +0100  
changeset 10914  aded4ba99b88 
parent 10893  408906dd1e1b 
child 10924  92305ae9f460 
permissions  rwrr 
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 
10914  25 
val ml_output: (string > unit) * (string > unit) 
8348
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

26 
val use_mltext: string > bool > theory option > unit 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

27 
val use_mltext_theory: string > bool > theory > theory 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

28 
val use_let: string > string > string > theory > theory 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

29 
val use_setup: string > theory > theory 
6185  30 
end; 
31 

32 
structure Context: CONTEXT = 

33 
struct 

34 

35 

36 
(* theory context *) 

37 

38 
local 

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

40 
in 

41 
fun get_context () = ! current_theory; 

42 
fun set_context opt_thy = current_theory := opt_thy; 

6238  43 
fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x; 
6185  44 
end; 
45 

46 
fun the_context () = 

47 
(case get_context () of 

48 
Some thy => thy 

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

50 

51 
fun context thy = set_context (Some thy); 

52 
fun reset_context () = set_context None; 

53 

6310  54 
fun pass opt_thy f x = 
6261  55 
setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x; 
56 

6310  57 
fun pass_theory thy f x = 
58 
(case pass (Some thy) f x of 

6261  59 
(y, Some thy') => (y, thy') 
8801  60 
 (_, None) => error "Lost theory context in ML"); 
6261  61 

6238  62 
fun save f x = setmp (get_context ()) f x; 
63 

6185  64 

65 
(* map context *) 

66 

67 
nonfix >>; 

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

69 

70 

8348
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

71 
(* use ML text *) 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

72 

10914  73 
val ml_output = (writeln, error_msg: string > unit); 
74 

75 
fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_text ml_output verb txt) (); 

76 
fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text ml_output verb) txt); 

8348
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

77 

ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

78 
fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false; 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

79 

9586  80 
fun use_let bind body txt = 
81 
use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); 

8348
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

82 

ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

83 
val use_setup = 
9586  84 
use_let "val setup: (theory > theory) list" "Library.apply setup"; 
8348
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

85 

ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

86 

6185  87 
end; 
88 

89 
structure BasicContext: BASIC_CONTEXT = Context; 

90 
open BasicContext; 