Quelle session.ML Sprache: SML

(*  Title:      Pure/PIDE/session.ML
    Author:     Makarius

Prover session: persistent state of logic image.
*)

signature SESSION =
sig
  val init: string -> unit
  val get_name: unit -> string
  val welcome: unit -> string
  val shutdown: unit -> unit
  val finish: unit -> unit
  val print_context_tracing: (Context.generic -> bool) -> unit
end;

structure Session: SESSION =
struct

(* session name *)

val session = Synchronized.var "Session.session" "";

fun init name = Synchronized.change session (K name);

fun get_name () = Synchronized.value session;

fun description () = (case get_name () of "" => "Isabelle" | name => "Isabelle/" ^ name);

fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading ();

(* finish *)

fun shutdown () =
(Execution.shutdown ();
  Event_Timer.shutdown ();
  Future.shutdown ());

fun finish () =
(shutdown ();
  Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ());
  Thy_Info.finish ();
  shutdown ();
  ignore (Context.finish_tracing ()));

fun print_context_tracing pred =
  List.app (writeln o Proof_Display.print_context_tracing)
    (filter (pred o #1) (#contexts (Context.finish_tracing ())));

end;

quality94%

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.