src/Pure/Thy/context.ML
author wenzelm
Sat Jun 20 20:18:51 1998 +0200 (1998-06-20)
changeset 5059 dcdb21e53537
parent 5049 bde086cfa597
child 5249 9d7e6f7110ef
permissions -rw-r--r--
renamed Thm(s) back to thm(s);
wenzelm@4338
     1
(*  Title:      Pure/Thy/context.ML
wenzelm@4338
     2
    ID:         $Id$
wenzelm@4338
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@4338
     4
wenzelm@4338
     5
Global contexts: session and theory.
wenzelm@4338
     6
*)
wenzelm@4338
     7
wenzelm@4486
     8
signature BASIC_CONTEXT =
wenzelm@4338
     9
sig
wenzelm@4338
    10
  val context: theory -> unit
wenzelm@5049
    11
  val the_context: unit -> theory
wenzelm@5059
    12
  val thm: xstring -> thm
wenzelm@5059
    13
  val thms: xstring -> thm list
wenzelm@4914
    14
  val Goal: string -> thm list
wenzelm@4914
    15
  val Goalw: thm list -> string -> thm list
wenzelm@4338
    16
end;
wenzelm@4338
    17
wenzelm@4486
    18
signature CONTEXT =
wenzelm@4486
    19
sig
wenzelm@4486
    20
  include BASIC_CONTEXT
wenzelm@5031
    21
  val get_session: unit -> string list
wenzelm@5031
    22
  val add_session: string -> unit
wenzelm@5031
    23
  val reset_session: unit -> unit
wenzelm@4925
    24
  val welcome: unit -> string
wenzelm@5031
    25
  val get_context: unit -> theory option
wenzelm@5031
    26
  val set_context: theory option -> unit
wenzelm@5031
    27
  val reset_context: unit -> unit
wenzelm@4486
    28
  val >> : (theory -> theory) -> unit
wenzelm@4486
    29
end;
wenzelm@4486
    30
wenzelm@4338
    31
structure Context: CONTEXT =
wenzelm@4338
    32
struct
wenzelm@4338
    33
wenzelm@4338
    34
wenzelm@4843
    35
(** session **)
wenzelm@4338
    36
wenzelm@4338
    37
val current_session = ref ([]: string list);
wenzelm@4338
    38
wenzelm@4338
    39
fun get_session () = ! current_session;
wenzelm@4338
    40
fun add_session s = current_session := ! current_session @ [s];
wenzelm@4338
    41
fun reset_session () = current_session := [];
wenzelm@4338
    42
wenzelm@4925
    43
fun welcome () =
wenzelm@4925
    44
  "Welcome to Isabelle/" ^
wenzelm@4925
    45
    (case get_session () of [] => "Pure" | ss => space_implode "/" ss) ^
wenzelm@4925
    46
    " (" ^ version ^ ")";
wenzelm@4925
    47
wenzelm@4338
    48
wenzelm@4843
    49
wenzelm@4843
    50
(** theory context **)
wenzelm@4338
    51
wenzelm@5027
    52
local
wenzelm@5027
    53
  val current_theory = ref (None: theory option);
wenzelm@5027
    54
in
wenzelm@5027
    55
  fun get_context () = ! current_theory;
wenzelm@5027
    56
  fun set_context opt_thy = current_theory := opt_thy;
wenzelm@5027
    57
end;
wenzelm@4338
    58
wenzelm@5027
    59
fun the_context () =
wenzelm@5027
    60
  (case get_context () of
wenzelm@5027
    61
    Some thy => thy
wenzelm@4364
    62
  | _ => error "Unknown theory context");
wenzelm@4364
    63
wenzelm@5027
    64
fun context thy = set_context (Some thy);
wenzelm@5027
    65
fun reset_context () = set_context None;
wenzelm@4338
    66
wenzelm@4338
    67
wenzelm@4843
    68
(* map context *)
wenzelm@4843
    69
wenzelm@4486
    70
nonfix >>;
wenzelm@5027
    71
fun >> f = set_context (Some (f (the_context ())));
wenzelm@4486
    72
wenzelm@4486
    73
wenzelm@4843
    74
(* retrieve thms *)
wenzelm@4843
    75
wenzelm@5059
    76
fun thm name = PureThy.get_thm (the_context ()) name;
wenzelm@5059
    77
fun thms name = PureThy.get_thms (the_context ()) name;
wenzelm@4843
    78
wenzelm@4843
    79
wenzelm@4914
    80
(* shortcut goal commands *)
wenzelm@4914
    81
nipkow@5042
    82
fun Goal s = Goals.atomic_goal (the_context ()) s;
nipkow@5042
    83
fun Goalw thms s = Goals.atomic_goalw (the_context ()) thms s;
wenzelm@4914
    84
wenzelm@4914
    85
wenzelm@4338
    86
end;
wenzelm@4338
    87
wenzelm@4486
    88
wenzelm@4486
    89
structure BasicContext: BASIC_CONTEXT = Context;
wenzelm@4486
    90
open BasicContext;