author  wenzelm 
Mon, 06 Mar 2000 21:08:15 +0100  
changeset 8348  ebbbfdb35c84 
parent 6310  353a8a9d9d2c 
child 8801  9d01c9a26134 
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 
8348
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

25 
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

26 
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

27 
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

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

31 
structure Context: CONTEXT = 

32 
struct 

33 

34 

35 
(* theory context *) 

36 

37 
local 

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

39 
in 

40 
fun get_context () = ! current_theory; 

41 
fun set_context opt_thy = current_theory := opt_thy; 

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

45 
fun the_context () = 

46 
(case get_context () of 

47 
Some thy => thy 

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

49 

50 
fun context thy = set_context (Some thy); 

51 
fun reset_context () = set_context None; 

52 

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

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

6261  58 
(y, Some thy') => (y, thy') 
59 
 (_, None) => error "Missing ML theory context"); 

60 

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

6185  63 

64 
(* map context *) 

65 

66 
nonfix >>; 

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

68 

69 

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

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

71 

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

72 
fun use_mltext txt verb opt_thy = setmp opt_thy (use_text writeln verb) txt; 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

73 
fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_text writeln verb) txt); 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

74 

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

75 
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

76 

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

77 
fun use_let name body txt = 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

78 
use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); 
ebbbfdb35c84
added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents:
6310
diff
changeset

79 

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

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

81 
use_let "setup: (theory > theory) list" "Library.apply setup"; 
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 

6185  84 
end; 
85 

86 
structure BasicContext: BASIC_CONTEXT = Context; 

87 
open BasicContext; 