author  wenzelm 
Sun, 20 Jun 2004 09:27:24 +0200  
changeset 14976  65f572245276 
parent 11819  9283b3c11234 
child 14981  e73f8140af78 
permissions  rwrr 
6185  1 
(* Title: Pure/context.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

11819  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
6185  5 

6 
Global theory context. 

7 
*) 

8 

9 
signature BASIC_CONTEXT = 

10 
sig 

11 
val context: theory > unit 

12 
val the_context: unit > theory 

13 
end; 

14 

15 
signature CONTEXT = 

16 
sig 

17 
include BASIC_CONTEXT 

18 
val get_context: unit > theory option 

19 
val set_context: theory option > unit 

20 
val reset_context: unit > unit 

6238  21 
val setmp: theory option > ('a > 'b) > 'a > 'b 
6310  22 
val pass: theory option > ('a > 'b) > 'a > 'b * theory option 
23 
val pass_theory: theory > ('a > 'b) > 'a > 'b * theory 

6238  24 
val save: ('a > 'b) > 'a > 'b 
6185  25 
val >> : (theory > theory) > unit 
10914  26 
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

27 
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

28 
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

29 
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

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

33 
structure Context: CONTEXT = 

34 
struct 

35 

36 

37 
(* theory context *) 

38 

39 
local 

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

41 
in 

42 
fun get_context () = ! current_theory; 

43 
fun set_context opt_thy = current_theory := opt_thy; 

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

47 
fun the_context () = 

48 
(case get_context () of 

49 
Some thy => thy 

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

51 

52 
fun context thy = set_context (Some thy); 

53 
fun reset_context () = set_context None; 

54 

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

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

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

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

6185  65 

66 
(* map context *) 

67 

68 
nonfix >>; 

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

70 

71 

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

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

73 

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

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

10914  77 

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

78 
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

79 
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

80 

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

81 
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

82 

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

85 

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

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

88 

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

89 

6185  90 
end; 
91 

92 
structure BasicContext: BASIC_CONTEXT = Context; 

93 
open BasicContext; 