src/Pure/context.ML
author wenzelm
Thu Apr 21 22:02:06 2005 +0200 (2005-04-21)
changeset 15801 d2f5ca3c048d
parent 15531 08c8dad8e399
child 16436 7eb6b6cbd166
permissions -rw-r--r--
superceded by Pure.thy and CPure.thy;
wenzelm@6185
     1
(*  Title:      Pure/context.ML
wenzelm@6185
     2
    ID:         $Id$
wenzelm@6185
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6185
     4
wenzelm@15801
     5
Theory contexts.
wenzelm@6185
     6
*)
wenzelm@6185
     7
wenzelm@6185
     8
signature BASIC_CONTEXT =
wenzelm@6185
     9
sig
wenzelm@6185
    10
  val context: theory -> unit
wenzelm@6185
    11
  val the_context: unit -> theory
wenzelm@6185
    12
end;
wenzelm@6185
    13
wenzelm@6185
    14
signature CONTEXT =
wenzelm@6185
    15
sig
wenzelm@6185
    16
  include BASIC_CONTEXT
wenzelm@6185
    17
  val get_context: unit -> theory option
wenzelm@6185
    18
  val set_context: theory option -> unit
wenzelm@6185
    19
  val reset_context: unit -> unit
wenzelm@6238
    20
  val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
wenzelm@6310
    21
  val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
wenzelm@6310
    22
  val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
wenzelm@6238
    23
  val save: ('a -> 'b) -> 'a -> 'b
wenzelm@6185
    24
  val >> : (theory -> theory) -> unit
wenzelm@10914
    25
  val ml_output: (string -> unit) * (string -> unit)
wenzelm@8348
    26
  val use_mltext: string -> bool -> theory option -> unit
wenzelm@8348
    27
  val use_mltext_theory: string -> bool -> theory -> theory
wenzelm@8348
    28
  val use_let: string -> string -> string -> theory -> theory
wenzelm@15801
    29
  val add_setup: (theory -> theory) list -> unit
wenzelm@15801
    30
  val setup: unit -> (theory -> theory) list
wenzelm@6185
    31
end;
wenzelm@6185
    32
wenzelm@6185
    33
structure Context: CONTEXT =
wenzelm@6185
    34
struct
wenzelm@6185
    35
wenzelm@6185
    36
wenzelm@15801
    37
(** implicit theory context in ML **)
wenzelm@6185
    38
wenzelm@6185
    39
local
skalberg@15531
    40
  val current_theory = ref (NONE: theory option);
wenzelm@6185
    41
in
wenzelm@6185
    42
  fun get_context () = ! current_theory;
wenzelm@6185
    43
  fun set_context opt_thy = current_theory := opt_thy;
wenzelm@6238
    44
  fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
wenzelm@6185
    45
end;
wenzelm@6185
    46
wenzelm@6185
    47
fun the_context () =
wenzelm@6185
    48
  (case get_context () of
skalberg@15531
    49
    SOME thy => thy
wenzelm@6185
    50
  | _ => error "Unknown theory context");
wenzelm@6185
    51
skalberg@15531
    52
fun context thy = set_context (SOME thy);
skalberg@15531
    53
fun reset_context () = set_context NONE;
wenzelm@6185
    54
wenzelm@6310
    55
fun pass opt_thy f x =
wenzelm@6261
    56
  setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
wenzelm@6261
    57
wenzelm@6310
    58
fun pass_theory thy f x =
skalberg@15531
    59
  (case pass (SOME thy) f x of
skalberg@15531
    60
    (y, SOME thy') => (y, thy')
skalberg@15531
    61
  | (_, NONE) => error "Lost theory context in ML");
wenzelm@6261
    62
wenzelm@6238
    63
fun save f x = setmp (get_context ()) f x;
wenzelm@6238
    64
wenzelm@6185
    65
wenzelm@6185
    66
(* map context *)
wenzelm@6185
    67
wenzelm@6185
    68
nonfix >>;
skalberg@15531
    69
fun >> f = set_context (SOME (f (the_context ())));
wenzelm@6185
    70
wenzelm@6185
    71
wenzelm@8348
    72
(* use ML text *)
wenzelm@8348
    73
wenzelm@10914
    74
val ml_output = (writeln, error_msg: string -> unit);
wenzelm@14976
    75
wenzelm@14976
    76
fun use_output verb txt = use_text ml_output verb (Symbol.escape txt);
wenzelm@10914
    77
wenzelm@10924
    78
fun use_mltext txt verb opt_thy = setmp opt_thy (fn () => use_output verb txt) ();
wenzelm@10924
    79
fun use_mltext_theory txt verb thy = #2 (pass_theory thy (use_output verb) txt);
wenzelm@8348
    80
wenzelm@8348
    81
fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
wenzelm@8348
    82
wenzelm@9586
    83
fun use_let bind body txt =
wenzelm@9586
    84
  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
wenzelm@8348
    85
wenzelm@15801
    86
wenzelm@15801
    87
wenzelm@15801
    88
(** delayed theory setup **)
wenzelm@15801
    89
wenzelm@15801
    90
local
wenzelm@15801
    91
  val setup_fns = ref ([]: (theory -> theory) list);
wenzelm@15801
    92
in
wenzelm@15801
    93
  fun add_setup fns = setup_fns := ! setup_fns @ fns;
wenzelm@15801
    94
  fun setup () = let val fns = ! setup_fns in setup_fns := []; fns end;
wenzelm@15801
    95
end;
wenzelm@8348
    96
wenzelm@8348
    97
wenzelm@6185
    98
end;
wenzelm@6185
    99
wenzelm@6185
   100
structure BasicContext: BASIC_CONTEXT = Context;
wenzelm@6185
   101
open BasicContext;