<commit_before>(*  Title:      Pure/Thy/context.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>

Global contexts: session and theory.
*)

signature BASIC_CONTEXT =
sig
  val get_session: unit -> string list
  val add_session: string -> unit
  val reset_session: unit -> unit
  val get_context: unit -> theory
  val context: theory -> unit
  val reset_context: unit -> unit
  val thm: xstring -> thm
  val thms: xstring -> thm list
  val Goal: string -> thm list
  val Goalw: thm list -> string -> thm list
end;

signature CONTEXT =
sig
  include BASIC_CONTEXT
  val welcome: unit -> string
  val >> : (theory -> theory) -> unit
end;

structure Context: CONTEXT =
struct


(** session **)

val current_session = ref ([]: string list);

fun get_session () = ! current_session;
fun add_session s = current_session := ! current_session @ [s];
fun reset_session () = current_session := [];

fun welcome () =
  "Welcome to Isabelle/" ^
    (case get_session () of [] => "Pure" | ss => space_implode "/" ss) ^
    " (" ^ version ^ ")";



(** theory context **)

val current_theory = ref (None: theory option);

fun get_context () =
  (case current_theory of
    ref (Some thy) => thy
  | _ => error "Unknown theory context");

fun context thy = current_theory := Some thy;
fun reset_context () = current_theory := None;


(* map context *)

nonfix >>;
fun >> f = current_theory := Some (f (get_context ()));


(* retrieve thms *)

fun thm name = PureThy.get_thm (get_context ()) name;
fun thms name = PureThy.get_thms (get_context ()) name;


(* shortcut goal commands *)

fun Goal s = Goals.goal (get_context ()) s;
fun Goalw thms s = Goals.goalw (get_context ()) thms s;


end;


structure BasicContext: BASIC_CONTEXT = Context;
open BasicContext;
<commit_msg>get_context renamed to the_context; added get_context, set_context;<commit_after>(*  Title:      Pure/Thy/context.ML
    ID:         $Id$
    Author:     <NAME>, <NAME>

Global contexts: session and theory.
*)

signature BASIC_CONTEXT =
sig
  val get_session: unit -> string list
  val add_session: string -> unit
  val reset_session: unit -> unit
  val get_context: unit -> theory option
  val set_context: theory option -> unit
  val the_context: unit -> theory
  val context: theory -> unit
  val reset_context: unit -> unit
  val thm: xstring -> thm
  val thms: xstring -> thm list
  val Goal: string -> thm list
  val Goalw: thm list -> string -> thm list
end;

signature CONTEXT =
sig
  include BASIC_CONTEXT
  val welcome: unit -> string
  val >> : (theory -> theory) -> unit
end;

structure Context: CONTEXT =
struct


(** session **)

val current_session = ref ([]: string list);

fun get_session () = ! current_session;
fun add_session s = current_session := ! current_session @ [s];
fun reset_session () = current_session := [];

fun welcome () =
  "Welcome to Isabelle/" ^
    (case get_session () of [] => "Pure" | ss => space_implode "/" ss) ^
    " (" ^ version ^ ")";



(** theory context **)

local
  val current_theory = ref (None: theory option);
in
  fun get_context () = ! current_theory;
  fun set_context opt_thy = current_theory := opt_thy;
end;

fun the_context () =
  (case get_context () of
    Some thy => thy
  | _ => error "Unknown theory context");

fun context thy = set_context (Some thy);
fun reset_context () = set_context None;


(* map context *)

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


(* retrieve thms *)

fun thm name = PureThy.get_thm (the_context ()) name;
fun thms name = PureThy.get_thms (the_context ()) name;


(* shortcut goal commands *)

fun Goal s = Goals.goal (the_context ()) s;
fun Goalw thms s = Goals.goalw (the_context ()) thms s;


end;


structure BasicContext: BASIC_CONTEXT = Context;
open BasicContext;

{'fraction_non_alphanumeric': 0.12972828982418752, 'fraction_numerical': 0.0, 'mean_word_length': 3.4916267942583734, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 57, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3707914', 'n_tokens_mistral': 1269, 'n_tokens_neox': 1227, 'n_words': 406}