src/Pure/context.ML
author wenzelm
Thu, 21 Apr 2005 22:02:06 +0200
changeset 15801 d2f5ca3c048d
parent 15531 08c8dad8e399
child 16436 7eb6b6cbd166
permissions -rw-r--r--
superceded by Pure.thy and CPure.thy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/context.ML
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     4
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
     5
Theory contexts.
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     6
*)
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     7
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     8
signature BASIC_CONTEXT =
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
     9
sig
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    10
  val context: theory -> unit
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    11
  val the_context: unit -> theory
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    12
end;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    13
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    14
signature CONTEXT =
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    15
sig
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    16
  include BASIC_CONTEXT
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    17
  val get_context: unit -> theory option
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    18
  val set_context: theory option -> unit
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    19
  val reset_context: unit -> unit
6238
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    20
  val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
6310
wenzelm
parents: 6261
diff changeset
    21
  val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
wenzelm
parents: 6261
diff changeset
    22
  val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
6238
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    23
  val save: ('a -> 'b) -> 'a -> 'b
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    24
  val >> : (theory -> theory) -> unit
10914
aded4ba99b88 use_text etc.: proper output of error messages;
wenzelm
parents: 10893
diff changeset
    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
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    29
  val add_setup: (theory -> theory) list -> unit
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    30
  val setup: unit -> (theory -> theory) list
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    31
end;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    32
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    33
structure Context: CONTEXT =
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    34
struct
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    35
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    36
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    37
(** implicit theory context in ML **)
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    38
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    39
local
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    40
  val current_theory = ref (NONE: theory option);
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    41
in
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    42
  fun get_context () = ! current_theory;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    43
  fun set_context opt_thy = current_theory := opt_thy;
6238
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    44
  fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    45
end;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    46
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    47
fun the_context () =
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    48
  (case get_context () of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    49
    SOME thy => thy
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    50
  | _ => error "Unknown theory context");
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    51
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    52
fun context thy = set_context (SOME thy);
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    53
fun reset_context () = set_context NONE;
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    54
6310
wenzelm
parents: 6261
diff changeset
    55
fun pass opt_thy f x =
6261
6dc692fb3d28 added fetch, fetch_theory;
wenzelm
parents: 6238
diff changeset
    56
  setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
6dc692fb3d28 added fetch, fetch_theory;
wenzelm
parents: 6238
diff changeset
    57
6310
wenzelm
parents: 6261
diff changeset
    58
fun pass_theory thy f x =
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    59
  (case pass (SOME thy) f x of
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    60
    (y, SOME thy') => (y, thy')
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    61
  | (_, NONE) => error "Lost theory context in ML");
6261
6dc692fb3d28 added fetch, fetch_theory;
wenzelm
parents: 6238
diff changeset
    62
6238
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    63
fun save f x = setmp (get_context ()) f x;
bd7b4a23118f setmp: theory option;
wenzelm
parents: 6185
diff changeset
    64
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    65
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    66
(* map context *)
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    67
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    68
nonfix >>;
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    69
fun >> f = set_context (SOME (f (the_context ())));
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    70
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    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
aded4ba99b88 use_text etc.: proper output of error messages;
wenzelm
parents: 10893
diff changeset
    74
val ml_output = (writeln, error_msg: string -> unit);
14976
65f572245276 use_output: Symbol.escape;
wenzelm
parents: 11819
diff changeset
    75
65f572245276 use_output: Symbol.escape;
wenzelm
parents: 11819
diff changeset
    76
fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
10914
aded4ba99b88 use_text etc.: proper output of error messages;
wenzelm
parents: 10893
diff changeset
    77
10924
92305ae9f460 use_output: proper handling of non-ASCII 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 non-ASCII 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
f6669dead969 use_let: exclude 'val';
wenzelm
parents: 8801
diff changeset
    83
fun use_let bind body txt =
f6669dead969 use_let: exclude 'val';
wenzelm
parents: 8801
diff changeset
    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
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    86
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    87
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    88
(** delayed theory setup **)
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    89
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    90
local
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    91
  val setup_fns = ref ([]: (theory -> theory) list);
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    92
in
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    93
  fun add_setup fns = setup_fns := ! setup_fns @ fns;
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    94
  fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end;
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15531
diff changeset
    95
end;
8348
ebbbfdb35c84 added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents: 6310
diff changeset
    96
ebbbfdb35c84 added use_mltext, use_mltext_theory, use_let, use_setup (from isar_thy.ML);
wenzelm
parents: 6310
diff changeset
    97
6185
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    98
end;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
    99
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
   100
structure BasicContext: BASIC_CONTEXT = Context;
11bf7a8b6a02 Global theory context (used to be in Thy/context.ML);
wenzelm
parents:
diff changeset
   101
open BasicContext;