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