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

Session management -- maintain state of logic images.
*)

signature SESSION =
sig
  val name: unit -> string
  val welcome: unit -> string
  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool ->
    string list -> string -> string -> bool * string -> string -> int -> bool -> unit
  val finish: unit -> unit
end;

structure Session: SESSION =
struct


(* session state *)

val session = ref ([Context.PureN]: string list);
val session_path = ref ([]: string list);
val session_finished = ref false;
val remote_path = ref (NONE: Url.T option);


(* access path *)

fun path () = ! session_path;

fun str_of [] = Context.PureN
  | str_of elems = space_implode "/" elems;

fun name () = "Isabelle/" ^ str_of (path ());
fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";


(* add_path *)

fun add_path reset s =
  let val sess = ! session @ [s] in
    (case duplicates (op =) sess of
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
  end;


(* init *)

fun init reset parent name =
  if not (member (op =) (! session) parent) orelse not (! session_finished) then
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
  else (add_path reset name; session_finished := false);


(* finish *)

fun finish () =
  (Output.accumulated_time ();
    ThyInfo.finish ();
    Present.finish ();
    Toplevel.init_state ();
    session_finished := true);


(* use_dir *)

fun get_rpath rpath =
  (if rpath = "" then () else
     if is_some (! remote_path) then
       error "Path for remote theory browsing information may only be set once"
     else
       remote_path := SOME (Url.explode rpath);
   (! remote_path, rpath <> ""));

fun dumping (_, "") = NONE
  | dumping (cp, path) = SOME (cp, Path.explode path);

fun use_dir root build modes reset info doc doc_graph doc_versions
    parent name dump rpath level verbose =
  Library.setmp print_mode (modes @ ! print_mode)
    (Library.setmp Proofterm.proofs level (fn () =>
      (init reset parent name;
       Present.init build info doc doc_graph doc_versions (path ()) name
         (dumping dump) (get_rpath rpath) verbose;
       ThyInfo.time_use root;
       finish ()))) ()
  handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);


end;
<commit_msg>clarified Present.init;<commit_after>(*  Title:      Pure/Isar/session.ML
    ID:         $Id$
    Author:     <NAME>, TU Muenchen

Session management -- maintain state of logic images.
*)

signature SESSION =
sig
  val name: unit -> string
  val welcome: unit -> string
  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool ->
    string list -> string -> string -> bool * string -> string -> int -> bool -> unit
  val finish: unit -> unit
end;

structure Session: SESSION =
struct


(* session state *)

val session = ref ([Context.PureN]: string list);
val session_path = ref ([]: string list);
val session_finished = ref false;
val remote_path = ref (NONE: Url.T option);


(* access path *)

fun path () = ! session_path;

fun str_of [] = Context.PureN
  | str_of elems = space_implode "/" elems;

fun name () = "Isabelle/" ^ str_of (path ());
fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";


(* add_path *)

fun add_path reset s =
  let val sess = ! session @ [s] in
    (case duplicates (op =) sess of
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
  end;


(* init *)

fun init reset parent name =
  if not (member (op =) (! session) parent) orelse not (! session_finished) then
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
  else (add_path reset name; session_finished := false);


(* finish *)

fun finish () =
  (Output.accumulated_time ();
    ThyInfo.finish ();
    Present.finish ();
    Toplevel.init_state ();
    session_finished := true);


(* use_dir *)

fun get_rpath rpath =
  (if rpath = "" then () else
     if is_some (! remote_path) then
       error "Path for remote theory browsing information may only be set once"
     else
       remote_path := SOME (Url.explode rpath);
   (! remote_path, rpath <> ""));

fun dumping (_, "") = NONE
  | dumping (cp, path) = SOME (cp, Path.explode path);

fun use_dir root build modes reset info doc doc_graph doc_versions
    parent name dump rpath level verbose =
  Library.setmp print_mode (modes @ ! print_mode)
    (Library.setmp Proofterm.proofs level (fn () =>
      (init reset parent name;
       Present.init build info doc doc_graph doc_versions (path ()) name
         (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));
       ThyInfo.time_use root;
       finish ()))) ()
  handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);


end;

{'fraction_non_alphanumeric': 0.13633692458374144, 'fraction_numerical': 0.0003917727717923604, 'mean_word_length': 3.0588235294117645, 'pattern_counts': {'":': 0, '<': 8, '<?xml version=': 0, '>': 50, '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': '3916367', 'n_tokens_mistral': 1658, 'n_tokens_neox': 1598, 'n_words': 545}