author  skalberg 
Sun, 13 Feb 2005 17:15:14 +0100  
changeset 15531  08c8dad8e399 
parent 14981  e73f8140af78 
child 15801  d2f5ca3c048d 
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 

15531  39 
val current_theory = ref (NONE: theory option); 
6185  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 

15531  48 
SOME thy => thy 
6185  49 
 _ => error "Unknown theory context"); 
50 

15531  51 
fun context thy = set_context (SOME thy); 
52 
fun reset_context () = set_context NONE; 

6185  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 = 
15531  58 
(case pass (SOME thy) f x of 
59 
(y, SOME thy') => (y, thy') 

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 >>; 

15531  68 
fun >> f = set_context (SOME (f (the_context ()))); 
6185  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); 
14976  74 

75 
fun use_output verb txt = use_text ml_output verb (Symbol.escape txt); 

10914  76 

10924
92305ae9f460
use_output: proper handling of nonASCII symbols;
wenzelm
parents:
10914
diff
changeset

77 
fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) (); 
92305ae9f460
use_output: proper handling of nonASCII symbols;
wenzelm
parents:
10914
diff
changeset

78 
fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt); 
8348
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 
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

81 

9586  82 
fun use_let bind body txt = 
83 
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

84 

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

85 
val use_setup = 
9586  86 
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

87 

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

88 

6185  89 
end; 
90 

91 
structure BasicContext: BASIC_CONTEXT = Context; 

92 
open BasicContext; 